:: TOPREAL6 semantic presentation

REAL is non empty non trivial non with_non-empty_elements non finite V202() V203() V204() V208() non bounded_below non bounded_above V280() set

NAT is non empty non with_non-empty_elements epsilon-transitive epsilon-connected ordinal V202() V203() V204() V205() V206() V207() V208() left_end bounded_below Element of bool REAL

bool REAL is non empty set

{} is empty functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() real ext-real non positive non negative finite V40() FinSequence-membered V202() V203() V204() V205() V206() V207() V208() bounded_below bounded_above real-bounded V280() set

the empty functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() real ext-real non positive non negative finite V40() FinSequence-membered V202() V203() V204() V205() V206() V207() V208() bounded_below bounded_above real-bounded V280() set is empty functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() real ext-real non positive non negative finite V40() FinSequence-membered V202() V203() V204() V205() V206() V207() V208() bounded_below bounded_above real-bounded V280() set

1 is non empty epsilon-transitive epsilon-connected ordinal natural V31() real ext-real positive non negative V62() V136() V202() V203() V204() V205() V206() V207() left_end bounded_below Element of NAT

{{},1} is non empty finite V202() V203() V204() V205() V206() V207() left_end right_end bounded_below bounded_above real-bounded set

INT is non empty non trivial non finite V202() V203() V204() V205() V206() V208() set

COMPLEX is non empty non trivial non finite V202() V208() set

omega is non empty non with_non-empty_elements epsilon-transitive epsilon-connected ordinal V202() V203() V204() V205() V206() V207() V208() left_end bounded_below set

bool omega is non empty set

bool NAT is non empty set

K252(NAT) is V61() set

[:1,1:] is non empty RAT -valued INT -valued complex-yielding V193() V194() V195() set

RAT is non empty non trivial non finite V202() V203() V204() V205() V208() set

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

[:[:1,1:],1:] is non empty RAT -valued INT -valued complex-yielding V193() V194() V195() set

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

[:[:1,1:],REAL:] is non empty complex-yielding V193() V194() set

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

[:REAL,REAL:] is non empty complex-yielding V193() V194() set

[:[:REAL,REAL:],REAL:] is non empty complex-yielding V193() V194() set

bool [:[:REAL,REAL:],REAL:] is non empty set

2 is non empty epsilon-transitive epsilon-connected ordinal natural V31() real ext-real positive non negative V62() V136() V202() V203() V204() V205() V206() V207() left_end bounded_below Element of NAT

[:2,2:] is non empty RAT -valued INT -valued complex-yielding V193() V194() V195() set

[:[:2,2:],REAL:] is non empty complex-yielding V193() V194() set

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

bool [:REAL,REAL:] is non empty set

K496() is non empty V151() L10()

the carrier of K496() is non empty set

K501() is non empty V151() V173() V174() V175() V177() V224() V225() V226() V227() V228() V229() L10()

K502() is non empty V151() V175() V177() V227() V228() V229() M17(K501())

K503() is non empty V151() V173() V175() V177() V227() V228() V229() V230() M20(K501(),K502())

K505() is non empty V151() V173() V175() V177() L10()

K506() is non empty V151() V173() V175() V177() V230() M17(K505())

TOP-REAL 2 is non empty TopSpace-like V149() V214() V215() V232() V233() V234() V235() V236() V237() V238() strict add-continuous Mult-continuous RLTopStruct

the carrier of (TOP-REAL 2) is non empty set

bool the carrier of (TOP-REAL 2) is non empty set

[: the carrier of (TOP-REAL 2),REAL:] is non empty complex-yielding V193() V194() set

bool [: the carrier of (TOP-REAL 2),REAL:] is non empty set

I[01] is non empty strict TopSpace-like V270() TopStruct

the carrier of I[01] is non empty V202() V203() V204() set

RealSpace is non empty strict Reflexive discerning symmetric triangle Discerning V270() MetrStruct

R^1 is non empty strict TopSpace-like V270() TopStruct

the carrier of R^1 is non empty V202() V203() V204() set

[:COMPLEX,COMPLEX:] is non empty complex-yielding set

bool [:COMPLEX,COMPLEX:] is non empty set

[:COMPLEX,REAL:] is non empty complex-yielding V193() V194() set

bool [:COMPLEX,REAL:] is non empty set

[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty complex-yielding set

bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set

[:RAT,RAT:] is non empty RAT -valued complex-yielding V193() V194() set

bool [:RAT,RAT:] is non empty set

[:[:RAT,RAT:],RAT:] is non empty RAT -valued complex-yielding V193() V194() set

bool [:[:RAT,RAT:],RAT:] is non empty set

[:INT,INT:] is non empty RAT -valued INT -valued complex-yielding V193() V194() set

bool [:INT,INT:] is non empty set

[:[:INT,INT:],INT:] is non empty RAT -valued INT -valued complex-yielding V193() V194() set

bool [:[:INT,INT:],INT:] is non empty set

[:NAT,NAT:] is non empty RAT -valued INT -valued complex-yielding V193() V194() V195() set

[:[:NAT,NAT:],NAT:] is non empty RAT -valued INT -valued complex-yielding V193() V194() V195() set

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

ExtREAL is non empty V203() V280() set

3 is non empty epsilon-transitive epsilon-connected ordinal natural V31() real ext-real positive non negative V62() V136() V202() V203() V204() V205() V206() V207() left_end bounded_below Element of NAT

0 is empty functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() real ext-real non positive non negative finite V40() FinSequence-membered V62() V136() V202() V203() V204() V205() V206() V207() V208() bounded_below bounded_above real-bounded V280() Element of NAT

absreal is non empty Relation-like REAL -defined REAL -valued Function-like total quasi_total complex-yielding V193() V194() Element of bool [:REAL,REAL:]

Seg 1 is non empty finite V43(1) V202() V203() V204() V205() V206() V207() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT

{1} is non empty finite V202() V203() V204() V205() V206() V207() left_end right_end bounded_below bounded_above real-bounded set

Seg 2 is non empty finite V43(2) V202() V203() V204() V205() V206() V207() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT

{1,2} is non empty finite V202() V203() V204() V205() V206() V207() left_end right_end bounded_below bounded_above real-bounded set

bool the carrier of R^1 is non empty set

[:NAT,REAL:] is non empty complex-yielding V193() V194() set

bool [:NAT,REAL:] is non empty set

proj1 is non empty Relation-like the carrier of (TOP-REAL 2) -defined REAL -valued Function-like total quasi_total complex-yielding V193() V194() continuous Element of bool [: the carrier of (TOP-REAL 2),REAL:]

proj2 is non empty Relation-like the carrier of (TOP-REAL 2) -defined REAL -valued Function-like total quasi_total complex-yielding V193() V194() continuous Element of bool [: the carrier of (TOP-REAL 2),REAL:]

sqrreal is non empty Relation-like REAL -defined REAL -valued Function-like total quasi_total complex-yielding V193() V194() Element of bool [:REAL,REAL:]

<*> REAL is empty proper Relation-like NAT -defined REAL -valued Function-like functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() real ext-real non positive non negative finite finite-yielding V40() FinSequence-like FinSubsequence-like FinSequence-membered complex-yielding V193() V194() V195() V202() V203() V204() V205() V206() V207() V208() bounded_below bounded_above real-bounded V280() FinSequence of REAL

Product (<*> REAL) is V31() real ext-real Element of REAL

sqrt 2 is V31() real ext-real Element of REAL

TopSpaceMetr RealSpace is non empty strict TopSpace-like TopStruct

R^2-unit_square is being_special_polygon non horizontal non vertical Element of bool the carrier of (TOP-REAL 2)

|[0,0]| is non empty Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)

