REAL is non empty non trivial non finite complex-membered ext-real-membered real-membered V132() set
NAT is non trivial ordinal non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V132() Element of bool REAL
bool REAL is non trivial non finite set
omega is non trivial ordinal non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V132() set
bool omega is non trivial non finite set
bool NAT is non trivial non finite set
COMPLEX is non empty non trivial non finite complex-membered V132() set
RAT is non empty non trivial non finite complex-membered ext-real-membered real-membered rational-membered V132() set
INT is non empty non trivial non finite complex-membered ext-real-membered real-membered rational-membered integer-membered V132() set
[:REAL,REAL:] is Relation-like non trivial complex-valued ext-real-valued real-valued non finite set
bool [:REAL,REAL:] is non trivial non finite set
K282() is non empty strict multMagma
the carrier of K282() is non empty set
K287() is non empty strict V107() V108() V109() V111() V148() V149() V150() V151() V152() V153() multMagma
K288() is non empty strict V109() V111() V151() V152() V153() M13(K287())
K289() is non empty strict V107() V109() V111() V151() V152() V153() V154() M16(K287(),K288())
K291() is non empty strict V107() V109() V111() multMagma
K292() is non empty strict V107() V109() V111() V154() M13(K291())
1 is non empty ext-real positive non negative ordinal natural complex real V43() V44() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
[:1,1:] is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued finite set
bool [:1,1:] is finite V49() set
[:[:1,1:],1:] is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued finite set
bool [:[:1,1:],1:] is finite V49() set
[:[:1,1:],REAL:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:[:1,1:],REAL:] is set
[:[:REAL,REAL:],REAL:] is Relation-like non trivial complex-valued ext-real-valued real-valued non finite set
bool [:[:REAL,REAL:],REAL:] is non trivial non finite set
2 is non empty ext-real positive non negative ordinal natural complex real V43() V44() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
[:2,2:] is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued finite set
[:[:2,2:],REAL:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:[:2,2:],REAL:] is set
TOP-REAL 2 is non empty left_complementable right_complementable V138() V139() TopSpace-like Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed strict L16()
the carrier of (TOP-REAL 2) is non empty set
K596() is non empty strict TopSpace-like real-membered TopStruct
the carrier of K596() is non empty complex-membered ext-real-membered real-membered set
RealSpace is strict real-membered MetrStruct
real_dist is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like total V18([:REAL,REAL:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]
MetrStruct(# REAL,real_dist #) is strict MetrStruct
R^1 is non empty strict TopSpace-like real-membered TopStruct
TopSpaceMetr RealSpace is TopStruct
the carrier of RealSpace is complex-membered ext-real-membered real-membered set
Family_open_set RealSpace is Element of bool (bool the carrier of RealSpace)
bool the carrier of RealSpace is set
bool (bool the carrier of RealSpace) is set
TopStruct(# the carrier of RealSpace,(Family_open_set RealSpace) #) is strict TopStruct
K603() is non empty strict TopSpace-like real-membered SubSpace of R^1
[:K603(),K603():] is non empty strict TopSpace-like TopStruct
the carrier of [:K603(),K603():] is non empty set
K605() is non empty strict TopSpace-like real-membered V244() SubSpace of R^1
the carrier of K605() is non empty complex-membered ext-real-membered real-membered set
bool the carrier of K605() is set
bool (bool the carrier of K605()) is set
Tunit_circle 2 is non empty TopSpace-like V245() SubSpace of TOP-REAL 2
0. (TOP-REAL 2) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite 2 -element FinSequence-like FinSubsequence-like zero V268() Element of the carrier of (TOP-REAL 2)
the ZeroF of (TOP-REAL 2) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite 2 -element FinSequence-like FinSubsequence-like V268() Element of the carrier of (TOP-REAL 2)
Tcircle ((0. (TOP-REAL 2)),1) is non empty strict TopSpace-like V245() SubSpace of TOP-REAL 2
Sphere ((0. (TOP-REAL 2)),1) is non empty closed V215( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
bool the carrier of (TOP-REAL 2) is set
(TOP-REAL 2) | (Sphere ((0. (TOP-REAL 2)),1)) is non empty strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of (Tunit_circle 2) is non empty set
[: the carrier of K605(), the carrier of (Tunit_circle 2):] is Relation-like set
bool [: the carrier of K605(), the carrier of (Tunit_circle 2):] is set
CircleMap is Relation-like the carrier of K605() -defined the carrier of K605() -defined the carrier of (Tunit_circle 2) -valued the carrier of (Tunit_circle 2) -valued Function-like non empty total total V18( the carrier of K605(), the carrier of (Tunit_circle 2)) V18( the carrier of K605(), the carrier of (Tunit_circle 2)) V19( the carrier of (Tunit_circle 2)) continuous Element of bool [: the carrier of K605(), the carrier of (Tunit_circle 2):]
c[10] is Element of the carrier of (Tunit_circle 2)
0 is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty ext-real non positive non negative ordinal natural complex complex-valued ext-real-valued real-valued natural-valued real V43() V44() finite finite-yielding V49() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V132() Function-yielding V156() V157() complex-functions-membered ext-real-functions-membered real-functions-membered rational-functions-membered integer-functions-membered natural-functions-membered complex-functions-valued ext-real-functions-valued real-functions-valued rational-functions-valued integer-functions-valued natural-functions-valued V267() V268() Element of NAT
{} is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty ext-real non positive non negative ordinal natural complex complex-valued ext-real-valued real-valued natural-valued real finite finite-yielding V49() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V132() Function-yielding V156() V157() complex-functions-membered ext-real-functions-membered real-functions-membered rational-functions-membered integer-functions-membered natural-functions-membered complex-functions-valued ext-real-functions-valued real-functions-valued rational-functions-valued integer-functions-valued natural-functions-valued V267() V268() set
the Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty ext-real non positive non negative ordinal natural complex complex-valued ext-real-valued real-valued natural-valued real finite finite-yielding V49() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V132() Function-yielding V156() V157() complex-functions-membered ext-real-functions-membered real-functions-membered rational-functions-membered integer-functions-membered natural-functions-membered complex-functions-valued ext-real-functions-valued real-functions-valued rational-functions-valued integer-functions-valued natural-functions-valued V267() V268() set is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty ext-real non positive non negative ordinal natural complex complex-valued ext-real-valued real-valued natural-valued real finite finite-yielding V49() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V132() Function-yielding V156() V157() complex-functions-membered ext-real-functions-membered real-functions-membered rational-functions-membered integer-functions-membered natural-functions-membered complex-functions-valued ext-real-functions-valued real-functions-valued rational-functions-valued integer-functions-valued natural-functions-valued V267() V268() set
|[1,0]| is Relation-like NAT -defined NAT -defined REAL -valued Function-like non empty complex-valued ext-real-valued real-valued finite 2 -element 2 -element FinSequence-like FinSubsequence-like V268() Element of the carrier of (TOP-REAL 2)
<*1*> is Relation-like NAT -defined Function-like one-to-one constant non empty trivial complex-valued ext-real-valued real-valued increasing decreasing non-decreasing non-increasing finite 1 -element FinSequence-like FinSubsequence-like V268() set
[1,1] is set
{1,1} is non empty finite V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{1} is non empty trivial finite V49() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{1,1},{1}} is non empty finite V49() set
{[1,1]} is Relation-like Function-like constant non empty trivial finite 1 -element V268() set
<*0*> is Relation-like NAT -defined Function-like one-to-one constant non empty trivial complex-valued ext-real-valued real-valued increasing decreasing non-decreasing non-increasing finite 1 -element FinSequence-like FinSubsequence-like Function-yielding V156() V157() V267() V268() set
[1,0] is set
{1,0} is non empty finite V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{1,0},{1}} is non empty finite V49() set
{[1,0]} is Relation-like Function-like constant non empty trivial finite 1 -element V268() set
<*1*> ^ <*0*> is Relation-like NAT -defined NAT -defined Function-like non empty complex-valued ext-real-valued real-valued finite K107(1,1) -element FinSequence-like FinSubsequence-like V268() set
K107(1,1) is non empty ext-real positive non negative ordinal natural complex real V43() V44() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
Topen_unit_circle c[10] is non empty strict TopSpace-like SubSpace of Tunit_circle 2
the carrier of (Topen_unit_circle c[10]) is non empty set
].0,1.[ is non empty complex-membered ext-real-membered real-membered open Element of bool REAL
R^1 ].0,1.[ is non empty complex-membered ext-real-membered real-membered open Element of bool the carrier of K605()
K605() | (R^1 ].0,1.[) is non empty strict TopSpace-like real-membered SubSpace of K605()
the carrier of (K605() | (R^1 ].0,1.[)) is non empty complex-membered ext-real-membered real-membered set
[: the carrier of (Topen_unit_circle c[10]), the carrier of (K605() | (R^1 ].0,1.[)):] is Relation-like complex-valued ext-real-valued real-valued set
bool [: the carrier of (Topen_unit_circle c[10]), the carrier of (K605() | (R^1 ].0,1.[)):] is set
c[-10] is Element of the carrier of (Tunit_circle 2)
K504(1) is non empty ext-real non positive negative complex real Element of REAL
|[K504(1),0]| is Relation-like NAT -defined NAT -defined REAL -valued Function-like non empty complex-valued ext-real-valued real-valued finite 2 -element 2 -element FinSequence-like FinSubsequence-like V268() Element of the carrier of (TOP-REAL 2)
<*K504(1)*> is Relation-like NAT -defined Function-like one-to-one constant non empty trivial complex-valued ext-real-valued real-valued increasing decreasing non-decreasing non-increasing finite 1 -element FinSequence-like FinSubsequence-like V268() set
[1,K504(1)] is set
{1,K504(1)} is non empty finite complex-membered ext-real-membered real-membered set
{{1,K504(1)},{1}} is non empty finite V49() set
{[1,K504(1)]} is Relation-like Function-like constant non empty trivial finite 1 -element V268() set
<*K504(1)*> ^ <*0*> is Relation-like NAT -defined NAT -defined Function-like non empty complex-valued ext-real-valued real-valued finite K107(1,1) -element FinSequence-like FinSubsequence-like V268() set
Topen_unit_circle c[-10] is non empty strict TopSpace-like SubSpace of Tunit_circle 2
the carrier of (Topen_unit_circle c[-10]) is non empty set
K513(1,2) is non empty ext-real positive non negative complex real Element of REAL
2 " is non empty ext-real positive non negative complex real set
1 * (2 ") is non empty ext-real positive non negative complex real set
3 is non empty ext-real positive non negative ordinal natural complex real V43() V44() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
K513(3,2) is non empty ext-real positive non negative complex real Element of REAL
3 * (2 ") is non empty ext-real positive non negative complex real set
].K513(1,2),K513(3,2).[ is non empty complex-membered ext-real-membered real-membered open Element of bool REAL
R^1 ].K513(1,2),K513(3,2).[ is non empty complex-membered ext-real-membered real-membered open Element of bool the carrier of K605()
K605() | (R^1 ].K513(1,2),K513(3,2).[) is non empty strict TopSpace-like real-membered SubSpace of K605()
the carrier of (K605() | (R^1 ].K513(1,2),K513(3,2).[)) is non empty complex-membered ext-real-membered real-membered set
[: the carrier of (Topen_unit_circle c[-10]), the carrier of (K605() | (R^1 ].K513(1,2),K513(3,2).[)):] is Relation-like complex-valued ext-real-valued real-valued set
bool [: the carrier of (Topen_unit_circle c[-10]), the carrier of (K605() | (R^1 ].K513(1,2),K513(3,2).[)):] is set
K759() is set
{{}} is functional non empty trivial finite V49() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered complex-functions-membered ext-real-functions-membered real-functions-membered set
{{}} * is functional non empty FinSequence-membered FinSequenceSet of {{}}
[:({{}} *),{{}}:] is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
bool [:({{}} *),{{}}:] is set
PFuncs (({{}} *),{{}}) is functional complex-functions-membered ext-real-functions-membered real-functions-membered rational-functions-membered integer-functions-membered natural-functions-membered set
[:COMPLEX,COMPLEX:] is Relation-like non trivial complex-valued non finite set
bool [:COMPLEX,COMPLEX:] is non trivial non finite set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is Relation-like non trivial complex-valued non finite set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non trivial non finite set
[:RAT,RAT:] is Relation-like RAT -valued non trivial complex-valued ext-real-valued real-valued non finite set
bool [:RAT,RAT:] is non trivial non finite set
[:[:RAT,RAT:],RAT:] is Relation-like RAT -valued non trivial complex-valued ext-real-valued real-valued non finite set
bool [:[:RAT,RAT:],RAT:] is non trivial non finite set
[:INT,INT:] is Relation-like RAT -valued INT -valued non trivial complex-valued ext-real-valued real-valued non finite set
bool [:INT,INT:] is non trivial non finite set
[:[:INT,INT:],INT:] is Relation-like RAT -valued INT -valued non trivial complex-valued ext-real-valued real-valued non finite set
bool [:[:INT,INT:],INT:] is non trivial non finite set
[:NAT,NAT:] is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
[:[:NAT,NAT:],NAT:] is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
bool [:[:NAT,NAT:],NAT:] is set
{{},1} is non empty finite V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
Euclid 0 is non empty V138() V139() strict Reflexive discerning V193() triangle MetrStruct
REAL 0 is functional non empty FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
0 -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL
REAL * is functional non empty FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V268() Element of REAL * : len b1 = 0 } is set
Pitag_dist 0 is Relation-like [:(REAL 0),(REAL 0):] -defined REAL -valued Function-like total V18([:(REAL 0),(REAL 0):], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[:(REAL 0),(REAL 0):],REAL:]
[:(REAL 0),(REAL 0):] is Relation-like set
[:[:(REAL 0),(REAL 0):],REAL:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:[:(REAL 0),(REAL 0):],REAL:] is set
MetrStruct(# (REAL 0),(Pitag_dist 0) #) is strict MetrStruct
TopSpaceMetr (Euclid 0) is trivial finite TopStruct
the carrier of (Euclid 0) is non empty set
Family_open_set (Euclid 0) is Element of bool (bool the carrier of (Euclid 0))
bool the carrier of (Euclid 0) is set
bool (bool the carrier of (Euclid 0)) is set
TopStruct(# the carrier of (Euclid 0),(Family_open_set (Euclid 0)) #) is non empty strict TopStruct
TOP-REAL 0 is non empty left_complementable right_complementable V138() V139() TopSpace-like Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed strict L16()
0. (TOP-REAL 0) is Relation-like non-empty empty-yielding NAT -defined REAL -valued Function-like one-to-one constant functional empty ext-real non positive non negative ordinal natural complex complex-valued ext-real-valued real-valued natural-valued real finite finite-yielding V49() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered zero complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V132() Function-yielding V156() V157() complex-functions-membered ext-real-functions-membered real-functions-membered rational-functions-membered integer-functions-membered natural-functions-membered complex-functions-valued ext-real-functions-valued real-functions-valued rational-functions-valued integer-functions-valued natural-functions-valued V267() V268() Element of the carrier of (TOP-REAL 0)
the carrier of (TOP-REAL 0) is non empty set
the ZeroF of (TOP-REAL 0) is Relation-like non-empty empty-yielding NAT -defined REAL -valued Function-like one-to-one constant functional empty ext-real non positive non negative ordinal natural complex complex-valued ext-real-valued real-valued natural-valued real finite finite-yielding V49() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V132() Function-yielding V156() V157() complex-functions-membered ext-real-functions-membered real-functions-membered rational-functions-membered integer-functions-membered natural-functions-membered complex-functions-valued ext-real-functions-valued real-functions-valued rational-functions-valued integer-functions-valued natural-functions-valued V267() V268() Element of the carrier of (TOP-REAL 0)
{(0. (TOP-REAL 0))} is functional non empty trivial finite V49() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered complex-functions-membered ext-real-functions-membered real-functions-membered set
the carrier of R^1 is non empty complex-membered ext-real-membered real-membered set
sqrt 0 is ext-real non negative complex real Element of REAL
<*> REAL is Relation-like non-empty empty-yielding NAT -defined REAL -valued Function-like one-to-one constant functional empty ext-real non positive non negative ordinal natural complex complex-valued ext-real-valued real-valued natural-valued real finite finite-yielding V49() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V132() Function-yielding V156() V157() complex-functions-membered ext-real-functions-membered real-functions-membered rational-functions-membered integer-functions-membered natural-functions-membered complex-functions-valued ext-real-functions-valued real-functions-valued rational-functions-valued integer-functions-valued natural-functions-valued V267() V268() FinSequence of REAL
Sum (<*> REAL) is ext-real complex real Element of REAL
m is trivial finite set
r is set
card m is ext-real non negative ordinal natural complex real V43() V44() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of omega
card r is ordinal cardinal set
m is ext-real complex real set
m ^2 is ext-real complex real set
m * m is ext-real non negative complex real set
m is non empty ext-real positive non negative complex real set
m ^2 is ext-real non negative complex real set
m * m is non empty ext-real positive non negative complex real set
m is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty ext-real non positive non negative ordinal natural complex complex-valued ext-real-valued real-valued natural-valued real finite finite-yielding V49() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V132() Function-yielding V156() V157() complex-functions-membered ext-real-functions-membered real-functions-membered rational-functions-membered integer-functions-membered natural-functions-membered complex-functions-valued ext-real-functions-valued real-functions-valued rational-functions-valued integer-functions-valued natural-functions-valued V267() V268() set
sqr m is Relation-like non-empty empty-yielding NAT -defined REAL -valued RAT -valued Function-like one-to-one constant functional empty ext-real non positive non negative ordinal natural complex complex-valued ext-real-valued real-valued natural-valued real finite finite-yielding V49() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V132() Function-yielding V156() V157() complex-functions-membered ext-real-functions-membered real-functions-membered rational-functions-membered integer-functions-membered natural-functions-membered complex-functions-valued ext-real-functions-valued real-functions-valued rational-functions-valued integer-functions-valued natural-functions-valued V267() V268() FinSequence of REAL
m (#) m is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty ext-real non positive non negative ordinal natural complex complex-valued ext-real-valued real-valued natural-valued real finite finite-yielding V49() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V132() Function-yielding V156() V157() complex-functions-membered ext-real-functions-membered real-functions-membered rational-functions-membered integer-functions-membered natural-functions-membered complex-functions-valued ext-real-functions-valued real-functions-valued rational-functions-valued integer-functions-valued natural-functions-valued V267() V268() set
K857() is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like total V18([:REAL,REAL:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]
K857() .: (m,m) is Relation-like Function-like set
<:m,m:> is Relation-like Function-like set
<:m,m:> (#) K857() is Relation-like REAL -valued Function-like complex-valued ext-real-valued real-valued set
sqrreal is Relation-like REAL -defined REAL -valued Function-like non empty total V18( REAL , REAL ) complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
m (#) sqrreal is Relation-like non-empty empty-yielding NAT -defined REAL -valued RAT -valued Function-like one-to-one constant functional empty ext-real non positive non negative ordinal natural complex complex-valued ext-real-valued real-valued natural-valued real finite finite-yielding V49() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V132() Function-yielding V156() V157() complex-functions-membered ext-real-functions-membered real-functions-membered rational-functions-membered integer-functions-membered natural-functions-membered complex-functions-valued ext-real-functions-valued real-functions-valued rational-functions-valued integer-functions-valued natural-functions-valued V267() V268() set
|.m.| is ext-real non negative complex real Element of REAL
Sum (sqr m) is ext-real complex real Element of REAL
sqrt (Sum (sqr m)) is ext-real complex real Element of REAL
m is complex set
r is complex set
m + r is complex set
T is Relation-like Function-like complex-valued set
(m + r) (#) T is Relation-like Function-like complex-valued set
m (#) T is Relation-like Function-like complex-valued set
r (#) T is Relation-like Function-like complex-valued set
(m (#) T) + (r (#) T) is Relation-like Function-like complex-valued set
dom ((m + r) (#) T) is set
dom T is set
dom (m (#) T) is set
dom (r (#) T) is set
dom ((m (#) T) + (r (#) T)) is set
(dom (m (#) T)) /\ (dom (r (#) T)) is set
f is set
((m + r) (#) T) . f is complex set
((m (#) T) + (r (#) T)) . f is complex set
T . f is complex set
(T . f) * (m + r) is complex set
(T . f) * m is complex set
(T . f) * r is complex set
((T . f) * m) + ((T . f) * r) is complex set
(m (#) T) . f is complex set
((m (#) T) . f) + ((T . f) * r) is complex set
(r (#) T) . f is complex set
((m (#) T) . f) + ((r (#) T) . f) is complex set
m is complex set
r is complex set
m - r is complex set
- r is complex set
m + (- r) is complex set
T is Relation-like Function-like complex-valued set
(m - r) (#) T is Relation-like Function-like complex-valued set
m (#) T is Relation-like Function-like complex-valued set
r (#) T is Relation-like Function-like complex-valued set
(m (#) T) - (r (#) T) is Relation-like Function-like complex-valued set
- (r (#) T) is Relation-like Function-like complex-valued set
- 1 is non empty ext-real non positive negative complex real set
(- 1) (#) (r (#) T) is Relation-like Function-like complex-valued set
(m (#) T) + (- (r (#) T)) is Relation-like Function-like complex-valued set
(- r) (#) T is Relation-like Function-like complex-valued set
(m (#) T) + ((- r) (#) T) is Relation-like Function-like complex-valued set
m is complex set
r is Relation-like Function-like complex-valued set
r (/) m is Relation-like Function-like complex-valued set
1 / m is complex set
m " is complex set
1 * (m ") is complex set
(1 / m) (#) r is Relation-like Function-like complex-valued set
T is Relation-like Function-like complex-valued set
T (/) m is Relation-like Function-like complex-valued set
(1 / m) (#) T is Relation-like Function-like complex-valued set
(r (/) m) + (T (/) m) is Relation-like Function-like complex-valued set
r + T is Relation-like Function-like complex-valued set
(r + T) (/) m is Relation-like Function-like complex-valued set
(1 / m) (#) (r + T) is Relation-like Function-like complex-valued set
dom ((r (/) m) + (T (/) m)) is set
dom (r (/) m) is set
dom (T (/) m) is set
(dom (r (/) m)) /\ (dom (T (/) m)) is set
dom r is set
dom T is set
dom ((r + T) (/) m) is set
dom (r + T) is set
(dom r) /\ (dom T) is set
f is set
((r (/) m) + (T (/) m)) . f is complex set
((r + T) (/) m) . f is complex set
(r + T) . f is complex set
((r + T) . f) / m is complex Element of COMPLEX
((r + T) . f) * (m ") is complex set
r . f is complex set
T . f is complex set
(r . f) + (T . f) is complex set
((r . f) + (T . f)) / m is complex Element of COMPLEX
((r . f) + (T . f)) * (m ") is complex set
(r . f) / m is complex Element of COMPLEX
(r . f) * (m ") is complex set
(T . f) / m is complex Element of COMPLEX
(T . f) * (m ") is complex set
((r . f) / m) + ((T . f) / m) is complex Element of COMPLEX
(T (/) m) . f is complex set
((r . f) / m) + ((T (/) m) . f) is complex set
(r (/) m) . f is complex set
((r (/) m) . f) + ((T (/) m) . f) is complex set
m is complex set
r is Relation-like Function-like complex-valued set
r (/) m is Relation-like Function-like complex-valued set
1 / m is complex set
m " is complex set
1 * (m ") is complex set
(1 / m) (#) r is Relation-like Function-like complex-valued set
T is Relation-like Function-like complex-valued set
T (/) m is Relation-like Function-like complex-valued set
(1 / m) (#) T is Relation-like Function-like complex-valued set
(r (/) m) - (T (/) m) is Relation-like Function-like complex-valued set
- (T (/) m) is Relation-like Function-like complex-valued set
- 1 is non empty ext-real non positive negative complex real set
(- 1) (#) (T (/) m) is Relation-like Function-like complex-valued set
(r (/) m) + (- (T (/) m)) is Relation-like Function-like complex-valued set
r - T is Relation-like Function-like complex-valued set
- T is Relation-like Function-like complex-valued set
(- 1) (#) T is Relation-like Function-like complex-valued set
r + (- T) is Relation-like Function-like complex-valued set
(r - T) (/) m is Relation-like Function-like complex-valued set
(1 / m) (#) (r - T) is Relation-like Function-like complex-valued set
(- T) (/) m is Relation-like Function-like complex-valued set
(1 / m) (#) (- T) is Relation-like Function-like complex-valued set
(r (/) m) + ((- T) (/) m) is Relation-like Function-like complex-valued set
m is complex set
r is complex set
m * r is complex set
T is Relation-like Function-like complex-valued set
T (/) m is Relation-like Function-like complex-valued set
1 / m is complex set
m " is complex set
1 * (m ") is complex set
(1 / m) (#) T is Relation-like Function-like complex-valued set
r (#) T is Relation-like Function-like complex-valued set
f is Relation-like Function-like complex-valued set
f (/) r is Relation-like Function-like complex-valued set
1 / r is complex set
r " is complex set
1 * (r ") is complex set
(1 / r) (#) f is Relation-like Function-like complex-valued set
(T (/) m) - (f (/) r) is Relation-like Function-like complex-valued set
- (f (/) r) is Relation-like Function-like complex-valued set
- 1 is non empty ext-real non positive negative complex real set
(- 1) (#) (f (/) r) is Relation-like Function-like complex-valued set
(T (/) m) + (- (f (/) r)) is Relation-like Function-like complex-valued set
m (#) f is Relation-like Function-like complex-valued set
(r (#) T) - (m (#) f) is Relation-like Function-like complex-valued set
- (m (#) f) is Relation-like Function-like complex-valued set
(- 1) (#) (m (#) f) is Relation-like Function-like complex-valued set
(r (#) T) + (- (m (#) f)) is Relation-like Function-like complex-valued set
((r (#) T) - (m (#) f)) (/) (m * r) is Relation-like Function-like complex-valued set
1 / (m * r) is complex set
(m * r) " is complex set
1 * ((m * r) ") is complex set
(1 / (m * r)) (#) ((r (#) T) - (m (#) f)) is Relation-like Function-like complex-valued set
dom (T (/) m) is set
dom T is set
dom (f (/) r) is set
dom f is set
dom (r (#) T) is set
dom (m (#) f) is set
dom ((T (/) m) - (f (/) r)) is set
(dom (T (/) m)) /\ (dom (f (/) r)) is set
dom ((r (#) T) - (m (#) f)) is set
(dom (r (#) T)) /\ (dom (m (#) f)) is set
dom (((r (#) T) - (m (#) f)) (/) (m * r)) is set
g is set
((T (/) m) - (f (/) r)) . g is complex set
(((r (#) T) - (m (#) f)) (/) (m * r)) . g is complex set
(T (/) m) . g is complex set
(f (/) r) . g is complex set
((T (/) m) . g) - ((f (/) r) . g) is complex set
- ((f (/) r) . g) is complex set
((T (/) m) . g) + (- ((f (/) r) . g)) is complex set
T . g is complex set
(T . g) / m is complex Element of COMPLEX
(T . g) * (m ") is complex set
((T . g) / m) - ((f (/) r) . g) is complex set
((T . g) / m) + (- ((f (/) r) . g)) is complex set
f . g is complex set
(f . g) / r is complex Element of COMPLEX
(f . g) * (r ") is complex set
((T . g) / m) - ((f . g) / r) is complex Element of COMPLEX
- ((f . g) / r) is complex set
((T . g) / m) + (- ((f . g) / r)) is complex set
(T . g) * r is complex set
(f . g) * m is complex set
((T . g) * r) - ((f . g) * m) is complex set
- ((f . g) * m) is complex set
((T . g) * r) + (- ((f . g) * m)) is complex set
(((T . g) * r) - ((f . g) * m)) / (m * r) is complex Element of COMPLEX
(((T . g) * r) - ((f . g) * m)) * ((m * r) ") is complex set
(m (#) f) . g is complex set
((T . g) * r) - ((m (#) f) . g) is complex set
- ((m (#) f) . g) is complex set
((T . g) * r) + (- ((m (#) f) . g)) is complex set
(((T . g) * r) - ((m (#) f) . g)) / (m * r) is complex Element of COMPLEX
(((T . g) * r) - ((m (#) f) . g)) * ((m * r) ") is complex set
(r (#) T) . g is complex set
((r (#) T) . g) - ((m (#) f) . g) is complex set
((r (#) T) . g) + (- ((m (#) f) . g)) is complex set
(((r (#) T) . g) - ((m (#) f) . g)) / (m * r) is complex Element of COMPLEX
(((r (#) T) . g) - ((m (#) f) . g)) * ((m * r) ") is complex set
((r (#) T) - (m (#) f)) . g is complex set
(((r (#) T) - (m (#) f)) . g) / (m * r) is complex Element of COMPLEX
(((r (#) T) - (m (#) f)) . g) * ((m * r) ") is complex set
m is complex set
r is Relation-like Function-like complex-valued set
r (/) m is Relation-like Function-like complex-valued set
1 / m is complex set
m " is complex set
1 * (m ") is complex set
(1 / m) (#) r is Relation-like Function-like complex-valued set
T is Relation-like Function-like complex-valued set
(r (/) m) - T is Relation-like Function-like complex-valued set
- T is Relation-like Function-like complex-valued set
- 1 is non empty ext-real non positive negative complex real set
(- 1) (#) T is Relation-like Function-like complex-valued set
(r (/) m) + (- T) is Relation-like Function-like complex-valued set
m (#) T is Relation-like Function-like complex-valued set
r - (m (#) T) is Relation-like Function-like complex-valued set
- (m (#) T) is Relation-like Function-like complex-valued set
(- 1) (#) (m (#) T) is Relation-like Function-like complex-valued set
r + (- (m (#) T)) is Relation-like Function-like complex-valued set
(r - (m (#) T)) (/) m is Relation-like Function-like complex-valued set
(1 / m) (#) (r - (m (#) T)) is Relation-like Function-like complex-valued set
dom ((r (/) m) - T) is set
dom (r (/) m) is set
dom T is set
(dom (r (/) m)) /\ (dom T) is set
dom r is set
(dom r) /\ (dom T) is set
dom (r - (m (#) T)) is set
dom (m (#) T) is set
(dom r) /\ (dom (m (#) T)) is set
dom ((r - (m (#) T)) (/) m) is set
f is set
((r (/) m) - T) . f is complex set
((r - (m (#) T)) (/) m) . f is complex set
(r (/) m) . f is complex set
T . f is complex set
((r (/) m) . f) - (T . f) is complex set
- (T . f) is complex set
((r (/) m) . f) + (- (T . f)) is complex set
r . f is complex set
(r . f) / m is complex Element of COMPLEX
(r . f) * (m ") is complex set
((r . f) / m) - (T . f) is complex set
((r . f) / m) + (- (T . f)) is complex set
m * (T . f) is complex set
(m * (T . f)) / m is complex Element of COMPLEX
(m * (T . f)) * (m ") is complex set
((r . f) / m) - ((m * (T . f)) / m) is complex Element of COMPLEX
- ((m * (T . f)) / m) is complex set
((r . f) / m) + (- ((m * (T . f)) / m)) is complex set
(m (#) T) . f is complex set
((m (#) T) . f) / m is complex Element of COMPLEX
((m (#) T) . f) * (m ") is complex set
((r . f) / m) - (((m (#) T) . f) / m) is complex Element of COMPLEX
- (((m (#) T) . f) / m) is complex set
((r . f) / m) + (- (((m (#) T) . f) / m)) is complex set
(r . f) - ((m (#) T) . f) is complex set
- ((m (#) T) . f) is complex set
(r . f) + (- ((m (#) T) . f)) is complex set
((r . f) - ((m (#) T) . f)) / m is complex Element of COMPLEX
((r . f) - ((m (#) T) . f)) * (m ") is complex set
(r - (m (#) T)) . f is complex set
((r - (m (#) T)) . f) / m is complex Element of COMPLEX
((r - (m (#) T)) . f) * (m ") is complex set
m is complex set
r is complex set
m - r is complex set
- r is complex set
m + (- r) is complex set
T is Relation-like Function-like complex-valued set
(m - r) (#) T is Relation-like Function-like complex-valued set
m (#) T is Relation-like Function-like complex-valued set
r (#) T is Relation-like Function-like complex-valued set
(m (#) T) - (r (#) T) is Relation-like Function-like complex-valued set
- (r (#) T) is Relation-like Function-like complex-valued set
- 1 is non empty ext-real non positive negative complex real set
(- 1) (#) (r (#) T) is Relation-like Function-like complex-valued set
(m (#) T) + (- (r (#) T)) is Relation-like Function-like complex-valued set
dom ((m (#) T) - (r (#) T)) is set
dom (m (#) T) is set
dom (r (#) T) is set
(dom (m (#) T)) /\ (dom (r (#) T)) is set
dom T is set
(dom T) /\ (dom (r (#) T)) is set
(dom T) /\ (dom T) is set
dom ((m - r) (#) T) is set
f is set
((m - r) (#) T) . f is complex set
((m (#) T) - (r (#) T)) . f is complex set
T . f is complex set
(m - r) * (T . f) is complex set
m * (T . f) is complex set
r * (T . f) is complex set
(m * (T . f)) - (r * (T . f)) is complex set
- (r * (T . f)) is complex set
(m * (T . f)) + (- (r * (T . f))) is complex set
(r (#) T) . f is complex set
(m * (T . f)) - ((r (#) T) . f) is complex set
- ((r (#) T) . f) is complex set
(m * (T . f)) + (- ((r (#) T) . f)) is complex set
(m (#) T) . f is complex set
((m (#) T) . f) - ((r (#) T) . f) is complex set
((m (#) T) . f) + (- ((r (#) T) . f)) is complex set
m is Relation-like Function-like complex-valued set
r is Relation-like Function-like complex-valued set
m - r is Relation-like Function-like complex-valued set
- r is Relation-like Function-like complex-valued set
- 1 is non empty ext-real non positive negative complex real set
(- 1) (#) r is Relation-like Function-like complex-valued set
m + (- r) is Relation-like Function-like complex-valued set
(m - r) ^2 is Relation-like Function-like complex-valued set
(m - r) (#) (m - r) is Relation-like Function-like complex-valued set
r - m is Relation-like Function-like complex-valued set
- m is Relation-like Function-like complex-valued set
(- 1) (#) m is Relation-like Function-like complex-valued set
r + (- m) is Relation-like Function-like complex-valued set
(r - m) ^2 is Relation-like Function-like complex-valued set
(r - m) (#) (r - m) is Relation-like Function-like complex-valued set
dom (m - r) is set
dom m is set
dom r is set
(dom m) /\ (dom r) is set
dom (r - m) is set
(dom r) /\ (dom m) is set
dom ((m - r) ^2) is set
dom ((r - m) ^2) is set
T is set
((m - r) ^2) . T is complex set
((r - m) ^2) . T is complex set
(m - r) . T is complex set
m . T is complex set
r . T is complex set
(m . T) - (r . T) is complex set
- (r . T) is complex set
(m . T) + (- (r . T)) is complex set
(r - m) . T is complex set
(r . T) - (m . T) is complex set
- (m . T) is complex set
(r . T) + (- (m . T)) is complex set
((m - r) . T) * ((m - r) . T) is complex set
((r - m) . T) * ((r - m) . T) is complex set
m is complex set
m ^2 is complex set
m * m is complex set
r is Relation-like Function-like complex-valued set
r (/) m is Relation-like Function-like complex-valued set
1 / m is complex set
m " is complex set
1 * (m ") is complex set
(1 / m) (#) r is Relation-like Function-like complex-valued set
(r (/) m) ^2 is Relation-like Function-like complex-valued set
(r (/) m) (#) (r (/) m) is Relation-like Function-like complex-valued set
r ^2 is Relation-like Function-like complex-valued set
r (#) r is Relation-like Function-like complex-valued set
(r ^2) (/) (m ^2) is Relation-like Function-like complex-valued set
1 / (m ^2) is complex set
(m ^2) " is complex set
1 * ((m ^2) ") is complex set
(1 / (m ^2)) (#) (r ^2) is Relation-like Function-like complex-valued set
dom ((r (/) m) ^2) is set
dom (r (/) m) is set
dom r is set
dom (r ^2) is set
dom ((r ^2) (/) (m ^2)) is set
T is set
((r (/) m) ^2) . T is complex set
((r ^2) (/) (m ^2)) . T is complex set
(r (/) m) . T is complex set
((r (/) m) . T) ^2 is complex set
((r (/) m) . T) * ((r (/) m) . T) is complex set
r . T is complex set
(r . T) / m is complex Element of COMPLEX
(r . T) * (m ") is complex set
((r . T) / m) ^2 is complex Element of COMPLEX
((r . T) / m) * ((r . T) / m) is complex set
(r . T) ^2 is complex set
(r . T) * (r . T) is complex set
((r . T) ^2) / (m ^2) is complex Element of COMPLEX
((r . T) ^2) * ((m ^2) ") is complex set
(r ^2) . T is complex set
((r ^2) . T) / (m ^2) is complex Element of COMPLEX
((r ^2) . T) * ((m ^2) ") is complex set
m is ext-real non negative ordinal natural complex real finite cardinal set
sqrt m is ext-real non negative complex real set
r is ext-real complex real set
m |-> r is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite m -element FinSequence-like FinSubsequence-like V268() set
Seg m is finite m -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
{ b1 where b1 is ext-real non negative ordinal natural complex real V43() V44() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT : ( 1 <= b1 & b1 <= m ) } is set
(Seg m) --> r is Relation-like Seg m -defined Seg m -defined {r} -valued Function-like constant total total V18( Seg m,{r}) complex-valued ext-real-valued real-valued finite FinSequence-like FinSubsequence-like V268() Element of bool [:(Seg m),{r}:]
{r} is non empty trivial finite 1 -element complex-membered ext-real-membered real-membered set
[:(Seg m),{r}:] is Relation-like complex-valued ext-real-valued real-valued finite set
bool [:(Seg m),{r}:] is finite V49() set
T is ext-real complex real set
m |-> T is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite m -element FinSequence-like FinSubsequence-like V268() set
(Seg m) --> T is Relation-like Seg m -defined Seg m -defined {T} -valued Function-like constant total total V18( Seg m,{T}) complex-valued ext-real-valued real-valued finite FinSequence-like FinSubsequence-like V268() Element of bool [:(Seg m),{T}:]
{T} is non empty trivial finite 1 -element complex-membered ext-real-membered real-membered set
[:(Seg m),{T}:] is Relation-like complex-valued ext-real-valued real-valued finite set
bool [:(Seg m),{T}:] is finite V49() set
(m |-> r) - (m |-> T) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite m -element FinSequence-like FinSubsequence-like V268() FinSequence of REAL
- (m |-> T) is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite m -element FinSequence-like FinSubsequence-like V268() set
- 1 is non empty ext-real non positive negative complex real set
(- 1) (#) (m |-> T) is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite m -element FinSequence-like FinSubsequence-like V268() set
K260((- 1)) is Relation-like REAL -defined REAL -valued Function-like non empty total V18( REAL , REAL ) complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
id REAL is Relation-like REAL -defined REAL -valued Function-like one-to-one non empty total V18( REAL , REAL ) complex-valued ext-real-valued real-valued increasing non-decreasing Element of bool [:REAL,REAL:]
K857() [;] ((- 1),(id REAL)) is Relation-like Function-like set
dom (id REAL) is non empty set
(dom (id REAL)) --> (- 1) is Relation-like non-empty dom (id REAL) -defined Function-like constant non empty total complex-valued ext-real-valued real-valued V315() V316() set
{(- 1)} is non empty trivial finite 1 -element complex-membered ext-real-membered real-membered set
[:(dom (id REAL)),{(- 1)}:] is Relation-like complex-valued ext-real-valued real-valued set
<:((dom (id REAL)) --> (- 1)),(id REAL):> is Relation-like Function-like set
<:((dom (id REAL)) --> (- 1)),(id REAL):> (#) K857() is Relation-like REAL -valued Function-like complex-valued ext-real-valued real-valued set
(m |-> T) (#) K260((- 1)) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite FinSequence-like FinSubsequence-like V268() set
K853() is Relation-like REAL -defined REAL -valued Function-like non empty total V18( REAL , REAL ) complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(m |-> T) (#) K853() is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite FinSequence-like FinSubsequence-like V268() set
(m |-> r) + (- (m |-> T)) is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite m -element FinSequence-like FinSubsequence-like V268() set
K855() is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like total V18([:REAL,REAL:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]
K855() .: ((m |-> r),(- (m |-> T))) is Relation-like Function-like set
<:(m |-> r),(- (m |-> T)):> is Relation-like Function-like set
<:(m |-> r),(- (m |-> T)):> (#) K855() is Relation-like REAL -valued Function-like complex-valued ext-real-valued real-valued set
K856() is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like total V18([:REAL,REAL:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]
K342(REAL,K855(),(id REAL),K853()) is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like total V18([:REAL,REAL:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]
K856() .: ((m |-> r),(m |-> T)) is Relation-like Function-like set
<:(m |-> r),(m |-> T):> is Relation-like Function-like set
<:(m |-> r),(m |-> T):> (#) K856() is Relation-like REAL -valued Function-like complex-valued ext-real-valued real-valued set
|.((m |-> r) - (m |-> T)).| is ext-real non negative complex real Element of REAL
sqr ((m |-> r) - (m |-> T)) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite m -element FinSequence-like FinSubsequence-like V268() FinSequence of REAL
((m |-> r) - (m |-> T)) (#) ((m |-> r) - (m |-> T)) is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite m -element FinSequence-like FinSubsequence-like V268() V317() set
K857() .: (((m |-> r) - (m |-> T)),((m |-> r) - (m |-> T))) is Relation-like Function-like set
<:((m |-> r) - (m |-> T)),((m |-> r) - (m |-> T)):> is Relation-like Function-like set
<:((m |-> r) - (m |-> T)),((m |-> r) - (m |-> T)):> (#) K857() is Relation-like REAL -valued Function-like complex-valued ext-real-valued real-valued set
((m |-> r) - (m |-> T)) (#) sqrreal is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite FinSequence-like FinSubsequence-like V268() set
Sum (sqr ((m |-> r) - (m |-> T))) is ext-real complex real Element of REAL
sqrt (Sum (sqr ((m |-> r) - (m |-> T)))) is ext-real complex real Element of REAL
r - T is ext-real complex real set
- T is ext-real complex real set
r + (- T) is ext-real complex real set
abs (r - T) is ext-real complex real Element of REAL
(sqrt m) * (abs (r - T)) is ext-real complex real set
m |-> (r - T) is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite m -element FinSequence-like FinSubsequence-like V268() set
(Seg m) --> (r - T) is Relation-like Seg m -defined Seg m -defined {(r - T)} -valued Function-like constant total total V18( Seg m,{(r - T)}) complex-valued ext-real-valued real-valued finite FinSequence-like FinSubsequence-like V268() Element of bool [:(Seg m),{(r - T)}:]
{(r - T)} is non empty trivial finite 1 -element complex-membered ext-real-membered real-membered set
[:(Seg m),{(r - T)}:] is Relation-like complex-valued ext-real-valued real-valued finite set
bool [:(Seg m),{(r - T)}:] is finite V49() set
sqr (m |-> (r - T)) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite m -element FinSequence-like FinSubsequence-like V268() FinSequence of REAL
(m |-> (r - T)) (#) (m |-> (r - T)) is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite m -element FinSequence-like FinSubsequence-like V268() set
K857() .: ((m |-> (r - T)),(m |-> (r - T))) is Relation-like Function-like set
<:(m |-> (r - T)),(m |-> (r - T)):> is Relation-like Function-like set
<:(m |-> (r - T)),(m |-> (r - T)):> (#) K857() is Relation-like REAL -valued Function-like complex-valued ext-real-valued real-valued set
(m |-> (r - T)) (#) sqrreal is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite FinSequence-like FinSubsequence-like V268() set
Sum (sqr (m |-> (r - T))) is ext-real complex real Element of REAL
sqrt (Sum (sqr (m |-> (r - T)))) is ext-real complex real Element of REAL
(r - T) ^2 is ext-real non negative complex real set
(r - T) * (r - T) is ext-real non negative complex real set
m |-> ((r - T) ^2) is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite m -element FinSequence-like FinSubsequence-like V268() set
(Seg m) --> ((r - T) ^2) is Relation-like Seg m -defined Seg m -defined {((r - T) ^2)} -valued Function-like constant total total V18( Seg m,{((r - T) ^2)}) complex-valued ext-real-valued real-valued finite FinSequence-like FinSubsequence-like V268() V317() Element of bool [:(Seg m),{((r - T) ^2)}:]
{((r - T) ^2)} is non empty trivial finite 1 -element complex-membered ext-real-membered real-membered set
[:(Seg m),{((r - T) ^2)}:] is Relation-like complex-valued ext-real-valued real-valued finite set
bool [:(Seg m),{((r - T) ^2)}:] is finite V49() set
Sum (m |-> ((r - T) ^2)) is ext-real complex real set
sqrt (Sum (m |-> ((r - T) ^2))) is ext-real complex real set
m * ((r - T) ^2) is ext-real non negative complex real set
sqrt (m * ((r - T) ^2)) is ext-real non negative complex real set
sqrt ((r - T) ^2) is ext-real non negative complex real set
(sqrt m) * (sqrt ((r - T) ^2)) is ext-real non negative complex real set
m is Relation-like Function-like complex-valued set
r is set
T is complex set
m +* (r,T) is Relation-like Function-like set
g is set
dom (m +* (r,T)) is set
(m +* (r,T)) . g is set
dom m is set
dom m is set
m . g is complex set
dom m is set
m . g is complex set
dom m is set
m is set
r is ext-real non negative ordinal natural complex real finite cardinal set
0* r is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite r -element FinSequence-like FinSubsequence-like V268() Element of REAL r
REAL r is functional non empty FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
r -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V268() Element of REAL * : len b1 = r } is set
r |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite r -element FinSequence-like FinSubsequence-like V268() Element of r -tuples_on REAL
Seg r is finite r -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
{ b1 where b1 is ext-real non negative ordinal natural complex real V43() V44() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT : ( 1 <= b1 & b1 <= r ) } is set
(Seg r) --> 0 is Relation-like Seg r -defined Seg r -defined RAT -valued INT -valued {0} -valued Function-like constant total total V18( Seg r,{0}) complex-valued ext-real-valued real-valued natural-valued finite FinSequence-like FinSubsequence-like Function-yielding V156() complex-functions-valued ext-real-functions-valued real-functions-valued V268() V316() V317() Element of bool [:(Seg r),{0}:]
{0} is functional non empty trivial finite V49() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered complex-functions-membered ext-real-functions-membered real-functions-membered set
[:(Seg r),{0}:] is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued finite set
bool [:(Seg r),{0}:] is finite V49() set
T is complex set
(0* r) +* (m,T) is Relation-like NAT -defined Function-like complex-valued finite r -element FinSequence-like FinSubsequence-like V268() set
((0* r) +* (m,T)) ^2 is Relation-like NAT -defined Function-like complex-valued finite r -element FinSequence-like FinSubsequence-like V268() set
((0* r) +* (m,T)) (#) ((0* r) +* (m,T)) is Relation-like NAT -defined Function-like complex-valued finite r -element FinSequence-like FinSubsequence-like V268() set
T ^2 is complex set
T * T is complex set
(0* r) +* (m,(T ^2)) is Relation-like NAT -defined Function-like complex-valued finite r -element FinSequence-like FinSubsequence-like V268() set
dom ((0* r) +* (m,T)) is finite r -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
dom (0* r) is finite r -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
dom ((0* r) +* (m,(T ^2))) is finite r -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
dom (((0* r) +* (m,T)) ^2) is finite r -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
dom (((0* r) +* (m,T)) ^2) is finite r -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
p is set
(((0* r) +* (m,T)) ^2) . p is complex set
((0* r) +* (m,(T ^2))) . p is complex set
((0* r) +* (m,T)) . p is complex set
(((0* r) +* (m,T)) . p) ^2 is complex set
(((0* r) +* (m,T)) . p) * (((0* r) +* (m,T)) . p) is complex set
(r |-> 0) . p is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty ext-real non positive non negative ordinal natural complex complex-valued ext-real-valued real-valued natural-valued real finite finite-yielding V49() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V132() Function-yielding V156() V157() complex-functions-membered ext-real-functions-membered real-functions-membered rational-functions-membered integer-functions-membered natural-functions-membered complex-functions-valued ext-real-functions-valued real-functions-valued rational-functions-valued integer-functions-valued natural-functions-valued V267() V268() set
{} . m is Relation-like non-empty empty-yielding NAT -defined RAT -valued INT -valued Function-like one-to-one constant functional empty ext-real non positive non negative ordinal natural complex complex-valued ext-real-valued real-valued natural-valued real V44() finite finite-yielding V49() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V132() Function-yielding V156() V157() complex-functions-membered ext-real-functions-membered real-functions-membered rational-functions-membered integer-functions-membered natural-functions-membered complex-functions-valued ext-real-functions-valued real-functions-valued rational-functions-valued integer-functions-valued natural-functions-valued V267() V268() set
m is set
r is ext-real non negative ordinal natural complex real finite cardinal set
Seg r is finite r -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
{ b1 where b1 is ext-real non negative ordinal natural complex real V43() V44() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT : ( 1 <= b1 & b1 <= r ) } is set
0* r is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite r -element FinSequence-like FinSubsequence-like V268() Element of REAL r
REAL r is functional non empty FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
r -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V268() Element of REAL * : len b1 = r } is set
r |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite r -element FinSequence-like FinSubsequence-like V268() Element of r -tuples_on REAL
(Seg r) --> 0 is Relation-like Seg r -defined Seg r -defined RAT -valued INT -valued {0} -valued Function-like constant total total V18( Seg r,{0}) complex-valued ext-real-valued real-valued natural-valued finite FinSequence-like FinSubsequence-like Function-yielding V156() complex-functions-valued ext-real-functions-valued real-functions-valued V268() V316() V317() Element of bool [:(Seg r),{0}:]
{0} is functional non empty trivial finite V49() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered complex-functions-membered ext-real-functions-membered real-functions-membered set
[:(Seg r),{0}:] is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued finite set
bool [:(Seg r),{0}:] is finite V49() set
T is ext-real complex real set
(0* r) +* (m,T) is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite r -element FinSequence-like FinSubsequence-like V268() set
|.((0* r) +* (m,T)).| is ext-real non negative complex real Element of REAL
sqr ((0* r) +* (m,T)) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite r -element FinSequence-like FinSubsequence-like V268() FinSequence of REAL
((0* r) +* (m,T)) (#) ((0* r) +* (m,T)) is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite r -element FinSequence-like FinSubsequence-like V268() set
K857() .: (((0* r) +* (m,T)),((0* r) +* (m,T))) is Relation-like Function-like set
<:((0* r) +* (m,T)),((0* r) +* (m,T)):> is Relation-like Function-like set
<:((0* r) +* (m,T)),((0* r) +* (m,T)):> (#) K857() is Relation-like REAL -valued Function-like complex-valued ext-real-valued real-valued set
((0* r) +* (m,T)) (#) sqrreal is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite FinSequence-like FinSubsequence-like V268() set
Sum (sqr ((0* r) +* (m,T))) is ext-real complex real Element of REAL
sqrt (Sum (sqr ((0* r) +* (m,T)))) is ext-real complex real Element of REAL
abs T is ext-real complex real Element of REAL
T ^2 is ext-real non negative complex real set
T * T is ext-real non negative complex real set
((0* r) +* (m,T)) ^2 is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite r -element FinSequence-like FinSubsequence-like V268() set
(0* r) +* (m,(T ^2)) is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite r -element FinSequence-like FinSubsequence-like V268() set
Sum (((0* r) +* (m,T)) ^2) is ext-real complex real set
m is set
r is ext-real non negative ordinal natural complex real finite cardinal set
0.REAL r is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite r -element FinSequence-like FinSubsequence-like V268() Element of the carrier of (TOP-REAL r)
TOP-REAL r is non empty left_complementable right_complementable V138() V139() TopSpace-like Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed strict L16()
the carrier of (TOP-REAL r) is non empty set
r |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite r -element FinSequence-like FinSubsequence-like V268() Element of r -tuples_on REAL
r -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V268() Element of REAL * : len b1 = r } is set
Seg r is finite r -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
{ b1 where b1 is ext-real non negative ordinal natural complex real V43() V44() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT : ( 1 <= b1 & b1 <= r ) } is set
(Seg r) --> 0 is Relation-like Seg r -defined Seg r -defined RAT -valued INT -valued {0} -valued Function-like constant total total V18( Seg r,{0}) complex-valued ext-real-valued real-valued natural-valued finite FinSequence-like FinSubsequence-like Function-yielding V156() complex-functions-valued ext-real-functions-valued real-functions-valued V268() V316() V317() Element of bool [:(Seg r),{0}:]
{0} is functional non empty trivial finite V49() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered complex-functions-membered ext-real-functions-membered real-functions-membered set
[:(Seg r),{0}:] is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued finite set
bool [:(Seg r),{0}:] is finite V49() set
(0.REAL r) +* (m,0) is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite r -element FinSequence-like FinSubsequence-like V268() set
dom ((0.REAL r) +* (m,0)) is finite r -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
dom (0.REAL r) is finite r -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
f is set
((0.REAL r) +* (m,0)) . f is ext-real complex real set
(0.REAL r) . f is ext-real complex real set
((0.REAL r) +* (m,0)) . f is ext-real complex real set
(0.REAL r) . f is ext-real complex real set
m is set
r is ext-real non negative ordinal natural complex real finite cardinal set
0.REAL r is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite r -element FinSequence-like FinSubsequence-like V268() Element of the carrier of (TOP-REAL r)
TOP-REAL r is non empty left_complementable right_complementable V138() V139() TopSpace-like Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed strict L16()
the carrier of (TOP-REAL r) is non empty set
r |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite r -element FinSequence-like FinSubsequence-like V268() Element of r -tuples_on REAL
r -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V268() Element of REAL * : len b1 = r } is set
Seg r is finite r -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
{ b1 where b1 is ext-real non negative ordinal natural complex real V43() V44() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT : ( 1 <= b1 & b1 <= r ) } is set
(Seg r) --> 0 is Relation-like Seg r -defined Seg r -defined RAT -valued INT -valued {0} -valued Function-like constant total total V18( Seg r,{0}) complex-valued ext-real-valued real-valued natural-valued finite FinSequence-like FinSubsequence-like Function-yielding V156() complex-functions-valued ext-real-functions-valued real-functions-valued V268() V316() V317() Element of bool [:(Seg r),{0}:]
{0} is functional non empty trivial finite V49() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered complex-functions-membered ext-real-functions-membered real-functions-membered set
[:(Seg r),{0}:] is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued finite set
bool [:(Seg r),{0}:] is finite V49() set
T is ext-real complex real set
(0.REAL r) +* (m,T) is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite r -element FinSequence-like FinSubsequence-like V268() set
f is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite r -element FinSequence-like FinSubsequence-like V268() set
mlt (f,((0.REAL r) +* (m,T))) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite r -element FinSequence-like FinSubsequence-like V268() FinSequence of REAL
K857() .: (f,((0.REAL r) +* (m,T))) is Relation-like Function-like set
<:f,((0.REAL r) +* (m,T)):> is Relation-like Function-like set
<:f,((0.REAL r)