:: EUCLID semantic presentation

REAL is non empty V37() V159() V160() V161() V165() set

NAT is ordinal V37() cardinal limit_cardinal V159() V160() V161() V162() V163() V164() V165() Element of bool REAL

bool REAL is V37() set

COMPLEX is non empty V37() V159() V165() set

RAT is non empty V37() V159() V160() V161() V162() V165() set

INT is non empty V37() V159() V160() V161() V162() V163() V165() set

[:COMPLEX,COMPLEX:] is V37() complex-valued set

bool [:COMPLEX,COMPLEX:] is V37() set

[:[:COMPLEX,COMPLEX:],COMPLEX:] is V37() complex-valued set

bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is V37() set

[:REAL,REAL:] is V37() complex-valued ext-real-valued real-valued set

bool [:REAL,REAL:] is V37() set

[:[:REAL,REAL:],REAL:] is V37() complex-valued ext-real-valued real-valued set

bool [:[:REAL,REAL:],REAL:] is V37() set

[:RAT,RAT:] is RAT -valued V37() complex-valued ext-real-valued real-valued set

bool [:RAT,RAT:] is V37() set

[:[:RAT,RAT:],RAT:] is RAT -valued V37() complex-valued ext-real-valued real-valued set

bool [:[:RAT,RAT:],RAT:] is V37() set

[:INT,INT:] is RAT -valued INT -valued V37() complex-valued ext-real-valued real-valued set

bool [:INT,INT:] is V37() set

[:[:INT,INT:],INT:] is RAT -valued INT -valued V37() complex-valued ext-real-valued real-valued set

bool [:[:INT,INT:],INT:] is V37() set

[:NAT,NAT:] is RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set

[:[:NAT,NAT:],NAT:] is RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set

bool [:[:NAT,NAT:],NAT:] is set

omega is ordinal V37() cardinal limit_cardinal V159() V160() V161() V162() V163() V164() V165() set

bool omega is V37() set

bool NAT is V37() set

1 is non empty ordinal natural complex real ext-real positive non negative V33() V34() V37() cardinal V159() V160() V161() V162() V163() V164() Element of NAT

[:1,1:] is RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set

bool [:1,1:] is set

[:[:1,1:],1:] is RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set

bool [:[:1,1:],1:] is set

[:[:1,1:],REAL:] is complex-valued ext-real-valued real-valued set

bool [:[:1,1:],REAL:] is set

2 is non empty ordinal natural complex real ext-real positive non negative V33() V34() V37() cardinal V159() V160() V161() V162() V163() V164() Element of NAT

[:2,2:] is RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set

[:[:2,2:],REAL:] is complex-valued ext-real-valued real-valued set

bool [:[:2,2:],REAL:] is set

K428() is non empty strict multMagma

the carrier of K428() is non empty set

<REAL,+> is non empty strict V130() V131() V132() V134() left-invertible right-invertible invertible left-cancelable right-cancelable V186() multMagma

addreal is Relation-like [:REAL,REAL:] -defined [:REAL,REAL:] -defined REAL -valued REAL -valued Function-like quasi_total quasi_total V76( REAL ) V77( REAL ) complex-valued ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]

multMagma(# REAL,addreal #) is strict multMagma

K434() is non empty strict V132() V134() left-cancelable right-cancelable V186() SubStr of <REAL,+>

<NAT,+> is non empty strict V130() V132() V134() left-cancelable right-cancelable V186() uniquely-decomposable SubStr of K434()

<REAL,*> is non empty strict V130() V132() V134() multMagma

multreal is Relation-like [:REAL,REAL:] -defined [:REAL,REAL:] -defined REAL -valued REAL -valued Function-like quasi_total quasi_total V76( REAL ) V77( REAL ) complex-valued ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]

