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
{ b1 where b1 is ordinal natural complex real ext-real V33() V34() V37() cardinal V159() V160() V161() V162() V163() V164() Element of NAT : ( 1 <= b1 & b1 <= 1 ) } is set
{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
{ b1 where b1 is ordinal natural complex real ext-real V33() V34() V37() cardinal V159() V160() V161() V162() V163() V164() Element of NAT : ( 1 <= b1 & b1 <= 2 ) } is set
{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
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = f } is set
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
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = f } 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
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = f } is set
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
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = f } is set
Seg f is V37() f -element V159() V160() V161() V162() V163() V164() Element of bool NAT
{ b1 where b1 is ordinal natural complex real ext-real V33() V34() V37() cardinal V159() V160() V161() V162() V163() V164() Element of NAT : ( 1 <= b1 & b1 <= f ) } is set
(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
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = f } is set
Seg f is V37() f -element V159() V160() V161() V162() V163() V164() Element of bool NAT
{ b1 where b1 is ordinal natural complex real ext-real V33() V34() V37() cardinal V159() V160() V161() V162() V163() V164() Element of NAT : ( 1 <= b1 & b1 <= f ) } is set
(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
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = f } 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 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
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = x } is set
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
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = f } 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)
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
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = M } is set
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
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = M } is set
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
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = f } 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)
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
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = M } is set
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
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = f } 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 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
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = f } 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 ^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
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = len f } is set
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
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = f } is 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
Seg f is V37() f -element V159() V160() V161() V162() V163() V164() Element of bool NAT
{ b1 where b1 is ordinal natural complex real ext-real V33() V34() V37() cardinal V159() V160() V161() V162() V163() V164() Element of NAT : ( 1 <= b1 & b1 <= f ) } is set
(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
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = f } is set
Seg f is V37() f -element V159() V160() V161() V162() V163() V164() Element of bool NAT
{ b1 where b1 is ordinal natural complex real ext-real V33() V34() V37() cardinal V159() V160() V161() V162() V163() V164() Element of NAT : ( 1 <= b1 & b1 <= f ) } is set
(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
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = f } is 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
Seg f is V37() f -element V159() V160() V161() V162() V163() V164() Element of bool NAT
{ b1 where b1 is ordinal natural complex real ext-real V33() V34() V37() cardinal V159() V160() V161() V162() V163() V164() Element of NAT : ( 1 <= b1 & b1 <= f ) } is set
(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
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = len f } is set
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
{ b1 where b1 is ordinal natural complex real ext-real V33() V34() V37() cardinal V159() V160() V161() V162() V163() V164() Element of NAT : ( 1 <= b1 & b1 <= len f ) } is set
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
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = f } 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 |-> 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
{ b1 where b1 is ordinal natural complex real ext-real V33() V34() V37() cardinal V159() V160() V161() V162() V163() V164() Element of NAT : ( 1 <= b1 & b1 <= f ) } is set
(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
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = len f } is set
(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
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = f } 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 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
{ b1 where b1 is ordinal natural complex real ext-real V33() V34() V37() cardinal V159() V160() V161() V162() V163() V164() Element of NAT : ( 1 <= b1 & b1 <= f ) } is 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
(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 (