|[0,1]| is non empty Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)

LSeg (|[0,0]|,|[0,1]|) is non empty boundary connected convex Element of bool the carrier of (TOP-REAL 2)

{ (((1 - b

|[1,1]| is non empty Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)

LSeg (|[0,1]|,|[1,1]|) is non empty boundary connected convex Element of bool the carrier of (TOP-REAL 2)

{ (((1 - b

(LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|)) is non empty Element of bool the carrier of (TOP-REAL 2)

|[1,0]| is non empty Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)

LSeg (|[1,1]|,|[1,0]|) is non empty boundary connected convex Element of bool the carrier of (TOP-REAL 2)

{ (((1 - b

LSeg (|[1,0]|,|[0,0]|) is non empty boundary connected convex Element of bool the carrier of (TOP-REAL 2)

{ (((1 - b

(LSeg (|[1,1]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[0,0]|)) is non empty Element of bool the carrier of (TOP-REAL 2)

((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (|[1,1]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[0,0]|))) is non empty Element of bool the carrier of (TOP-REAL 2)

(LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) is Element of bool the carrier of (TOP-REAL 2)

{|[0,1]|} is non empty finite V40() set

LSeg (|[0,0]|,|[1,0]|) is non empty boundary connected convex Element of bool the carrier of (TOP-REAL 2)

{ (((1 - b

LSeg (|[1,0]|,|[1,1]|) is non empty boundary connected convex Element of bool the carrier of (TOP-REAL 2)

{ (((1 - b

(LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) is Element of bool the carrier of (TOP-REAL 2)

{|[1,0]|} is non empty finite V40() set

(LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) is Element of bool the carrier of (TOP-REAL 2)

{|[1,1]|} is non empty finite V40() set

Euclid 2 is non empty strict Reflexive discerning symmetric triangle Discerning MetrStruct

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

2 -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL

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

{ b

Pitag_dist 2 is non empty Relation-like [:(REAL 2),(REAL 2):] -defined REAL -valued Function-like total quasi_total complex-yielding V193() V194() Element of bool [:[:(REAL 2),(REAL 2):],REAL:]

[:(REAL 2),(REAL 2):] is non empty set

[:[:(REAL 2),(REAL 2):],REAL:] is non empty complex-yielding V193() V194() set

bool [:[:(REAL 2),(REAL 2):],REAL:] is non empty set

MetrStruct(# (REAL 2),(Pitag_dist 2) #) is strict MetrStruct

the carrier of (Euclid 2) is non empty set

union {} is epsilon-transitive epsilon-connected ordinal finite set

x1 is V31() real ext-real set

x2 is V31() real ext-real set

x1 + x2 is V31() real ext-real set

sqrt (x1 + x2) is V31() real ext-real set

sqrt x1 is V31() real ext-real set

sqrt x2 is V31() real ext-real set

(sqrt x1) + (sqrt x2) is V31() real ext-real set

x1 is V31() real ext-real set

abs x1 is V31() real ext-real Element of REAL

x2 is V31() real ext-real set

abs x2 is V31() real ext-real Element of REAL

x1 is V31() real ext-real set

abs x1 is V31() real ext-real Element of REAL

x2 is V31() real ext-real set

abs x2 is V31() real ext-real Element of REAL

- x2 is V31() real ext-real set

- x1 is V31() real ext-real set

x1 is V31() real ext-real Element of REAL

0 |-> x1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of 0 -tuples_on REAL

0 -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL

{ b

Seg 0 is empty proper functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() real ext-real non positive non negative finite V40() V43( 0 ) FinSequence-membered V202() V203() V204() V205() V206() V207() V208() bounded_below bounded_above real-bounded V280() Element of bool NAT

(Seg 0) --> x1 is empty Relation-like Seg 0 -defined {x1} -valued Function-like functional total quasi_total epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() real ext-real non positive non negative finite finite-yielding V40() FinSequence-like FinSubsequence-like FinSequence-membered complex-yielding V193() V194() V195() V202() V203() V204() V205() V206() V207() V208() bounded_below bounded_above real-bounded V280() Element of bool [:(Seg 0),{x1}:]

{x1} is non empty finite V202() V203() V204() left_end right_end bounded_below bounded_above real-bounded set

[:(Seg 0),{x1}:] is finite complex-yielding V193() V194() set

bool [:(Seg 0),{x1}:] is non empty finite V40() set

Product (0 |-> x1) is V31() real ext-real Element of REAL

x1 is V31() real ext-real Element of REAL

1 |-> x1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of 1 -tuples_on REAL

1 -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL

{ b

(Seg 1) --> x1 is non empty Relation-like Seg 1 -defined {x1} -valued Function-like total quasi_total finite complex-yielding V193() V194() Element of bool [:(Seg 1),{x1}:]

{x1} is non empty finite V202() V203() V204() left_end right_end bounded_below bounded_above real-bounded set

[:(Seg 1),{x1}:] is non empty finite complex-yielding V193() V194() set

bool [:(Seg 1),{x1}:] is non empty finite V40() set

Product (1 |-> x1) is V31() real ext-real Element of REAL

<*x1*> is non empty Relation-like NAT -defined REAL -valued Function-like finite V43(1) FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL

Product <*x1*> is V31() real ext-real Element of REAL

x1 is V31() real ext-real Element of REAL

2 |-> x1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of 2 -tuples_on REAL

(Seg 2) --> x1 is non empty Relation-like Seg 2 -defined {x1} -valued Function-like total quasi_total finite complex-yielding V193() V194() Element of bool [:(Seg 2),{x1}:]

{x1} is non empty finite V202() V203() V204() left_end right_end bounded_below bounded_above real-bounded set

[:(Seg 2),{x1}:] is non empty finite complex-yielding V193() V194() set

bool [:(Seg 2),{x1}:] is non empty finite V40() set

Product (2 |-> x1) is V31() real ext-real Element of REAL

x1 * x1 is V31() real ext-real Element of REAL

<*x1,x1*> is non empty Relation-like NAT -defined REAL -valued Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL

Product <*x1,x1*> is V31() real ext-real Element of REAL

x1 is V31() real ext-real Element of REAL

x2 is epsilon-transitive epsilon-connected ordinal natural V31() real ext-real V62() V136() V202() V203() V204() V205() V206() V207() bounded_below Element of NAT

x2 + 1 is epsilon-transitive epsilon-connected ordinal natural V31() real ext-real V62() V136() V202() V203() V204() V205() V206() V207() bounded_below Element of NAT

(x2 + 1) |-> x1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of (x2 + 1) -tuples_on REAL

(x2 + 1) -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL

{ b

Seg (x2 + 1) is finite V43(x2 + 1) V202() V203() V204() V205() V206() V207() bounded_below bounded_above real-bounded Element of bool NAT

(Seg (x2 + 1)) --> x1 is Relation-like Seg (x2 + 1) -defined {x1} -valued Function-like total quasi_total finite complex-yielding V193() V194() Element of bool [:(Seg (x2 + 1)),{x1}:]

{x1} is non empty finite V202() V203() V204() left_end right_end bounded_below bounded_above real-bounded set

[:(Seg (x2 + 1)),{x1}:] is finite complex-yielding V193() V194() set

bool [:(Seg (x2 + 1)),{x1}:] is non empty finite V40() set

Product ((x2 + 1) |-> x1) is V31() real ext-real Element of REAL

x2 |-> x1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of x2 -tuples_on REAL

x2 -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL

{ b

Seg x2 is finite V43(x2) V202() V203() V204() V205() V206() V207() bounded_below bounded_above real-bounded Element of bool NAT

(Seg x2) --> x1 is Relation-like Seg x2 -defined {x1} -valued Function-like total quasi_total finite complex-yielding V193() V194() Element of bool [:(Seg x2),{x1}:]

[:(Seg x2),{x1}:] is finite complex-yielding V193() V194() set

bool [:(Seg x2),{x1}:] is non empty finite V40() set

Product (x2 |-> x1) is V31() real ext-real Element of REAL

(Product (x2 |-> x1)) * x1 is V31() real ext-real Element of REAL

1 |-> x1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of 1 -tuples_on REAL

1 -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL

{ b

(Seg 1) --> x1 is non empty Relation-like Seg 1 -defined {x1} -valued Function-like total quasi_total finite complex-yielding V193() V194() Element of bool [:(Seg 1),{x1}:]

[:(Seg 1),{x1}:] is non empty finite complex-yielding V193() V194() set

bool [:(Seg 1),{x1}:] is non empty finite V40() set

Product (1 |-> x1) is V31() real ext-real Element of REAL

(Product (x2 |-> x1)) * (Product (1 |-> x1)) is V31() real ext-real Element of REAL

x1 is V31() real ext-real Element of REAL

x2 is epsilon-transitive epsilon-connected ordinal natural V31() real ext-real V62() V136() V202() V203() V204() V205() V206() V207() bounded_below Element of NAT

x2 |-> x1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of x2 -tuples_on REAL

x2 -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL

{ b

Seg x2 is finite V43(x2) V202() V203() V204() V205() V206() V207() bounded_below bounded_above real-bounded Element of bool NAT

(Seg x2) --> x1 is Relation-like Seg x2 -defined {x1} -valued Function-like total quasi_total finite complex-yielding V193() V194() Element of bool [:(Seg x2),{x1}:]

{x1} is non empty finite V202() V203() V204() left_end right_end bounded_below bounded_above real-bounded set

[:(Seg x2),{x1}:] is finite complex-yielding V193() V194() set

bool [:(Seg x2),{x1}:] is non empty finite V40() set

Product (x2 |-> x1) is V31() real ext-real Element of REAL

dom (x2 |-> x1) is finite V202() V203() V204() V205() V206() V207() bounded_below bounded_above real-bounded Element of bool NAT

y2 is epsilon-transitive epsilon-connected ordinal natural V31() real ext-real set

y2 + 1 is epsilon-transitive epsilon-connected ordinal natural V31() real ext-real V62() V136() V202() V203() V204() V205() V206() V207() bounded_below Element of NAT

(x2 |-> x1) . 1 is V31() real ext-real Element of REAL

y2 is epsilon-transitive epsilon-connected ordinal natural V31() real ext-real set

(x2 |-> x1) . y2 is V31() real ext-real Element of REAL

x1 is V31() real ext-real Element of REAL

x2 is epsilon-transitive epsilon-connected ordinal natural V31() real ext-real V62() V136() V202() V203() V204() V205() V206() V207() bounded_below Element of NAT

x2 |-> x1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of x2 -tuples_on REAL

x2 -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL

{ b

Seg x2 is finite V43(x2) V202() V203() V204() V205() V206() V207() bounded_below bounded_above real-bounded Element of bool NAT

(Seg x2) --> x1 is Relation-like Seg x2 -defined {x1} -valued Function-like total quasi_total finite complex-yielding V193() V194() Element of bool [:(Seg x2),{x1}:]

{x1} is non empty finite V202() V203() V204() left_end right_end bounded_below bounded_above real-bounded set

[:(Seg x2),{x1}:] is finite complex-yielding V193() V194() set

bool [:(Seg x2),{x1}:] is non empty finite V40() set

Product (x2 |-> x1) is V31() real ext-real Element of REAL

y1 is epsilon-transitive epsilon-connected ordinal natural V31() real ext-real V62() V136() V202() V203() V204() V205() V206() V207() bounded_below Element of NAT

y1 -' x2 is epsilon-transitive epsilon-connected ordinal natural V31() real ext-real non negative V62() V136() V202() V203() V204() V205() V206() V207() bounded_below Element of NAT

(y1 -' x2) |-> x1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of (y1 -' x2) -tuples_on REAL

(y1 -' x2) -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL

{ b

Seg (y1 -' x2) is finite V43(y1 -' x2) V202() V203() V204() V205() V206() V207() bounded_below bounded_above real-bounded Element of bool NAT

(Seg (y1 -' x2)) --> x1 is Relation-like Seg (y1 -' x2) -defined {x1} -valued Function-like total quasi_total finite complex-yielding V193() V194() Element of bool [:(Seg (y1 -' x2)),{x1}:]

[:(Seg (y1 -' x2)),{x1}:] is finite complex-yielding V193() V194() set

bool [:(Seg (y1 -' x2)),{x1}:] is non empty finite V40() set

Product ((y1 -' x2) |-> x1) is V31() real ext-real Element of REAL

y1 |-> x1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of y1 -tuples_on REAL

y1 -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL

{ b

Seg y1 is finite V43(y1) V202() V203() V204() V205() V206() V207() bounded_below bounded_above real-bounded Element of bool NAT

(Seg y1) --> x1 is Relation-like Seg y1 -defined {x1} -valued Function-like total quasi_total finite complex-yielding V193() V194() Element of bool [:(Seg y1),{x1}:]

[:(Seg y1),{x1}:] is finite complex-yielding V193() V194() set

bool [:(Seg y1),{x1}:] is non empty finite V40() set

Product (y1 |-> x1) is V31() real ext-real Element of REAL

(Product (y1 |-> x1)) / (Product (x2 |-> x1)) is V31() real ext-real Element of REAL

y2 is epsilon-transitive epsilon-connected ordinal natural V31() real ext-real V62() V136() V202() V203() V204() V205() V206() V207() bounded_below Element of NAT

y2 -' x2 is epsilon-transitive epsilon-connected ordinal natural V31() real ext-real non negative V62() V136() V202() V203() V204() V205() V206() V207() bounded_below Element of NAT

(y2 -' x2) |-> x1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of (y2 -' x2) -tuples_on REAL

(y2 -' x2) -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL

{ b

Seg (y2 -' x2) is finite V43(y2 -' x2) V202() V203() V204() V205() V206() V207() bounded_below bounded_above real-bounded Element of bool NAT

(Seg (y2 -' x2)) --> x1 is Relation-like Seg (y2 -' x2) -defined {x1} -valued Function-like total quasi_total finite complex-yielding V193() V194() Element of bool [:(Seg (y2 -' x2)),{x1}:]

[:(Seg (y2 -' x2)),{x1}:] is finite complex-yielding V193() V194() set

bool [:(Seg (y2 -' x2)),{x1}:] is non empty finite V40() set

Product ((y2 -' x2) |-> x1) is V31() real ext-real Element of REAL

y2 |-> x1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of y2 -tuples_on REAL

y2 -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL

{ b

Seg y2 is finite V43(y2) V202() V203() V204() V205() V206() V207() bounded_below bounded_above real-bounded Element of bool NAT

(Seg y2) --> x1 is Relation-like Seg y2 -defined {x1} -valued Function-like total quasi_total finite complex-yielding V193() V194() Element of bool [:(Seg y2),{x1}:]

[:(Seg y2),{x1}:] is finite complex-yielding V193() V194() set

bool [:(Seg y2),{x1}:] is non empty finite V40() set

Product (y2 |-> x1) is V31() real ext-real Element of REAL

(Product (y2 |-> x1)) / (Product (x2 |-> x1)) is V31() real ext-real Element of REAL

y2 + 1 is epsilon-transitive epsilon-connected ordinal natural V31() real ext-real V62() V136() V202() V203() V204() V205() V206() V207() bounded_below Element of NAT

(y2 + 1) -' x2 is epsilon-transitive epsilon-connected ordinal natural V31() real ext-real non negative V62() V136() V202() V203() V204() V205() V206() V207() bounded_below Element of NAT

((y2 + 1) -' x2) |-> x1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of ((y2 + 1) -' x2) -tuples_on REAL

((y2 + 1) -' x2) -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL

{ b

Seg ((y2 + 1) -' x2) is finite V43((y2 + 1) -' x2) V202() V203() V204() V205() V206() V207() bounded_below bounded_above real-bounded Element of bool NAT

(Seg ((y2 + 1) -' x2)) --> x1 is Relation-like Seg ((y2 + 1) -' x2) -defined {x1} -valued Function-like total quasi_total finite complex-yielding V193() V194() Element of bool [:(Seg ((y2 + 1) -' x2)),{x1}:]

[:(Seg ((y2 + 1) -' x2)),{x1}:] is finite complex-yielding V193() V194() set

bool [:(Seg ((y2 + 1) -' x2)),{x1}:] is non empty finite V40() set

Product (((y2 + 1) -' x2) |-> x1) is V31() real ext-real Element of REAL

(y2 + 1) |-> x1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of (y2 + 1) -tuples_on REAL

(y2 + 1) -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL

{ b

Seg (y2 + 1) is finite V43(y2 + 1) V202() V203() V204() V205() V206() V207() bounded_below bounded_above real-bounded Element of bool NAT

(Seg (y2 + 1)) --> x1 is Relation-like Seg (y2 + 1) -defined {x1} -valued Function-like total quasi_total finite complex-yielding V193() V194() Element of bool [:(Seg (y2 + 1)),{x1}:]

[:(Seg (y2 + 1)),{x1}:] is finite complex-yielding V193() V194() set

bool [:(Seg (y2 + 1)),{x1}:] is non empty finite V40() set

Product ((y2 + 1) |-> x1) is V31() real ext-real Element of REAL

(Product ((y2 + 1) |-> x1)) / (Product (x2 |-> x1)) is V31() real ext-real Element of REAL

(y2 -' x2) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V31() real ext-real positive non negative V62() V136() V202() V203() V204() V205() V206() V207() left_end bounded_below Element of NAT

((y2 -' x2) + 1) |-> x1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of ((y2 -' x2) + 1) -tuples_on REAL

((y2 -' x2) + 1) -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL

{ b

Seg ((y2 -' x2) + 1) is non empty finite V43((y2 -' x2) + 1) V202() V203() V204() V205() V206() V207() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT

(Seg ((y2 -' x2) + 1)) --> x1 is non empty Relation-like Seg ((y2 -' x2) + 1) -defined {x1} -valued Function-like total quasi_total finite complex-yielding V193() V194() Element of bool [:(Seg ((y2 -' x2) + 1)),{x1}:]

[:(Seg ((y2 -' x2) + 1)),{x1}:] is non empty finite complex-yielding V193() V194() set

bool [:(Seg ((y2 -' x2) + 1)),{x1}:] is non empty finite V40() set

Product (((y2 -' x2) + 1) |-> x1) is V31() real ext-real Element of REAL

1 |-> x1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of 1 -tuples_on REAL

1 -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL

{ b

(Seg 1) --> x1 is non empty Relation-like Seg 1 -defined {x1} -valued Function-like total quasi_total finite complex-yielding V193() V194() Element of bool [:(Seg 1),{x1}:]

[:(Seg 1),{x1}:] is non empty finite complex-yielding V193() V194() set

bool [:(Seg 1),{x1}:] is non empty finite V40() set

Product (1 |-> x1) is V31() real ext-real Element of REAL

(Product ((y2 -' x2) |-> x1)) * (Product (1 |-> x1)) is V31() real ext-real Element of REAL

((Product (y2 |-> x1)) / (Product (x2 |-> x1))) * x1 is V31() real ext-real Element of REAL

(Product (y2 |-> x1)) * x1 is V31() real ext-real Element of REAL

((Product (y2 |-> x1)) * x1) / (Product (x2 |-> x1)) is V31() real ext-real Element of REAL

0 |-> x1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of 0 -tuples_on REAL

0 -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL

{ b

Seg 0 is empty proper functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() real ext-real non positive non negative finite V40() V43( 0 ) FinSequence-membered V202() V203() V204() V205() V206() V207() V208() bounded_below bounded_above real-bounded V280() Element of bool NAT

(Seg 0) --> x1 is empty Relation-like Seg 0 -defined {x1} -valued Function-like functional total quasi_total epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() real ext-real non positive non negative finite finite-yielding V40() FinSequence-like FinSubsequence-like FinSequence-membered complex-yielding V193() V194() V195() V202() V203() V204() V205() V206() V207() V208() bounded_below bounded_above real-bounded V280() Element of bool [:(Seg 0),{x1}:]

[:(Seg 0),{x1}:] is finite complex-yielding V193() V194() set

bool [:(Seg 0),{x1}:] is non empty finite V40() set

Product (0 |-> x1) is V31() real ext-real Element of REAL

0 -' x2 is epsilon-transitive epsilon-connected ordinal natural V31() real ext-real non negative V62() V136() V202() V203() V204() V205() V206() V207() bounded_below Element of NAT

(0 -' x2) |-> x1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of (0 -' x2) -tuples_on REAL

(0 -' x2) -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL

{ b

Seg (0 -' x2) is finite V43(0 -' x2) V202() V203() V204() V205() V206() V207() bounded_below bounded_above real-bounded Element of bool NAT

(Seg (0 -' x2)) --> x1 is Relation-like Seg (0 -' x2) -defined {x1} -valued Function-like total quasi_total finite complex-yielding V193() V194() Element of bool [:(Seg (0 -' x2)),{x1}:]

[:(Seg (0 -' x2)),{x1}:] is finite complex-yielding V193() V194() set

bool [:(Seg (0 -' x2)),{x1}:] is non empty finite V40() set

Product ((0 -' x2) |-> x1) is V31() real ext-real Element of REAL

0 |-> x1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of 0 -tuples_on REAL

0 -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL

{ b

Seg 0 is empty proper functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() real ext-real non positive non negative finite V40() V43( 0 ) FinSequence-membered V202() V203() V204() V205() V206() V207() V208() bounded_below bounded_above real-bounded V280() Element of bool NAT

(Seg 0) --> x1 is empty Relation-like Seg 0 -defined {x1} -valued Function-like functional total quasi_total epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() real ext-real non positive non negative finite finite-yielding V40() FinSequence-like FinSubsequence-like FinSequence-membered complex-yielding V193() V194() V195() V202() V203() V204() V205() V206() V207() V208() bounded_below bounded_above real-bounded V280() Element of bool [:(Seg 0),{x1}:]

[:(Seg 0),{x1}:] is finite complex-yielding V193() V194() set

bool [:(Seg 0),{x1}:] is non empty finite V40() set

Product (0 |-> x1) is V31() real ext-real Element of REAL

(Product (0 |-> x1)) / (Product (x2 |-> x1)) is V31() real ext-real Element of REAL

(Product (0 |-> x1)) / (Product (<*> REAL)) is V31() real ext-real Element of REAL

x1 is V31() real ext-real Element of REAL

x2 is epsilon-transitive epsilon-connected ordinal natural V31() real ext-real V62() V136() V202() V203() V204() V205() V206() V207() bounded_below Element of NAT

x1 |^ x2 is V31() real ext-real Element of REAL

y1 is epsilon-transitive epsilon-connected ordinal natural V31() real ext-real V62() V136() V202() V203() V204() V205() V206() V207() bounded_below Element of NAT

y1 -' x2 is epsilon-transitive epsilon-connected ordinal natural V31() real ext-real non negative V62() V136() V202() V203() V204() V205() V206() V207() bounded_below Element of NAT

x1 |^ (y1 -' x2) is V31() real ext-real Element of REAL

x1 |^ y1 is V31() real ext-real Element of REAL

(x1 |^ y1) / (x1 |^ x2) is V31() real ext-real Element of REAL

y1 |-> x1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of y1 -tuples_on REAL

y1 -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL

{ b

Seg y1 is finite V43(y1) V202() V203() V204() V205() V206() V207() bounded_below bounded_above real-bounded Element of bool NAT

(Seg y1) --> x1 is Relation-like Seg y1 -defined {x1} -valued Function-like total quasi_total finite complex-yielding V193() V194() Element of bool [:(Seg y1),{x1}:]

{x1} is non empty finite V202() V203() V204() left_end right_end bounded_below bounded_above real-bounded set

[:(Seg y1),{x1}:] is finite complex-yielding V193() V194() set

bool [:(Seg y1),{x1}:] is non empty finite V40() set

Product (y1 |-> x1) is V31() real ext-real Element of REAL

(Product (y1 |-> x1)) / (x1 |^ x2) is V31() real ext-real Element of REAL

x2 |-> x1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of x2 -tuples_on REAL

x2 -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL

{ b

Seg x2 is finite V43(x2) V202() V203() V204() V205() V206() V207() bounded_below bounded_above real-bounded Element of bool NAT

(Seg x2) --> x1 is Relation-like Seg x2 -defined {x1} -valued Function-like total quasi_total finite complex-yielding V193() V194() Element of bool [:(Seg x2),{x1}:]

[:(Seg x2),{x1}:] is finite complex-yielding V193() V194() set

bool [:(Seg x2),{x1}:] is non empty finite V40() set

Product (x2 |-> x1) is V31() real ext-real Element of REAL

(Product (y1 |-> x1)) / (Product (x2 |-> x1)) is V31() real ext-real Element of REAL

(y1 -' x2) |-> x1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of (y1 -' x2) -tuples_on REAL

(y1 -' x2) -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL

{ b

Seg (y1 -' x2) is finite V43(y1 -' x2) V202() V203() V204() V205() V206() V207() bounded_below bounded_above real-bounded Element of bool NAT

(Seg (y1 -' x2)) --> x1 is Relation-like Seg (y1 -' x2) -defined {x1} -valued Function-like total quasi_total finite complex-yielding V193() V194() Element of bool [:(Seg (y1 -' x2)),{x1}:]

[:(Seg (y1 -' x2)),{x1}:] is finite complex-yielding V193() V194() set

bool [:(Seg (y1 -' x2)),{x1}:] is non empty finite V40() set

Product ((y1 -' x2) |-> x1) is V31() real ext-real Element of REAL

x1 is V31() real ext-real Element of REAL

x1 ^2 is V31() real ext-real Element of REAL

x1 * x1 is V31() real ext-real set

x2 is V31() real ext-real Element of REAL

<*x1,x2*> is non empty Relation-like NAT -defined REAL -valued Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL

sqr <*x1,x2*> is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL

x2 ^2 is V31() real ext-real Element of REAL

x2 * x2 is V31() real ext-real set

<*(x1 ^2),(x2 ^2)*> is non empty Relation-like NAT -defined REAL -valued Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL

dom sqrreal is V202() V203() V204() Element of bool REAL

rng <*x1,x2*> is finite compact closed V202() V203() V204() bounded_below bounded_above real-bounded Element of bool REAL

dom <*(x1 ^2),(x2 ^2)*> is finite V202() V203() V204() V205() V206() V207() bounded_below bounded_above real-bounded Element of bool NAT

y1 is set

(sqr <*x1,x2*>) . y1 is V31() real ext-real Element of REAL

<*(x1 ^2),(x2 ^2)*> . y1 is V31() real ext-real Element of REAL

<*x1,x2*> . 1 is V31() real ext-real Element of REAL

<*x1,x2*> . 2 is V31() real ext-real Element of REAL

dom (sqr <*x1,x2*>) is finite V202() V203() V204() V205() V206() V207() bounded_below bounded_above real-bounded Element of bool NAT

sqrreal * <*x1,x2*> is Relation-like NAT -defined REAL -valued Function-like finite complex-yielding V193() V194() Element of bool [:NAT,REAL:]

dom (sqrreal * <*x1,x2*>) is finite V202() V203() V204() V205() V206() V207() bounded_below bounded_above real-bounded Element of bool NAT

dom <*x1,x2*> is finite V202() V203() V204() V205() V206() V207() bounded_below bounded_above real-bounded Element of bool NAT

x1 is V31() real ext-real Element of REAL

abs x1 is V31() real ext-real Element of REAL

x2 is epsilon-transitive epsilon-connected ordinal natural V31() real ext-real set

y1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL

abs y1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL

y1 * absreal is Relation-like finite complex-yielding V193() V194() set

dom (abs y1) is finite V202() V203() V204() V205() V206() V207() bounded_below bounded_above real-bounded Element of bool NAT

y1 . x2 is V31() real ext-real Element of REAL

(abs y1) . x2 is V31() real ext-real Element of REAL

absreal . x1 is V31() real ext-real Element of REAL

x1 is V31() real ext-real Element of REAL

abs x1 is V31() real ext-real Element of REAL

x2 is V31() real ext-real Element of REAL

<*x1,x2*> is non empty Relation-like NAT -defined REAL -valued Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL

abs <*x1,x2*> is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL

<*x1,x2*> * absreal is Relation-like finite complex-yielding V193() V194() set

abs x2 is V31() real ext-real Element of REAL

<*(abs x1),(abs x2)*> is non empty Relation-like NAT -defined REAL -valued Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL

dom absreal is V202() V203() V204() Element of bool REAL

rng <*x1,x2*> is finite compact closed V202() V203() V204() bounded_below bounded_above real-bounded Element of bool REAL

dom (abs <*x1,x2*>) is finite V202() V203() V204() V205() V206() V207() bounded_below bounded_above real-bounded Element of bool NAT

dom <*x1,x2*> is finite V202() V203() V204() V205() V206() V207() bounded_below bounded_above real-bounded Element of bool NAT

dom <*(abs x1),(abs x2)*> is finite V202() V203() V204() V205() V206() V207() bounded_below bounded_above real-bounded Element of bool NAT

y1 is set

(abs <*x1,x2*>) . y1 is V31() real ext-real Element of REAL

<*(abs x1),(abs x2)*> . y1 is V31() real ext-real Element of REAL

<*x1,x2*> . 1 is V31() real ext-real Element of REAL

<*x1,x2*> . 2 is V31() real ext-real Element of REAL

x1 is V31() real ext-real set

x2 is V31() real ext-real set

y1 is V31() real ext-real set

y2 is V31() real ext-real set

x2 - x1 is V31() real ext-real set

abs (x2 - x1) is V31() real ext-real Element of REAL

y2 - y1 is V31() real ext-real set

abs (y2 - y1) is V31() real ext-real Element of REAL

(abs (x2 - x1)) + (abs (y2 - y1)) is V31() real ext-real Element of REAL

(x2 - x1) + (y2 - y1) is V31() real ext-real set

x1 - x1 is V31() real ext-real set

y1 - y1 is V31() real ext-real set

x2 is V31() real ext-real set

x1 is V31() real ext-real set

x1 - x2 is V31() real ext-real set

x1 + x2 is V31() real ext-real set

].(x1 - x2),(x1 + x2).[ is open V202() V203() V204() non left_end non right_end V280() Element of bool REAL

x1 - x1 is V31() real ext-real set

abs (x1 - x1) is V31() real ext-real Element of REAL

x2 is V31() real ext-real set

x1 is V31() real ext-real set

x1 - x2 is V31() real ext-real set

x1 + x2 is V31() real ext-real set

[.(x1 - x2),(x1 + x2).] is compact closed V202() V203() V204() bounded_below bounded_above real-bounded V280() Element of bool REAL

y1 is V31() real ext-real Element of REAL

y1 + 0 is V31() real ext-real Element of REAL

y2 is V31() real ext-real Element of REAL

y1 + y2 is V31() real ext-real Element of REAL

y1 - y2 is V31() real ext-real Element of REAL

[.(y1 - y2),(y1 + y2).] is compact closed V202() V203() V204() bounded_below bounded_above real-bounded V280() Element of bool REAL

{ b

y1 - 0 is V31() real ext-real Element of REAL

x2 is V31() real ext-real set

x1 is V31() real ext-real set

].x1,x2.[ is open V202() V203() V204() non left_end non right_end V280() Element of bool REAL

lower_bound ].x1,x2.[ is V31() real ext-real Element of REAL

upper_bound ].x1,x2.[ is V31() real ext-real Element of REAL

a is V31() real ext-real Element of REAL

y2 is V31() real ext-real Element of REAL

y2 + a is V31() real ext-real Element of REAL

(y2 + a) / 2 is V31() real ext-real Element of REAL

{ b

b is V31() real ext-real set

y2 + b is V31() real ext-real Element of REAL

O is V31() real ext-real Element of REAL

y2 + O is V31() real ext-real Element of REAL

O is V31() real ext-real Element of REAL

y2 + O is V31() real ext-real Element of REAL

y2 + (y2 + O) is V31() real ext-real Element of REAL

(y2 + (y2 + O)) / 2 is V31() real ext-real Element of REAL

O is V31() real ext-real Element of REAL

y2 + O is V31() real ext-real Element of REAL

b is V31() real ext-real set

a - b is V31() real ext-real Element of REAL

O is V31() real ext-real Element of REAL

a - O is V31() real ext-real Element of REAL

O is V31() real ext-real Element of REAL

a - O is V31() real ext-real Element of REAL

a - 0 is V31() real ext-real Element of REAL

a + (a - O) is V31() real ext-real Element of REAL

(a + (a - O)) / 2 is V31() real ext-real Element of REAL

O is V31() real ext-real Element of REAL

a - O is V31() real ext-real Element of REAL

b is ext-real set

O is V31() real ext-real Element of REAL

b is V31() real ext-real set

O is V31() real ext-real Element of REAL

b is ext-real set

O is V31() real ext-real Element of REAL

b is V31() real ext-real set

O is V31() real ext-real Element of REAL

x1 is TopStruct

the carrier of x1 is set

bool the carrier of x1 is non empty set

x2 is finite Element of bool the carrier of x1

x1 | x2 is strict SubSpace of x1

x1 is TopStruct

the carrier of x1 is set

bool the carrier of x1 is non empty set

x2 is Element of bool the carrier of x1

x1 | x2 is strict SubSpace of x1

the carrier of (x1 | x2) is set

bool the carrier of (x1 | x2) is non empty set

[#] (x1 | x2) is non proper dense Element of bool the carrier of (x1 | x2)

y2 is Element of bool the carrier of (x1 | x2)

a is Element of bool the carrier of (x1 | x2)

y2 \/ a is Element of bool the carrier of (x1 | x2)

{} (x1 | x2) is empty functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() real ext-real non positive non negative finite V40() FinSequence-membered boundary compact V202() V203() V204() V205() V206() V207() V208() bounded_below bounded_above real-bounded V280() Element of bool the carrier of (x1 | x2)

y1 is empty functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() real ext-real non positive non negative finite V40() FinSequence-membered boundary compact V202() V203() V204() V205() V206() V207() V208() bounded_below bounded_above real-bounded V280() Element of bool the carrier of x1

x1 | y1 is empty trivial finite {} -element strict T_0 T_1 T_2 SubSpace of x1

[#] (x1 | y1) is empty trivial non proper functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() real ext-real non positive non negative finite V40() FinSequence-membered dense boundary compact V202() V203() V204() V205() V206() V207() V208() bounded_below bounded_above real-bounded V280() Element of bool the carrier of (x1 | y1)

the carrier of (x1 | y1) is empty trivial functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() real ext-real non positive non negative finite V40() FinSequence-membered V202() V203() V204() V205() V206() V207() V208() bounded_below bounded_above real-bounded V280() set

bool the carrier of (x1 | y1) is non empty finite V40() set

x1 is TopSpace-like TopStruct

x2 is TopSpace-like TopStruct

the carrier of x1 is set

the carrier of x2 is set

[: the carrier of x1, the carrier of x2:] is set

bool [: the carrier of x1, the carrier of x2:] is non empty set

y1 is Relation-like the carrier of x1 -defined the carrier of x2 -valued Function-like quasi_total Element of bool [: the carrier of x1, the carrier of x2:]

rng y1 is Element of bool the carrier of x2

bool the carrier of x2 is non empty set

[#] x2 is non proper open closed dense Element of bool the carrier of x2

dom y1 is Element of bool the carrier of x1

bool the carrier of x1 is non empty set

[#] x1 is non proper open closed dense Element of bool the carrier of x1

y1 .: ([#] x1) is Element of bool the carrier of x2

x1 is TopSpace-like TopStruct

the carrier of x1 is set

bool the carrier of x1 is non empty set

bool (bool the carrier of x1) is non empty set

x2 is finite Element of bool (bool the carrier of x1)

union x2 is Element of bool the carrier of x1

y1 is set

y2 is set

union y2 is set

{y1} is non empty finite set

y2 \/ {y1} is non empty set

union (y2 \/ {y1}) is set

bool the carrier of x1 is non empty Element of bool (bool the carrier of x1)

a is set

O is Element of bool the carrier of x1

a is Element of bool (bool the carrier of x1)

union a is Element of bool the carrier of x1

b is Element of bool the carrier of x1

(union a) \/ b is Element of bool the carrier of x1

union {y1} is set

{} x1 is empty functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() real ext-real non positive non negative finite V40() FinSequence-membered open closed boundary nowhere_dense connected compact V202() V203() V204() V205() V206() V207() V208() bounded_below bounded_above real-bounded V280() Element of bool the carrier of x1

union x2 is set

y1 is Element of bool the carrier of x1

x1 is set

x2 is set

y1 is set

y2 is set

a is set

b is set

(a,b) --> (x1,y1) is Relation-like Function-like finite set

product ((a,b) --> (x1,y1)) is set

(a,b) --> (x2,y2) is Relation-like Function-like finite set

product ((a,b) --> (x2,y2)) is set

dom ((a,b) --> (x1,y1)) is finite set

{a,b} is non empty finite set

g is set

((a,b) --> (x1,y1)) . g is set

((a,b) --> (x2,y2)) . g is set

((a,b) --> (x1,y1)) . b is set

((a,b) --> (x1,y1)) . a is set

a .--> y1 is trivial finite set

((a,b) --> (x1,y1)) . a is set

a .--> y2 is trivial finite set

dom ((a,b) --> (x2,y2)) is finite set

x1 is V202() V203() V204() Element of bool REAL

x2 is V202() V203() V204() Element of bool REAL

(1,2) --> (x1,x2) is non empty Relation-like NAT -defined {1,2} -defined bool REAL -valued Function-like total quasi_total finite Element of bool [:{1,2},(bool REAL):]

[:{1,2},(bool REAL):] is non empty set

bool [:{1,2},(bool REAL):] is non empty set

product ((1,2) --> (x1,x2)) is set

y2 is set

((1,2) --> (x1,x2)) . 1 is set

((1,2) --> (x1,x2)) . 2 is set

dom ((1,2) --> (x1,x2)) is finite V202() V203() V204() V205() V206() V207() bounded_below bounded_above real-bounded Element of bool {1,2}

bool {1,2} is non empty finite V40() set

a is Relation-like Function-like set

dom a is set

a . 2 is set

a . 1 is set

g is set

a . g is set

<*(a . 1),(a . 2)*> is non empty Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like set

<*(a . 1),(a . 2)*> . g is set

dom <*(a . 1),(a . 2)*> is finite V202() V203() V204() V205() V206() V207() bounded_below bounded_above real-bounded Element of bool NAT

b is V31() real ext-real Element of REAL

O is V31() real ext-real Element of REAL

|[b,O]| is non empty Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)

x1 is V31() real ext-real Element of REAL

|[0,x1]| is non empty Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)

|.|[0,x1]|.| is V31() real ext-real non negative Element of REAL

sqr |[0,x1]| is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL

Sum (sqr |[0,x1]|) is V31() real ext-real Element of REAL

sqrt (Sum (sqr |[0,x1]|)) is V31() real ext-real Element of REAL

abs x1 is V31() real ext-real Element of REAL

|[x1,0]| is non empty Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)

|.|[x1,0]|.| is V31() real ext-real non negative Element of REAL

sqr |[x1,0]| is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL

Sum (sqr |[x1,0]|) is V31() real ext-real Element of REAL

sqrt (Sum (sqr |[x1,0]|)) is V31() real ext-real Element of REAL

<*0,x1*> is non empty Relation-like NAT -defined REAL -valued Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL

|.<*0,x1*>.| is V31() real ext-real non negative Element of REAL

sqr <*0,x1*> is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL

Sum (sqr <*0,x1*>) is V31() real ext-real Element of REAL

sqrt (Sum (sqr <*0,x1*>)) is V31() real ext-real Element of REAL

0 ^2 is V31() real ext-real Element of REAL

0 * 0 is empty functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() real ext-real non positive non negative finite V40() FinSequence-membered V202() V203() V204() V205() V206() V207() V208() bounded_below bounded_above real-bounded V280() set

x1 ^2 is V31() real ext-real Element of REAL

x1 * x1 is V31() real ext-real set

<*(0 ^2),(x1 ^2)*> is non empty Relation-like NAT -defined REAL -valued Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL

Sum <*(0 ^2),(x1 ^2)*> is V31() real ext-real Element of REAL

sqrt (Sum <*(0 ^2),(x1 ^2)*>) is V31() real ext-real Element of REAL

0 + (x1 ^2) is V31() real ext-real Element of REAL

sqrt (0 + (x1 ^2)) is V31() real ext-real Element of REAL

<*x1,0*> is non empty Relation-like NAT -defined REAL -valued Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL

|.<*x1,0*>.| is V31() real ext-real non negative Element of REAL

sqr <*x1,0*> is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL

Sum (sqr <*x1,0*>) is V31() real ext-real Element of REAL

sqrt (Sum (sqr <*x1,0*>)) is V31() real ext-real Element of REAL

<*(x1 ^2),(0 ^2)*> is non empty Relation-like NAT -defined REAL -valued Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL

Sum <*(x1 ^2),(0 ^2)*> is V31() real ext-real Element of REAL

sqrt (Sum <*(x1 ^2),(0 ^2)*>) is V31() real ext-real Element of REAL

(x1 ^2) + 0 is V31() real ext-real Element of REAL

sqrt ((x1 ^2) + 0) is V31() real ext-real Element of REAL

0. (TOP-REAL 2) is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like V72( TOP-REAL 2) complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)

the ZeroF of (TOP-REAL 2) is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)

<*0,0*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() V195() FinSequence of NAT

x1 is Element of the carrier of (Euclid 2)

x2 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)

x2 `1 is V31() real ext-real Element of REAL

x2 . 1 is V31() real ext-real Element of REAL

x2 `2 is V31() real ext-real Element of REAL

x2 . 2 is V31() real ext-real Element of REAL

0.REAL 2 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)

2 |-> 0 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of 2 -tuples_on REAL

(Seg 2) --> 0 is non empty Relation-like Seg 2 -defined INT -valued RAT -valued {0} -valued Function-like total quasi_total finite complex-yielding V193() V194() V195() Element of bool [:(Seg 2),{0}:]

{0} is non empty finite V40() V202() V203() V204() V205() V206() V207() left_end right_end bounded_below bounded_above real-bounded set

[:(Seg 2),{0}:] is non empty INT -valued RAT -valued finite complex-yielding V193() V194() V195() set

bool [:(Seg 2),{0}:] is non empty finite V40() set

0.REAL 2 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)

2 |-> 0 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of 2 -tuples_on REAL

(Seg 2) --> 0 is non empty Relation-like Seg 2 -defined INT -valued RAT -valued {0} -valued Function-like total quasi_total finite complex-yielding V193() V194() V195() Element of bool [:(Seg 2),{0}:]

{0} is non empty finite V40() V202() V203() V204() V205() V206() V207() left_end right_end bounded_below bounded_above real-bounded set

[:(Seg 2),{0}:] is non empty INT -valued RAT -valued finite complex-yielding V193() V194() V195() set

bool [:(Seg 2),{0}:] is non empty finite V40() set

x1 is Element of the carrier of (Euclid 2)

x2 is Element of the carrier of (Euclid 2)

dist (x1,x2) is V31() real ext-real Element of REAL

y1 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)

|.y1.| is V31() real ext-real non negative Element of REAL

sqr y1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL

Sum (sqr y1) is V31() real ext-real Element of REAL

sqrt (Sum (sqr y1)) is V31() real ext-real Element of REAL

y2 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)

y2 `1 is V31() real ext-real Element of REAL

y2 . 1 is V31() real ext-real Element of REAL

y2 `2 is V31() real ext-real Element of REAL

y2 . 2 is V31() real ext-real Element of REAL

(Pitag_dist 2) . (x1,x2) is set

[x1,x2] is set

{x1,x2} is non empty finite set

{x1} is non empty finite set

{{x1,x2},{x1}} is non empty finite V40() set

(Pitag_dist 2) . [x1,x2] is V31() real ext-real set

y1 `1 is V31() real ext-real Element of REAL

y1 . 1 is V31() real ext-real Element of REAL

(y2 `1) - (y1 `1) is V31() real ext-real Element of REAL

((y2 `1) - (y1 `1)) ^2 is V31() real ext-real Element of REAL

((y2 `1) - (y1 `1)) * ((y2 `1) - (y1 `1)) is V31() real ext-real set

y1 `2 is V31() real ext-real Element of REAL

y1 . 2 is V31() real ext-real Element of REAL

(y2 `2) - (y1 `2) is V31() real ext-real Element of REAL

((y2 `2) - (y1 `2)) ^2 is V31() real ext-real Element of REAL

((y2 `2) - (y1 `2)) * ((y2 `2) - (y1 `2)) is V31() real ext-real set

(((y2 `1) - (y1 `1)) ^2) + (((y2 `2) - (y1 `2)) ^2) is V31() real ext-real Element of REAL

sqrt ((((y2 `1) - (y1 `1)) ^2) + (((y2 `2) - (y1 `2)) ^2)) is V31() real ext-real Element of REAL

(y1 `1) ^2 is V31() real ext-real Element of REAL

(y1 `1) * (y1 `1) is V31() real ext-real set

(y1 `2) ^2 is V31() real ext-real Element of REAL

(y1 `2) * (y1 `2) is V31() real ext-real set

((y1 `1) ^2) + ((y1 `2) ^2) is V31() real ext-real Element of REAL

sqrt (((y1 `1) ^2) + ((y1 `2) ^2)) is V31() real ext-real Element of REAL

x1 is V31() real ext-real Element of REAL

x2 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)

x1 * x2 is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like complex-yielding V193() V194() Element of the carrier of (TOP-REAL 2)

x1 * x2 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V193() V194() FinSequence of REAL

x2 `1 is V31() real ext-real Element of REAL

x2 . 1 is V31() real ext-real Element of REAL

x1 * (x2 `1) is V31() real ext-real Element of REAL

x2 `2 is V31() real ext-real Element of REAL

x2 . 2 is V31() real ext-real Element of REAL

x1 * (x2