multMagma(# REAL,multreal #) is strict multMagma

<NAT,*> is non empty strict V130() V132() V134() uniquely-decomposable SubStr of <REAL,*>

K522() is V207() TopStruct

the carrier of K522() is V159() V160() V161() set

RealSpace is non empty strict Reflexive discerning V86() triangle Discerning V207() MetrStruct

K527() is non empty strict TopSpace-like V207() TopStruct

{} is empty ordinal Function-like functional cardinal {} -element FinSequence-membered V159() V160() V161() V162() V163() V164() V165() set

0 is empty ordinal natural complex real ext-real non positive non negative Function-like functional V33() V34() V37() cardinal {} -element FinSequence-membered V159() V160() V161() V162() V163() V164() V165() Element of NAT

3 is non empty ordinal natural complex real ext-real positive non negative V33() V34() V37() cardinal V159() V160() V161() V162() V163() V164() Element of NAT

Seg 1 is non empty trivial V37() 1 -element V159() V160() V161() V162() V163() V164() Element of bool NAT

{ b

{1} is non empty trivial 1 -element V159() V160() V161() V162() V163() V164() set

Seg 2 is non empty V37() 2 -element V159() V160() V161() V162() V163() V164() Element of bool NAT

{ b

{1,2} is non empty V159() V160() V161() V162() V163() V164() set

sqrt 0 is complex real ext-real Element of REAL

sqrt 1 is complex real ext-real Element of REAL

- 1 is complex real ext-real non positive Element of REAL

f is ordinal natural complex real ext-real V37() cardinal set

f -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL

REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL

{ b

f is ordinal natural complex real ext-real V37() cardinal set

(f) is functional FinSequence-membered FinSequenceSet of REAL

f -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL

{ b

f is ordinal natural complex real ext-real V37() cardinal set

(f) is non empty functional FinSequence-membered FinSequenceSet of REAL

f -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL

{ b

f is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (f)

f is Relation-like REAL -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

f is complex real ext-real set

f . f is complex real ext-real Element of REAL

abs f is complex real ext-real Element of REAL

f is Relation-like REAL -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

f is Relation-like REAL -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

x is complex real ext-real Element of REAL

f . x is complex real ext-real Element of REAL

abs x is complex real ext-real Element of REAL

f . x is complex real ext-real Element of REAL

() is Relation-like REAL -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

f is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

|.f.| is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

rng |.f.| is V159() V160() V161() Element of bool REAL

f (#) () is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

dom () is set

rng f is V159() V160() V161() Element of bool REAL

dom |.f.| is V159() V160() V161() V162() V163() V164() Element of bool NAT

dom f is V159() V160() V161() V162() V163() V164() Element of bool NAT

dom (f (#) ()) is V159() V160() V161() V162() V163() V164() Element of bool NAT

x is set

|.f.| . x is complex real ext-real Element of REAL

f . x is complex real ext-real Element of REAL

abs (f . x) is complex real ext-real Element of REAL

() . (f . x) is complex real ext-real Element of REAL

(f (#) ()) . x is complex real ext-real Element of REAL

x is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

M is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

f is ordinal natural complex real ext-real V37() cardinal set

f |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like V37() f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of f -tuples_on REAL

f -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL

{ b

Seg f is V37() f -element V159() V160() V161() V162() V163() V164() Element of bool NAT

{ b

(Seg f) --> 0 is Relation-like Seg f -defined RAT -valued INT -valued {0} -valued Function-like quasi_total V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued Element of bool [:(Seg f),{0}:]

{0} is non empty trivial 1 -element V159() V160() V161() V162() V163() V164() set

[:(Seg f),{0}:] is RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set

bool [:(Seg f),{0}:] is set

f is ordinal natural complex real ext-real V37() cardinal set

(f) is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

f |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like V37() f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of f -tuples_on REAL

f -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL

{ b

Seg f is V37() f -element V159() V160() V161() V162() V163() V164() Element of bool NAT

{ b

(Seg f) --> 0 is Relation-like Seg f -defined RAT -valued INT -valued {0} -valued Function-like quasi_total V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued Element of bool [:(Seg f),{0}:]

[:(Seg f),{0}:] is RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set

bool [:(Seg f),{0}:] is set

(f) is non empty functional FinSequence-membered FinSequenceSet of REAL

f is ordinal natural complex real ext-real V37() cardinal set

(f) is non empty functional FinSequence-membered FinSequenceSet of REAL

f -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL

{ b

f is Relation-like NAT -defined REAL -valued Function-like V37() f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (f)

- f is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

compreal is Relation-like REAL -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

f (#) compreal is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

- 1 is complex real ext-real non positive set

(- 1) (#) f is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

(- 1) multreal is Relation-like REAL -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

K83(REAL) is non empty Relation-like REAL -defined REAL -valued Function-like one-to-one V26( REAL ) complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

multreal [;] ((- 1),K83(REAL)) is set

f (#) ((- 1) multreal) is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

x is ordinal natural complex real ext-real V33() V34() V37() cardinal V159() V160() V161() V162() V163() V164() Element of NAT

x -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL

{ b

M is Relation-like NAT -defined REAL -valued Function-like V37() x -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of x -tuples_on REAL

- M is Relation-like NAT -defined REAL -valued Function-like V37() x -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of x -tuples_on REAL

M (#) compreal is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

(- 1) (#) M is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

M (#) ((- 1) multreal) is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

f is ordinal natural complex real ext-real V37() cardinal set

(f) is non empty functional FinSequence-membered FinSequenceSet of REAL

f -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL

{ b

f is Relation-like NAT -defined REAL -valued Function-like V37() f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (f)

x is Relation-like NAT -defined REAL -valued Function-like V37() f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (f)

f + x is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

addreal .: (f,x) is set

M is ordinal natural complex real ext-real V33() V34() V37() cardinal V159() V160() V161() V162() V163() V164() Element of NAT

M -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL

{ b

M is Relation-like NAT -defined REAL -valued Function-like V37() M -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of M -tuples_on REAL

s is Relation-like NAT -defined REAL -valued Function-like V37() M -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of M -tuples_on REAL

M + s is Relation-like NAT -defined REAL -valued Function-like V37() M -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of M -tuples_on REAL

addreal .: (M,s) is set

f - x is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

diffreal is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]

addreal * (K83(REAL),compreal) is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]

diffreal .: (f,x) is set

- x is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

x (#) compreal is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

(- 1) (#) x is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

x (#) ((- 1) multreal) is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

f + (- x) is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

addreal .: (f,(- x)) is set

M is ordinal natural complex real ext-real V33() V34() V37() cardinal V159() V160() V161() V162() V163() V164() Element of NAT

M -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL

{ b

M is Relation-like NAT -defined REAL -valued Function-like V37() M -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of M -tuples_on REAL

s is Relation-like NAT -defined REAL -valued Function-like V37() M -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of M -tuples_on REAL

M - s is Relation-like NAT -defined REAL -valued Function-like V37() M -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of M -tuples_on REAL

diffreal .: (M,s) is set

- s is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

s (#) compreal is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

(- 1) (#) s is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

s (#) ((- 1) multreal) is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

M + (- s) is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

addreal .: (M,(- s)) is set

f is ordinal natural complex real ext-real V37() cardinal set

(f) is non empty functional FinSequence-membered FinSequenceSet of REAL

f -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL

{ b

f is Relation-like NAT -defined REAL -valued Function-like V37() f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (f)

x is complex real ext-real set

x (#) f is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

x multreal is Relation-like REAL -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

multreal [;] (x,K83(REAL)) is set

f (#) (x multreal) is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

M is ordinal natural complex real ext-real V33() V34() V37() cardinal V159() V160() V161() V162() V163() V164() Element of NAT

M -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL

{ b

M is Relation-like NAT -defined REAL -valued Function-like V37() M -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of M -tuples_on REAL

x * M is Relation-like NAT -defined REAL -valued Function-like V37() M -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of M -tuples_on REAL

M (#) (x multreal) is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

f is ordinal natural complex real ext-real V37() cardinal set

(f) is non empty functional FinSequence-membered FinSequenceSet of REAL

f -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL

{ b

f is Relation-like NAT -defined REAL -valued Function-like V37() f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (f)

|.f.| is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

f (#) () is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

f is ordinal natural complex real ext-real V37() cardinal set

(f) is non empty functional FinSequence-membered FinSequenceSet of REAL

f -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL

{ b

f is Relation-like NAT -defined REAL -valued Function-like V37() f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (f)

f ^2 is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

sqrreal is Relation-like REAL -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

f (#) sqrreal is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

f (#) f is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

multreal .: (f,f) is set

f is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

sqr f is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

f (#) sqrreal is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

f (#) f is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

multreal .: (f,f) is set

Sum (sqr f) is complex real ext-real Element of REAL

sqrt (Sum (sqr f)) is complex real ext-real Element of REAL

f is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

len f is ordinal natural complex real ext-real V33() V34() V37() cardinal V159() V160() V161() V162() V163() V164() Element of NAT

((len f)) is non empty functional FinSequence-membered FinSequenceSet of REAL

(len f) -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL

{ b

rng f is V159() V160() V161() Element of bool REAL

f is ordinal natural complex real ext-real V37() cardinal set

(f) is Relation-like NAT -defined REAL -valued Function-like V37() f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (f)

(f) is non empty functional FinSequence-membered FinSequenceSet of REAL

f -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL

{ b

f |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like V37() f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of f -tuples_on REAL

Seg f is V37() f -element V159() V160() V161() V162() V163() V164() Element of bool NAT

{ b

(Seg f) --> 0 is Relation-like Seg f -defined RAT -valued INT -valued {0} -valued Function-like quasi_total V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued Element of bool [:(Seg f),{0}:]

[:(Seg f),{0}:] is RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set

bool [:(Seg f),{0}:] is set

(f,(f)) is Relation-like NAT -defined REAL -valued Function-like V37() f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of f -tuples_on REAL

(f) (#) () is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

f is ordinal natural complex real ext-real V33() V34() V37() cardinal V159() V160() V161() V162() V163() V164() Element of NAT

() . 0 is complex real ext-real Element of REAL

f |-> (() . 0) is Relation-like NAT -defined REAL -valued Function-like V37() f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of f -tuples_on REAL

f -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL

{ b

Seg f is V37() f -element V159() V160() V161() V162() V163() V164() Element of bool NAT

{ b

(Seg f) --> (() . 0) is Relation-like Seg f -defined {(() . 0)} -valued Function-like quasi_total V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of bool [:(Seg f),{(() . 0)}:]

{(() . 0)} is non empty trivial 1 -element V159() V160() V161() set

[:(Seg f),{(() . 0)}:] is complex-valued ext-real-valued real-valued set

bool [:(Seg f),{(() . 0)}:] is set

abs 0 is complex real ext-real V34() Element of REAL

f |-> (abs 0) is Relation-like NAT -defined REAL -valued Function-like V37() f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of f -tuples_on REAL

(Seg f) --> (abs 0) is Relation-like Seg f -defined RAT -valued {(abs 0)} -valued Function-like quasi_total V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of bool [:(Seg f),{(abs 0)}:]

{(abs 0)} is non empty trivial 1 -element V159() V160() V161() V162() set

[:(Seg f),{(abs 0)}:] is RAT -valued complex-valued ext-real-valued real-valued set

bool [:(Seg f),{(abs 0)}:] is set

f is Relation-like Function-like complex-valued set

- f is Relation-like Function-like complex-valued set

(- 1) (#) f is Relation-like Function-like complex-valued set

|.(- f).| is Relation-like Function-like complex-valued ext-real-valued real-valued set

|.f.| is Relation-like Function-like complex-valued ext-real-valued real-valued set

dom |.(- f).| is set

dom (- f) is set

dom |.f.| is set

dom f is set

f is set

|.(- f).| . f is complex real ext-real Element of REAL

(- f) . f is complex set

abs ((- f) . f) is complex real ext-real Element of REAL

f . f is complex set

- (f . f) is complex Element of COMPLEX

abs (- (f . f)) is complex real ext-real Element of REAL

abs (f . f) is complex real ext-real Element of REAL

|.f.| . f is complex real ext-real Element of REAL

f is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

f is complex real ext-real set

f * f is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

f multreal is Relation-like REAL -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

multreal [;] (f,K83(REAL)) is set

f (#) (f multreal) is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

((f * f)) is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

(f * f) (#) () is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

(f) is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

f (#) () is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

abs f is complex real ext-real Element of REAL

(abs f) * (f) is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

(abs f) multreal is Relation-like REAL -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

multreal [;] ((abs f),K83(REAL)) is set

(f) (#) ((abs f) multreal) is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

f is ordinal natural complex real ext-real V37() cardinal set

(f) is Relation-like NAT -defined REAL -valued Function-like V37() f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (f)

(f) is non empty functional FinSequence-membered FinSequenceSet of REAL

f -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL

{ b

f |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like V37() f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of f -tuples_on REAL

Seg f is V37() f -element V159() V160() V161() V162() V163() V164() Element of bool NAT

{ b

(Seg f) --> 0 is Relation-like Seg f -defined RAT -valued INT -valued {0} -valued Function-like quasi_total V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued Element of bool [:(Seg f),{0}:]

[:(Seg f),{0}:] is RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set

bool [:(Seg f),{0}:] is set

((f)) is complex real ext-real Element of REAL

sqr (f) is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

(f) (#) sqrreal is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

(f) (#) (f) is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

multreal .: ((f),(f)) is set

Sum (sqr (f)) is complex real ext-real Element of REAL

sqrt (Sum (sqr (f))) is complex real ext-real Element of REAL

0 ^2 is complex real ext-real Element of REAL

0 * 0 is empty ordinal complex real ext-real non positive non negative Function-like functional cardinal {} -element FinSequence-membered V159() V160() V161() V162() V163() V164() V165() set

f |-> (0 ^2) is Relation-like NAT -defined REAL -valued Function-like V37() f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of f -tuples_on REAL

(Seg f) --> (0 ^2) is Relation-like Seg f -defined {(0 ^2)} -valued Function-like quasi_total V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of bool [:(Seg f),{(0 ^2)}:]

{(0 ^2)} is non empty trivial 1 -element V159() V160() V161() set

[:(Seg f),{(0 ^2)}:] is complex-valued ext-real-valued real-valued set

bool [:(Seg f),{(0 ^2)}:] is set

Sum (f |-> (0 ^2)) is complex real ext-real Element of REAL

sqrt (Sum (f |-> (0 ^2))) is complex real ext-real Element of REAL

f * 0 is complex real ext-real Element of REAL

sqrt (f * 0) is complex real ext-real Element of REAL

f is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

(f) is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

f (#) () is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

sqr (f) is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

(f) (#) sqrreal is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

(f) (#) (f) is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

multreal .: ((f),(f)) is set

sqr f is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

f (#) sqrreal is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

f (#) f is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

multreal .: (f,f) is set

len f is ordinal natural complex real ext-real V33() V34() V37() cardinal V159() V160() V161() V162() V163() V164() Element of NAT

((len f)) is non empty functional FinSequence-membered FinSequenceSet of REAL

(len f) -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL

{ b

M is ordinal natural complex real ext-real V37() cardinal set

Seg (len f) is V37() len f -element V159() V160() V161() V162() V163() V164() Element of bool NAT

{ b

x is Relation-like NAT -defined REAL -valued Function-like V37() len f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of ((len f))

((len f),x) is Relation-like NAT -defined REAL -valued Function-like V37() len f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (len f) -tuples_on REAL

x (#) () is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

sqr ((len f),x) is Relation-like NAT -defined REAL -valued Function-like V37() len f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (len f) -tuples_on REAL

((len f),x) (#) sqrreal is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

((len f),x) (#) ((len f),x) is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

multreal .: (((len f),x),((len f),x)) is set

(sqr ((len f),x)) . M is complex real ext-real Element of REAL

((len f),x) . M is complex real ext-real Element of REAL

(((len f),x) . M) ^2 is complex real ext-real Element of REAL

(((len f),x) . M) * (((len f),x) . M) is complex real ext-real set

x . M is complex real ext-real Element of REAL

abs (x . M) is complex real ext-real Element of REAL

(abs (x . M)) ^2 is complex real ext-real Element of REAL

(abs (x . M)) * (abs (x . M)) is complex real ext-real set

(x . M) ^2 is complex real ext-real Element of REAL

(x . M) * (x . M) is complex real ext-real set

((len f),x) is Relation-like NAT -defined REAL -valued Function-like V37() len f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (len f) -tuples_on REAL

x (#) sqrreal is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

x (#) x is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

multreal .: (x,x) is set

((len f),x) . M is complex real ext-real Element of REAL

f is ordinal natural complex real ext-real V37() cardinal set

(f) is non empty functional FinSequence-membered FinSequenceSet of REAL

f -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL

{ b

(f) is Relation-like NAT -defined REAL -valued Function-like V37() f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (f)

f |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like V37() f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of f -tuples_on REAL

Seg f is V37() f -element V159() V160() V161() V162() V163() V164() Element of bool NAT

{ b

(Seg f) --> 0 is Relation-like Seg f -defined RAT -valued INT -valued {0} -valued Function-like quasi_total V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued Element of bool [:(Seg f),{0}:]

[:(Seg f),{0}:] is RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set

bool [:(Seg f),{0}:] is set

f is Relation-like NAT -defined REAL -valued Function-like V37() f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (f)

(f) is complex real ext-real Element of REAL

sqr f is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

f (#) sqrreal is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

f (#) f is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

multreal .: (f,f) is set

Sum (sqr f) is complex real ext-real Element of REAL

sqrt (Sum (sqr f)) is complex real ext-real Element of REAL

x is ordinal natural complex real ext-real V37() cardinal set

f . x is complex real ext-real Element of REAL

(f,f) is Relation-like NAT -defined REAL -valued Function-like V37() f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of f -tuples_on REAL

Sum (f,f) is complex real ext-real Element of REAL

(f,f) is Relation-like NAT -defined REAL -valued Function-like V37() f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of f -tuples_on REAL

f (#) () is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

sqr (f,f) is Relation-like NAT -defined REAL -valued Function-like V37() f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of f -tuples_on REAL

(f,f) (#) sqrreal is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

(f,f) (#) (f,f) is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

multreal .: ((f,f),(f,f)) is set

Sum (sqr (f,f)) is complex real ext-real Element of REAL

(f,f) . x is complex real ext-real Element of REAL

(f |-> 0) . x is empty ordinal complex real ext-real non positive non negative Function-like functional cardinal {} -element FinSequence-membered V159() V160() V161() V162() V163() V164() V165() Element of REAL

M is complex real ext-real Element of REAL

abs M is complex real ext-real Element of REAL

f is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

(f) is complex real ext-real Element of REAL

sqr f is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

f (#) sqrreal is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

f (#) f is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

multreal .: (f,f) is set

Sum (sqr f) is complex real ext-real Element of REAL

sqrt (Sum (sqr f)) is complex real ext-real Element of REAL

f is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

(f) is complex real ext-real Element of REAL

sqr f is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

f (#) sqrreal is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

f (#) f is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

multreal .: (f,f) is set

Sum (sqr f) is complex real ext-real Element of REAL

sqrt (Sum (sqr f)) is complex real ext-real Element of REAL

f is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

- f is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

f (#) compreal is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

(- 1) (#) f is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

f (#) ((- 1) multreal) is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

((- f)) is complex real ext-real non negative Element of REAL

sqr (- f) is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

(- f) (#) sqrreal is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

(- f) (#) (- f) is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

multreal .: ((- f),(- f)) is set

Sum (sqr (- f)) is complex real ext-real Element of REAL

sqrt (Sum (sqr (- f))) is complex real ext-real Element of REAL

(f) is complex real ext-real non negative Element of REAL

sqr f is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

f (#) sqrreal is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

f (#) f is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

multreal .: (f,f) is set

Sum (sqr f) is complex real ext-real Element of REAL

sqrt (Sum (sqr f)) is complex real ext-real Element of REAL

((- f)) is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

(- f) (#) () is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

sqr ((- f)) is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

((- f)) (#) sqrreal is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

((- f)) (#) ((- f)) is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

multreal .: (((- f)),((- f))) is set

Sum (sqr ((- f))) is complex real ext-real Element of REAL

sqrt (Sum (sqr ((- f)))) is complex real ext-real Element of REAL

(f) is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

f (#) () is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

sqr (f) is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

(f) (#) sqrreal is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

(f) (#) (f) is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

multreal .: ((f),(f)) is set

Sum (sqr (f)) is complex real ext-real Element of REAL

sqrt (Sum (sqr (f))) is complex real ext-real Element of REAL

f is complex real ext-real set

abs f is complex real ext-real Element of REAL

f is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

f * f is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

f multreal is Relation-like REAL -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

multreal [;] (f,K83(REAL)) is set

f (#) (f multreal) is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

((f * f)) is complex real ext-real non negative Element of REAL

sqr (f * f) is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

(f * f) (#) sqrreal is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

(f * f) (#) (f * f) is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

multreal .: ((f * f),(f * f)) is set

Sum (sqr (f * f)) is complex real ext-real Element of REAL

sqrt (Sum (sqr (f * f))) is complex real ext-real Element of REAL

(f) is complex real ext-real non negative Element of REAL

sqr f is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

f (#) sqrreal is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

f (#) f is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

multreal .: (f,f) is set

Sum (sqr f) is complex real ext-real Element of REAL

sqrt (Sum (sqr f)) is complex real ext-real Element of REAL

(abs f) * (f) is complex real ext-real Element of REAL

len f is ordinal natural complex real ext-real V33() V34() V37() cardinal V159() V160() V161() V162() V163() V164() Element of NAT

((len f)) is non empty functional FinSequence-membered FinSequenceSet of REAL

(len f) -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL

{ b

(abs f) ^2 is complex real ext-real Element of REAL

(abs f) * (abs f) is complex real ext-real set

M is Relation-like NAT -defined REAL -valued Function-like V37() len f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of ((len f))

((len f),M) is Relation-like NAT -defined REAL -valued Function-like V37() len f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (len f) -tuples_on REAL

M (#) () is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

sqr ((len f),M) is Relation-like NAT -defined REAL -valued Function-like V37() len f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (len f) -tuples_on REAL

((len f),M) (#) sqrreal is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

((len f),M) (#) ((len f),M) is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

multreal .: (((len f),M),((len f),M)) is set

Sum (sqr ((len f),M)) is complex real ext-real Element of REAL

((len f),M,f) is Relation-like NAT -defined REAL -valued Function-like V37() len f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of ((len f))

M (#) (f multreal) is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

((len f),((len f),M,f)) is Relation-like NAT -defined REAL -valued Function-like V37() len f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (len f) -tuples_on REAL

((len f),M,f) (#) () is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

sqr ((len f),((len f),M,f)) is Relation-like NAT -defined REAL -valued Function-like V37() len f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (len f) -tuples_on REAL

((len f),((len f),M,f)) (#) sqrreal is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

((len f),((len f),M,f)) (#) ((len f),((len f),M,f)) is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

multreal .: (((len f),((len f),M,f)),((len f),((len f),M,f))) is set

Sum (sqr ((len f),((len f),M,f))) is complex real ext-real Element of REAL

sqrt (Sum (sqr ((len f),((len f),M,f)))) is complex real ext-real Element of REAL

(abs f) * ((len f),M) is Relation-like NAT -defined REAL -valued Function-like V37() len f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (len f) -tuples_on REAL

(abs f) multreal is Relation-like REAL -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

multreal [;] ((abs f),K83(REAL)) is set

((len f),M) (#) ((abs f) multreal) is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

sqr ((abs f) * ((len f),M)) is Relation-like NAT -defined REAL -valued Function-like V37() len f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (len f) -tuples_on REAL

((abs f) * ((len f),M)) (#) sqrreal is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

((abs f) * ((len f),M)) (#) ((abs f) * ((len f),M)) is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

multreal .: (((abs f) * ((len f),M)),((abs f) * ((len f),M))) is set

Sum (sqr ((abs f) * ((len f),M))) is complex real ext-real Element of REAL

sqrt (Sum (sqr ((abs f) * ((len f),M)))) is complex real ext-real Element of REAL

((abs f) ^2) * (sqr ((len f),M)) is Relation-like NAT -defined REAL -valued Function-like V37() len f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (len f) -tuples_on REAL

((abs f) ^2) multreal is Relation-like REAL -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

multreal [;] (((abs f) ^2),K83(REAL)) is set

(sqr ((len f),M)) (#) (((abs f) ^2) multreal) is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

Sum (((abs f) ^2) * (sqr ((len f),M))) is complex real ext-real Element of REAL

sqrt (Sum (((abs f) ^2) * (sqr ((len f),M)))) is complex real ext-real Element of REAL

((abs f) ^2) * (Sum (sqr ((len f),M))) is complex real ext-real Element of REAL

sqrt (((abs f) ^2) * (Sum (sqr ((len f),M)))) is complex real ext-real Element of REAL

sqrt ((abs f) ^2) is complex real ext-real Element of REAL

sqrt (Sum (sqr ((len f),M))) is complex real ext-real Element of REAL

(sqrt ((abs f) ^2)) * (sqrt (Sum (sqr ((len f),M)))) is complex real ext-real Element of REAL

(abs f) * (sqrt (Sum (sqr ((len f),M)))) is complex real ext-real Element of REAL

f is ordinal natural complex real ext-real V37() cardinal set

(f) is non empty functional FinSequence-membered FinSequenceSet of REAL

f -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL

{ b

f is Relation-like NAT -defined REAL -valued Function-like V37() f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (f)

(f) is complex real ext-real non negative Element of REAL

sqr f is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

f (#) sqrreal is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

f (#) f is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

multreal .: (f,f) is set

Sum (sqr f) is complex real ext-real Element of REAL

sqrt (Sum (sqr f)) is complex real ext-real Element of REAL

x is Relation-like NAT -defined REAL -valued Function-like V37() f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (f)

(f,f,x) is Relation-like NAT -defined REAL -valued Function-like V37() f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (f)

addreal .: (f,x) is set

((f,f,x)) is complex real ext-real non negative Element of REAL

sqr (f,f,x) is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

(f,f,x) (#) sqrreal is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

(f,f,x) (#) (f,f,x) is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

multreal .: ((f,f,x),(f,f,x)) is set

Sum (sqr (f,f,x)) is complex real ext-real Element of REAL

sqrt (Sum (sqr (f,f,x))) is complex real ext-real Element of REAL

(x) is complex real ext-real non negative Element of REAL

sqr x is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

x (#) sqrreal is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

x (#) x is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

multreal .: (x,x) is set

Sum (sqr x) is complex real ext-real Element of REAL

sqrt (Sum (sqr x)) is complex real ext-real Element of REAL

(f) + (x) is complex real ext-real non negative Element of REAL

(f,(f,f,x)) is Relation-like NAT -defined REAL -valued Function-like V37() f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of f -tuples_on REAL

Sum (f,(f,f,x)) is complex real ext-real Element of REAL

(f,f) is Relation-like NAT -defined REAL -valued Function-like V37() f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of f -tuples_on REAL

f (#) () is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

sqr (f,f) is Relation-like NAT -defined REAL -valued Function-like V37() f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of f -tuples_on REAL

(f,f) (#) sqrreal is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

(f,f) (#) (f,f) is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

multreal .: ((f,f),(f,f)) is set

Sum (sqr (f,f)) is complex real ext-real Element of REAL

sqrt (Sum (sqr (f,f))) is complex real ext-real Element of REAL

Seg f is V37() f -element V159() V160() V161() V162() V163() V164() Element of bool NAT

{ b

(f,(f,f,x)) is Relation-like NAT -defined REAL -valued Function-like V37() f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of f -tuples_on REAL

(f,f,x) (#) () is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

sqr (f,(f,f,x)) is Relation-like NAT -defined REAL -valued Function-like V37() f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of f -tuples_on REAL

(f,(f,f,x)) (#) sqrreal is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

(f,(f,f,x)) (#) (f,(f,f,x)) is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

multreal .: ((f,(f,f,x)),(f,(f,f,x))) is set

(f,x) is Relation-like NAT -defined REAL -valued Function-like V37() f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of f -tuples_on REAL

x (#) () is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

(f,f) + (f,x) is Relation-like NAT -defined REAL -valued Function-like V37() f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of f -tuples_on REAL

addreal .: ((f,f),(f,x)) is set

sqr ((f,f) + (f,x)) is Relation-like NAT -defined REAL -valued Function-like V37() f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of f -tuples_on REAL

((f,f) + (f,x)) (#) sqrreal is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

((f,f) + (f,x)) (#) ((f,f) + (f,x)) is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

multreal .: (((f,f) + (f,x)),((f,f) + (f,x))) is set

M is ordinal natural complex real ext-real V37() cardinal set

(sqr (f,(f,f,x))) . M is complex real ext-real Element of REAL

(sqr ((f,f) + (f,x))) . M is complex real ext-real Element of REAL

len (f,f,x) is ordinal natural complex real ext-real V33() V34() V37() cardinal V159() V160() V161() V162() V163() V164() Element of NAT

dom (f,f,x) is f -element V159() V160() V161() V162() V163() V164() Element of bool NAT

(f,f) . M is complex real ext-real Element of REAL

(f,x) . M is complex real ext-real Element of REAL

(f,f,x) . M is complex real ext-real Element of REAL

f . M is complex real ext-real Element of REAL

x . M is complex real ext-real Element of REAL

y is complex real ext-real Element of REAL

r22 is complex real ext-real Element of REAL

y + r22 is complex real ext-real Element of REAL

abs (y + r22) is complex real ext-real Element of REAL

abs y is complex real ext-real Element of REAL

abs r22 is complex real ext-real Element of REAL

(abs y) + (abs r22) is complex real ext-real Element of REAL

f is complex real ext-real Element of REAL

abs f is complex real ext-real Element of REAL

s is complex real ext-real Element of REAL

(abs y) + s is complex real ext-real Element of REAL

M is complex real ext-real Element of REAL

M + s is complex real ext-real Element of REAL

(f,(f,f,x)) . M is complex real ext-real Element of REAL

((f,f) + (f,x)) . M is complex real ext-real Element of REAL

abs912 is complex real ext-real Element of REAL

len ((f,f) + (f,x)) is ordinal natural complex real ext-real V33() V34() V37() cardinal V159() V160() V161() V162() V163() V164() Element of NAT

dom ((f,f) + (f,x)) is f -element V159() V160() V161() V162() V163() V164() Element of bool NAT

abs12 is complex real ext-real Element of REAL

abs912 ^2 is complex real ext-real Element of REAL

abs912 * abs912 is complex real ext-real set

abs12 ^2 is complex real ext-real Element of REAL

abs12 * abs12 is complex real ext-real set

mlt ((f,f),(f,x)) is Relation-like NAT -defined REAL -valued Function-like V37() f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of f -tuples_on REAL

multreal .: ((f,f),(f,x)) is set

Sum (mlt ((f,f),(f,x))) is complex real ext-real Element of REAL

(Sum (mlt ((f,f),(f,x)))) ^2 is complex real ext-real Element of REAL

(Sum (mlt ((f,f),(f,x)))) * (Sum (mlt ((f,f),(f,x)))) is complex real ext-real set

sqrt ((Sum (mlt ((f,f),(f,x)))) ^2) is complex real ext-real Element of REAL

sqr (f,x) is Relation-like NAT -defined REAL -valued Function-like V37() f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of f -tuples_on REAL

(f,x) (#) sqrreal is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

(f,x) (#) (f,x) is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

multreal .: ((f,x),(f,x)) is set

Sum (sqr (f,x)) is complex real ext-real Element of REAL

(Sum (sqr (f,f))) * (Sum (sqr (f,x))) is complex real ext-real Element of REAL

sqrt ((Sum (sqr (f,f))) * (Sum (sqr (f,x)))) is complex real ext-real Element of REAL

M is ordinal natural complex real ext-real V37() cardinal set

(mlt ((f,f),(f,x))) . M is complex real ext-real Element of REAL

f . M is complex real ext-real Element of REAL

x . M is complex real ext-real Element of REAL

(f,f) . M is complex real ext-real Element of REAL

s is complex real ext-real Element of REAL

abs s is complex real ext-real Element of REAL

(f,x) . M is complex real ext-real Element of REAL

f is complex real ext-real Element of REAL

abs f is complex real ext-real Element of REAL

(abs s) * (abs f) is complex real ext-real Element of REAL

len (mlt ((f,f),(f,x))) is ordinal natural complex real ext-real V33() V34() V37() cardinal V159() V160() V161() V162() V163() V164() Element of NAT

dom (mlt ((f,f),(f,x))) is f -element V159() V160() V161() V162() V163() V164() Element of bool NAT

2 * (Sum (mlt ((f,f),(f,x)))) is complex real ext-real Element of REAL

2 * (sqrt ((Sum (sqr (f,f))) * (Sum (sqr (f,x))))) is complex real ext-real Element of REAL

(Sum (sqr (f,f))) + (2 * (Sum (mlt ((f,f),(f,x))))) is complex real ext-real Element of REAL

(Sum (sqr (f,f))) + (2 * (sqrt ((Sum (sqr (f,f))) * (Sum (sqr (f,x)))))) is complex real ext-real Element of REAL

((Sum (sqr (f,f))) + (2 * (Sum (mlt ((f,f),(f,x)))))) + (Sum (sqr (f,x))) is complex real ext-real Element of REAL

((Sum (sqr (f,f))) + (2 * (sqrt ((Sum (sqr (f,f))) * (Sum (sqr (f,x))))))) + (Sum (sqr (f,x))) is complex real ext-real Element of REAL

sqrt (Sum (sqr (f,x))) is complex real ext-real Element of REAL

Sum (sqr ((f,f) + (f,x))) is complex real ext-real Element of REAL

2 * (mlt ((f,f),(f,x))) is Relation-like NAT -defined REAL -valued Function-like V37() f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of f -tuples_on REAL

2 multreal is Relation-like REAL -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

multreal [;] (2,K83(REAL)) is set

(mlt ((f,f),(f,x))) (#) (2 multreal) is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

(sqr (f,f)) + (2 * (mlt ((f,f),(f,x)))) is Relation-like NAT -defined REAL -valued Function-like V37() f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of f -tuples_on REAL

addreal .: ((sqr (f,f)),(2 * (mlt ((f,f),(f,x))))) is set

((sqr (f,f)) + (2 * (mlt ((f,f),(f,x))))) + (sqr (f,x)) is Relation-like NAT -defined REAL -valued Function-like V37() f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of f -tuples_on REAL

addreal .: (((sqr (f,f)) + (2 * (mlt ((f,f),(f,x))))),(sqr (f,x))) is set

Sum (((sqr (f,f)) + (2 * (mlt ((f,f),(f,x))))) + (sqr (f,x))) is complex real ext-real Element of REAL

Sum ((sqr (f,f)) + (2 * (mlt ((f,f),(f,x))))) is complex real ext-real Element of REAL

(Sum ((sqr (f,f)) + (2 * (mlt ((f,f),(f,x)))))) + (Sum (sqr (f,x))) is complex real ext-real Element of REAL

Sum (2 * (mlt ((f,f),(f,x)))) is complex real ext-real Element of REAL

(Sum (sqr (f,f))) + (Sum (2 * (mlt ((f,f),(f,x))))) is complex real ext-real Element of REAL

((Sum (sqr (f,f))) + (Sum (2 * (mlt ((f,f),(f,x)))))) + (Sum (sqr (f,x))) is complex real ext-real Element of REAL

Sum (sqr (f,(f,f,x))) is complex real ext-real Element of REAL

(sqrt (Sum (sqr (f,f)))) * (sqrt (Sum (sqr (f,x)))) is complex real ext-real Element of REAL

2 * ((sqrt (Sum (sqr (f,f)))) * (sqrt (Sum (sqr (f,x))))) is complex real ext-real Element of REAL

(Sum (sqr (f,f))) + (2 * ((sqrt (Sum (sqr (f,f)))) * (sqrt (Sum (sqr (f,x)))))) is complex real ext-real Element of REAL

((Sum (sqr (f,f))) + (2 * ((sqrt (Sum (sqr (f,f)))) * (sqrt (Sum (sqr (f,x))))))) + (Sum (sqr (f,x))) is complex real ext-real Element of REAL

(sqrt (Sum (sqr (f,x)))) ^2 is complex real ext-real Element of REAL

(sqrt (Sum (sqr (f,x)))) * (sqrt (Sum (sqr (f,x)))) is complex real ext-real set

(sqrt (Sum (sqr (f,f)))) ^2 is complex real ext-real Element of REAL

(sqrt (Sum (sqr (f,f)))) * (sqrt (Sum (sqr (f,f)))) is complex real ext-real set

sqrt (Sum (f,(f,f,x))) is complex real ext-real Element of REAL

(sqrt (Sum (sqr (f,f)))) + (sqrt (Sum (sqr (f,x)))) is complex real ext-real Element of REAL

((sqrt (Sum (sqr (f,f)))) + (sqrt (Sum (sqr (f,x))))) ^2 is complex real ext-real Element of REAL

((sqrt (Sum (sqr (f,f)))) + (sqrt (Sum (sqr (f,x))))) * ((sqrt (Sum (sqr (f,f)))) + (sqrt (Sum (sqr (f,x))))) is complex real ext-real set

sqrt (((sqrt (Sum (sqr (f,f)))) + (sqrt (Sum (sqr (f,x))))) ^2) is complex real ext-real Element of REAL

(f,x) is Relation-like NAT -defined REAL -valued Function-like V37() f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of f -tuples_on REAL

Sum (f,x) is complex real ext-real Element of REAL

sqrt (Sum (f,x)) is complex real ext-real Element of REAL

(sqrt (