:: TOPREALC semantic presentation

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

{ b

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

{ b

(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

{ b

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

{ b

(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

{ b

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

{ b

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

{ b

Seg r is finite r -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT

{ b

(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

{ b

Seg r is finite r -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT

{ b

(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)