:: JGRAPH_2 semantic presentation

REAL is non empty V38() set

NAT is non empty epsilon-transitive epsilon-connected ordinal Element of K19(REAL)

K19(REAL) is set

COMPLEX is non empty V38() set

omega is non empty epsilon-transitive epsilon-connected ordinal set

K19(omega) is set

K19(NAT) is set

RAT is non empty V38() set

INT is non empty V38() set

K20(REAL,REAL) is set

K19(K20(REAL,REAL)) is set

K313() is non empty V78() L8()

the carrier of K313() is non empty set

K318() is non empty V78() V100() V101() V102() V104() V151() V152() V153() V154() V155() V156() L8()

K319() is non empty V78() V102() V104() V154() V155() V156() M14(K318())

K320() is non empty V78() V100() V102() V104() V154() V155() V156() V157() M17(K318(),K319())

K322() is non empty V78() V100() V102() V104() L8()

K323() is non empty V78() V100() V102() V104() V157() M14(K322())

K408() is non empty strict TopSpace-like V204() TopStruct

the carrier of K408() is non empty V131() set

1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real ext-real positive non negative Element of NAT

K20(1,1) is set

K19(K20(1,1)) is set

K20(K20(1,1),1) is set

K19(K20(K20(1,1),1)) is set

K20(K20(1,1),REAL) is set

K19(K20(K20(1,1),REAL)) is set

K20(K20(REAL,REAL),REAL) is set

K19(K20(K20(REAL,REAL),REAL)) is set

2 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real ext-real positive non negative Element of NAT

K20(2,2) is set

K20(K20(2,2),REAL) is set

K19(K20(K20(2,2),REAL)) is set

RealSpace is strict V204() MetrStruct

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

TOP-REAL 2 is non empty V76() V141() V142() TopSpace-like V206() V207() V208() V209() V210() V211() V212() V218() L16()

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

K20( the carrier of (TOP-REAL 2),REAL) is set

K19(K20( the carrier of (TOP-REAL 2),REAL)) is set

K19( the carrier of (TOP-REAL 2)) is set

ExtREAL is non empty set

{} is set

the empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() real ext-real non positive non negative set is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() real ext-real non positive non negative set

the carrier of R^1 is non empty V131() set

K19( the carrier of R^1) is set

0 is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real Element of NAT

0. (TOP-REAL 2) is Relation-like Function-like V45(2) FinSequence-like V57( TOP-REAL 2) V119() V120() V121() Element of the carrier of (TOP-REAL 2)

the ZeroF of (TOP-REAL 2) is Relation-like Function-like V45(2) FinSequence-like V119() V120() V121() Element of the carrier of (TOP-REAL 2)

|[0,0]| is Relation-like Function-like V45(2) FinSequence-like V119() V120() V121() Element of the carrier of (TOP-REAL 2)

I[01] is non empty strict TopSpace-like V204() SubSpace of R^1

the carrier of I[01] is non empty V131() set

K20( the carrier of I[01], the carrier of (TOP-REAL 2)) is set

K19(K20( the carrier of I[01], the carrier of (TOP-REAL 2))) is set

- 1 is V28() real ext-real non positive set

proj1 is Relation-like the carrier of (TOP-REAL 2) -defined REAL -valued Function-like non empty total V18( the carrier of (TOP-REAL 2), REAL ) V119() V120() V121() continuous Element of K19(K20( the carrier of (TOP-REAL 2),REAL))

proj2 is Relation-like the carrier of (TOP-REAL 2) -defined REAL -valued Function-like non empty total V18( the carrier of (TOP-REAL 2), REAL ) V119() V120() V121() continuous Element of K19(K20( the carrier of (TOP-REAL 2),REAL))

K0 is non empty TopSpace-like TopStruct

the carrier of K0 is non empty set

[#] K0 is non empty non proper open closed Element of K19( the carrier of K0)

K19( the carrier of K0) is set

f is non empty TopSpace-like TopStruct

the carrier of f is non empty set

K20( the carrier of K0, the carrier of f) is set

K19(K20( the carrier of K0, the carrier of f)) is set

g is non empty TopSpace-like TopStruct

the carrier of g is non empty set

K20( the carrier of g, the carrier of f) is set

K19(K20( the carrier of g, the carrier of f)) is set

[#] g is non empty non proper open closed Element of K19( the carrier of g)

K19( the carrier of g) is set

([#] K0) \/ ([#] g) is set

([#] K0) /\ ([#] g) is Element of K19( the carrier of g)

a is non empty TopSpace-like TopStruct

the carrier of a is non empty set

K19( the carrier of a) is set

[#] a is non empty non proper open closed Element of K19( the carrier of a)

K20( the carrier of a, the carrier of f) is set

K19(K20( the carrier of a, the carrier of f)) is set

b is Relation-like the carrier of K0 -defined the carrier of f -valued Function-like non empty total V18( the carrier of K0, the carrier of f) Element of K19(K20( the carrier of K0, the carrier of f))

c is Relation-like the carrier of g -defined the carrier of f -valued Function-like non empty total V18( the carrier of g, the carrier of f) Element of K19(K20( the carrier of g, the carrier of f))

b +* c is Relation-like Function-like set

d is Element of K19( the carrier of a)

O is Element of K19( the carrier of a)

dom c is Element of K19( the carrier of g)

dom b is Element of K19( the carrier of K0)

dom (b +* c) is set

rng (b +* c) is set

rng b is Element of K19( the carrier of f)

K19( the carrier of f) is set

rng c is Element of K19( the carrier of f)

(rng b) \/ (rng c) is Element of K19( the carrier of f)

A is Relation-like the carrier of a -defined the carrier of f -valued Function-like non empty total V18( the carrier of a, the carrier of f) Element of K19(K20( the carrier of a, the carrier of f))

B is Element of K19( the carrier of f)

A " B is Element of K19( the carrier of a)

b " B is Element of K19( the carrier of K0)

c " B is Element of K19( the carrier of g)

dom A is Element of K19( the carrier of a)

(dom b) \/ (dom c) is set

g2 is set

(A " B) /\ ([#] g) is Element of K19( the carrier of g)

A . g2 is set

c . g2 is set

c . g2 is set

A . g2 is set

g2 is set

A . g2 is set

b . g2 is set

c . g2 is set

g2 is set

(A " B) /\ ([#] K0) is Element of K19( the carrier of K0)

A . g2 is set

b . g2 is set

b . g2 is set

A . g2 is set

ff is Element of K19( the carrier of a)

g2 is Element of K19( the carrier of a)

g2 /\ ([#] K0) is Element of K19( the carrier of K0)

f2 is Element of K19( the carrier of a)

g2 is Element of K19( the carrier of a)

g2 /\ ([#] g) is Element of K19( the carrier of g)

(A " B) /\ (([#] K0) \/ ([#] g)) is Element of K19( the carrier of a)

((A " B) /\ ([#] K0)) \/ ((A " B) /\ ([#] g)) is set

(b " B) \/ (c " B) is set

K0 is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real Element of NAT

Euclid K0 is non empty strict Reflexive discerning V197() triangle MetrStruct

REAL K0 is non empty FinSequence-membered FinSequenceSet of REAL

K0 -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL

Pitag_dist K0 is Relation-like K20((REAL K0),(REAL K0)) -defined REAL -valued Function-like total V18(K20((REAL K0),(REAL K0)), REAL ) V119() V120() V121() Element of K19(K20(K20((REAL K0),(REAL K0)),REAL))

K20((REAL K0),(REAL K0)) is set

K20(K20((REAL K0),(REAL K0)),REAL) is set

K19(K20(K20((REAL K0),(REAL K0)),REAL)) is set

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

the carrier of (Euclid K0) is non empty set

TOP-REAL K0 is non empty V76() V141() V142() TopSpace-like V206() V207() V208() V209() V210() V211() V212() V218() L16()

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

f is Element of the carrier of (Euclid K0)

g is Relation-like Function-like V45(K0) FinSequence-like V119() V120() V121() Element of the carrier of (TOP-REAL K0)

a is V28() real ext-real set

Ball (f,a) is Element of K19( the carrier of (Euclid K0))

K19( the carrier of (Euclid K0)) is set

{ b

{ b

b is set

c is Element of the carrier of (Euclid K0)

dist (f,c) is V28() real ext-real Element of REAL

d is Relation-like Function-like V45(K0) FinSequence-like V119() V120() V121() Element of the carrier of (TOP-REAL K0)

g - d is Relation-like Function-like V45(K0) FinSequence-like V119() V120() V121() Element of the carrier of (TOP-REAL K0)

K296(g,d) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V119() V120() V121() FinSequence of REAL

|.(g - d).| is V28() real ext-real non negative Element of REAL

K300((g - d)) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V119() V120() V121() FinSequence of REAL

K306(K300((g - d))) is V28() real ext-real Element of REAL

sqrt K306(K300((g - d))) is V28() real ext-real Element of REAL

b is set

c is Relation-like Function-like V45(K0) FinSequence-like V119() V120() V121() Element of the carrier of (TOP-REAL K0)

g - c is Relation-like Function-like V45(K0) FinSequence-like V119() V120() V121() Element of the carrier of (TOP-REAL K0)

K296(g,c) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V119() V120() V121() FinSequence of REAL

|.(g - c).| is V28() real ext-real non negative Element of REAL

K300((g - c)) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V119() V120() V121() FinSequence of REAL

K306(K300((g - c))) is V28() real ext-real Element of REAL

sqrt K306(K300((g - c))) is V28() real ext-real Element of REAL

d is Element of the carrier of (Euclid K0)

dist (f,d) is V28() real ext-real Element of REAL

(0. (TOP-REAL 2)) `1 is V28() real ext-real Element of REAL

K526((0. (TOP-REAL 2)),1) is V28() real ext-real Element of REAL

(0. (TOP-REAL 2)) `2 is V28() real ext-real Element of REAL

K526((0. (TOP-REAL 2)),2) is V28() real ext-real Element of REAL

1.REAL 2 is Relation-like Function-like V45(2) FinSequence-like V119() V120() V121() Element of the carrier of (TOP-REAL 2)

1* 2 is Relation-like NAT -defined REAL -valued Function-like V45(2) FinSequence-like V119() V120() V121() Element of REAL 2

REAL 2 is non empty FinSequence-membered FinSequenceSet of REAL

2 -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL

2 |-> 1 is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V119() V120() V121() Element of 2 -tuples_on REAL

<*1,1*> is set

(1.REAL 2) `1 is V28() real ext-real Element of REAL

K526((1.REAL 2),1) is V28() real ext-real Element of REAL

(1.REAL 2) `2 is V28() real ext-real Element of REAL

K526((1.REAL 2),2) is V28() real ext-real Element of REAL

dom proj1 is Element of K19( the carrier of (TOP-REAL 2))

dom proj2 is Element of K19( the carrier of (TOP-REAL 2))

K0 is Relation-like Function-like V45(2) FinSequence-like V119() V120() V121() Element of the carrier of (TOP-REAL 2)

proj1 . K0 is V28() real ext-real Element of REAL

proj2 . K0 is V28() real ext-real Element of REAL

|[(proj1 . K0),(proj2 . K0)]| is Relation-like Function-like V45(2) FinSequence-like V119() V120() V121() Element of the carrier of (TOP-REAL 2)

K0 `1 is V28() real ext-real Element of REAL

K526(K0,1) is V28() real ext-real Element of REAL

K0 `2 is V28() real ext-real Element of REAL

K526(K0,2) is V28() real ext-real Element of REAL

|[(K0 `1),(K0 `2)]| is Relation-like Function-like V45(2) FinSequence-like V119() V120() V121() Element of the carrier of (TOP-REAL 2)

{(0. (TOP-REAL 2))} is Element of K19( the carrier of (TOP-REAL 2))

K0 is Element of K19( the carrier of (TOP-REAL 2))

K0 ` is Element of K19( the carrier of (TOP-REAL 2))

the carrier of (TOP-REAL 2) \ K0 is Element of K19( the carrier of (TOP-REAL 2))

|[0,1]| is Relation-like Function-like V45(2) FinSequence-like V119() V120() V121() Element of the carrier of (TOP-REAL 2)

|[0,1]| `2 is V28() real ext-real Element of REAL

K526(|[0,1]|,2) is V28() real ext-real Element of REAL

K0 is non empty TopSpace-like TopStruct

the carrier of K0 is non empty set

f is non empty TopSpace-like TopStruct

the carrier of f is non empty set

K20( the carrier of K0, the carrier of f) is set

K19(K20( the carrier of K0, the carrier of f)) is set

K19( the carrier of f) is set

K19( the carrier of K0) is set

g is Relation-like the carrier of K0 -defined the carrier of f -valued Function-like non empty total V18( the carrier of K0, the carrier of f) Element of K19(K20( the carrier of K0, the carrier of f))

[#] f is non empty non proper open closed Element of K19( the carrier of f)

dom g is Element of K19( the carrier of K0)

a is Element of the carrier of K0

g . a is Element of the carrier of f

b is Element of K19( the carrier of f)

g " b is Element of K19( the carrier of K0)

g .: (g " b) is Element of K19( the carrier of f)

a is Element of K19( the carrier of f)

g " a is Element of K19( the carrier of K0)

b is set

g . b is set

c is Element of the carrier of K0

d is Element of K19( the carrier of K0)

g .: d is Element of K19( the carrier of f)

g " (g .: d) is Element of K19( the carrier of K0)

c is Element of K19( the carrier of K0)

d is Element of K19( the carrier of K0)

K0 is Relation-like Function-like V45(2) FinSequence-like V119() V120() V121() Element of the carrier of (TOP-REAL 2)

K0 `1 is V28() real ext-real Element of REAL

K526(K0,1) is V28() real ext-real Element of REAL

K0 `2 is V28() real ext-real Element of REAL

K526(K0,2) is V28() real ext-real Element of REAL

f is Element of K19( the carrier of (TOP-REAL 2))

the topology of (TOP-REAL 2) is non empty Element of K19(K19( the carrier of (TOP-REAL 2)))

K19(K19( the carrier of (TOP-REAL 2))) is set

TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) is non empty strict TopSpace-like TopStruct

the carrier of TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) is non empty set

K19( the carrier of TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #)) is set

Euclid 2 is non empty strict Reflexive discerning V197() triangle MetrStruct

Pitag_dist 2 is Relation-like K20((REAL 2),(REAL 2)) -defined REAL -valued Function-like total V18(K20((REAL 2),(REAL 2)), REAL ) V119() V120() V121() Element of K19(K20(K20((REAL 2),(REAL 2)),REAL))

K20((REAL 2),(REAL 2)) is set

K20(K20((REAL 2),(REAL 2)),REAL) is set

K19(K20(K20((REAL 2),(REAL 2)),REAL)) is set

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

the carrier of (Euclid 2) is non empty set

TopSpaceMetr (Euclid 2) is TopStruct

g is Element of K19( the carrier of TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #))

a is Element of the carrier of (Euclid 2)

b is V28() real ext-real set

Ball (a,b) is Element of K19( the carrier of (Euclid 2))

K19( the carrier of (Euclid 2)) is set

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

b / (sqrt 2) is V28() real ext-real Element of REAL

(sqrt 2) " is V28() real ext-real set

b * ((sqrt 2) ") is V28() real ext-real set

{ b

(K0 `1) - (b / (sqrt 2)) is V28() real ext-real Element of REAL

- (b / (sqrt 2)) is V28() real ext-real set

(K0 `1) + (- (b / (sqrt 2))) is V28() real ext-real set

(K0 `1) + (b / (sqrt 2)) is V28() real ext-real Element of REAL

(K0 `2) - (b / (sqrt 2)) is V28() real ext-real Element of REAL

(K0 `2) + (- (b / (sqrt 2))) is V28() real ext-real set

(K0 `2) + (b / (sqrt 2)) is V28() real ext-real Element of REAL

{ b

d is set

O is Relation-like Function-like V45(2) FinSequence-like V119() V120() V121() Element of the carrier of (TOP-REAL 2)

O `1 is V28() real ext-real Element of REAL

K526(O,1) is V28() real ext-real Element of REAL

O `2 is V28() real ext-real Element of REAL

K526(O,2) is V28() real ext-real Element of REAL

((K0 `1) + (b / (sqrt 2))) - (b / (sqrt 2)) is V28() real ext-real Element of REAL

((K0 `1) + (b / (sqrt 2))) + (- (b / (sqrt 2))) is V28() real ext-real set

(O `1) - (b / (sqrt 2)) is V28() real ext-real Element of REAL

(O `1) + (- (b / (sqrt 2))) is V28() real ext-real set

(K0 `1) - (O `1) is V28() real ext-real Element of REAL

- (O `1) is V28() real ext-real set

(K0 `1) + (- (O `1)) is V28() real ext-real set

- (b / (sqrt 2)) is V28() real ext-real Element of REAL

(O `1) + (- (b / (sqrt 2))) is V28() real ext-real Element of REAL

((O `1) + (- (b / (sqrt 2)))) - (O `1) is V28() real ext-real Element of REAL

((O `1) + (- (b / (sqrt 2)))) + (- (O `1)) is V28() real ext-real set

((K0 `2) + (b / (sqrt 2))) - (b / (sqrt 2)) is V28() real ext-real Element of REAL

((K0 `2) + (b / (sqrt 2))) + (- (b / (sqrt 2))) is V28() real ext-real set

(O `2) - (b / (sqrt 2)) is V28() real ext-real Element of REAL

(O `2) + (- (b / (sqrt 2))) is V28() real ext-real set

(K0 `2) - (O `2) is V28() real ext-real Element of REAL

- (O `2) is V28() real ext-real set

(K0 `2) + (- (O `2)) is V28() real ext-real set

(O `2) + (- (b / (sqrt 2))) is V28() real ext-real Element of REAL

((O `2) + (- (b / (sqrt 2)))) - (O `2) is V28() real ext-real Element of REAL

((O `2) + (- (b / (sqrt 2)))) + (- (O `2)) is V28() real ext-real set

(O `2) + (b / (sqrt 2)) is V28() real ext-real Element of REAL

((K0 `2) - (b / (sqrt 2))) + (b / (sqrt 2)) is V28() real ext-real Element of REAL

((O `2) + (b / (sqrt 2))) - (O `2) is V28() real ext-real Element of REAL

((O `2) + (b / (sqrt 2))) + (- (O `2)) is V28() real ext-real set

(b / (sqrt 2)) ^2 is V28() real ext-real Element of REAL

(b / (sqrt 2)) * (b / (sqrt 2)) is V28() real ext-real set

((K0 `2) - (O `2)) ^2 is V28() real ext-real Element of REAL

((K0 `2) - (O `2)) * ((K0 `2) - (O `2)) is V28() real ext-real set

b ^2 is V28() real ext-real set

b * b is V28() real ext-real set

(sqrt 2) ^2 is V28() real ext-real Element of REAL

(sqrt 2) * (sqrt 2) is V28() real ext-real set

(b ^2) / ((sqrt 2) ^2) is V28() real ext-real Element of REAL

((sqrt 2) ^2) " is V28() real ext-real set

(b ^2) * (((sqrt 2) ^2) ") is V28() real ext-real set

(b ^2) / 2 is V28() real ext-real Element of REAL

2 " is non empty V28() real ext-real positive non negative set

(b ^2) * (2 ") is V28() real ext-real set

((b / (sqrt 2)) ^2) + ((b / (sqrt 2)) ^2) is V28() real ext-real Element of REAL

(O `1) + (b / (sqrt 2)) is V28() real ext-real Element of REAL

((K0 `1) - (b / (sqrt 2))) + (b / (sqrt 2)) is V28() real ext-real Element of REAL

((O `1) + (b / (sqrt 2))) - (O `1) is V28() real ext-real Element of REAL

((O `1) + (b / (sqrt 2))) + (- (O `1)) is V28() real ext-real set

K0 - O is Relation-like Function-like V45(2) FinSequence-like V119() V120() V121() Element of the carrier of (TOP-REAL 2)

K296(K0,O) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V119() V120() V121() FinSequence of REAL

(K0 - O) `2 is V28() real ext-real Element of REAL

K526((K0 - O),2) is V28() real ext-real Element of REAL

((K0 `1) - (O `1)) ^2 is V28() real ext-real Element of REAL

((K0 `1) - (O `1)) * ((K0 `1) - (O `1)) is V28() real ext-real set

|.(K0 - O).| is V28() real ext-real non negative Element of REAL

K300((K0 - O)) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V119() V120() V121() FinSequence of REAL

K306(K300((K0 - O))) is V28() real ext-real Element of REAL

sqrt K306(K300((K0 - O))) is V28() real ext-real Element of REAL

|.(K0 - O).| ^2 is V28() real ext-real Element of REAL

|.(K0 - O).| * |.(K0 - O).| is V28() real ext-real non negative set

(K0 - O) `1 is V28() real ext-real Element of REAL

K526((K0 - O),1) is V28() real ext-real Element of REAL

((K0 - O) `1) ^2 is V28() real ext-real Element of REAL

((K0 - O) `1) * ((K0 - O) `1) is V28() real ext-real set

((K0 - O) `2) ^2 is V28() real ext-real Element of REAL

((K0 - O) `2) * ((K0 - O) `2) is V28() real ext-real set

(((K0 - O) `1) ^2) + (((K0 - O) `2) ^2) is V28() real ext-real Element of REAL

f is non empty TopSpace-like TopStruct

the carrier of f is non empty set

K19( the carrier of f) is set

g is non empty TopSpace-like TopStruct

the carrier of g is non empty set

K19( the carrier of g) is set

K0 is non empty TopSpace-like TopStruct

the carrier of K0 is non empty set

K20( the carrier of K0, the carrier of f) is set

K19(K20( the carrier of K0, the carrier of f)) is set

K20( the carrier of K0, the carrier of g) is set

K19(K20( the carrier of K0, the carrier of g)) is set

a is Element of K19( the carrier of f)

f | a is strict TopSpace-like SubSpace of f

the carrier of (f | a) is set

b is Element of K19( the carrier of g)

g | b is strict TopSpace-like SubSpace of g

the carrier of (g | b) is set

K20( the carrier of (f | a), the carrier of (g | b)) is set

K19(K20( the carrier of (f | a), the carrier of (g | b))) is set

c is Relation-like the carrier of K0 -defined the carrier of f -valued Function-like non empty total V18( the carrier of K0, the carrier of f) Element of K19(K20( the carrier of K0, the carrier of f))

rng c is Element of K19( the carrier of f)

d is Relation-like the carrier of (f | a) -defined the carrier of (g | b) -valued Function-like V18( the carrier of (f | a), the carrier of (g | b)) Element of K19(K20( the carrier of (f | a), the carrier of (g | b)))

d * c is Relation-like the carrier of K0 -defined the carrier of (g | b) -valued Function-like Element of K19(K20( the carrier of K0, the carrier of (g | b)))

K20( the carrier of K0, the carrier of (g | b)) is set

K19(K20( the carrier of K0, the carrier of (g | b))) is set

dom c is Element of K19( the carrier of K0)

K19( the carrier of K0) is set

[#] (f | a) is non proper open closed Element of K19( the carrier of (f | a))

K19( the carrier of (f | a)) is set

K20( the carrier of K0, the carrier of (f | a)) is set

K19(K20( the carrier of K0, the carrier of (f | a))) is set

I is non empty Element of K19( the carrier of f)

f | I is non empty strict TopSpace-like SubSpace of f

A is non empty TopSpace-like TopStruct

the carrier of A is non empty set

K20( the carrier of K0, the carrier of A) is set

K19(K20( the carrier of K0, the carrier of A)) is set

O is Relation-like the carrier of K0 -defined the carrier of (f | a) -valued Function-like V18( the carrier of K0, the carrier of (f | a)) Element of K19(K20( the carrier of K0, the carrier of (f | a)))

B is non empty Element of K19( the carrier of g)

g | B is non empty strict TopSpace-like SubSpace of g

D is non empty TopSpace-like TopStruct

the carrier of D is non empty set

K20( the carrier of A, the carrier of D) is set

K19(K20( the carrier of A, the carrier of D)) is set

[#] (g | b) is non proper open closed Element of K19( the carrier of (g | b))

K19( the carrier of (g | b)) is set

C is Relation-like the carrier of K0 -defined the carrier of A -valued Function-like non empty total V18( the carrier of K0, the carrier of A) Element of K19(K20( the carrier of K0, the carrier of A))

ff is Relation-like the carrier of A -defined the carrier of D -valued Function-like non empty total V18( the carrier of A, the carrier of D) Element of K19(K20( the carrier of A, the carrier of D))

ff * C is Relation-like the carrier of K0 -defined the carrier of D -valued Function-like non empty total V18( the carrier of K0, the carrier of D) Element of K19(K20( the carrier of K0, the carrier of D))

K20( the carrier of K0, the carrier of D) is set

K19(K20( the carrier of K0, the carrier of D)) is set

d * O is Relation-like the carrier of K0 -defined the carrier of (g | b) -valued Function-like Element of K19(K20( the carrier of K0, the carrier of (g | b)))

f2 is Relation-like the carrier of K0 -defined the carrier of g -valued Function-like non empty total V18( the carrier of K0, the carrier of g) Element of K19(K20( the carrier of K0, the carrier of g))

NonZero (TOP-REAL 2) is Element of K19( the carrier of (TOP-REAL 2))

[#] (TOP-REAL 2) is non empty non proper open closed Element of K19( the carrier of (TOP-REAL 2))

{(0. (TOP-REAL 2))} is set

([#] (TOP-REAL 2)) \ {(0. (TOP-REAL 2))} is Element of K19( the carrier of (TOP-REAL 2))

K20((NonZero (TOP-REAL 2)),(NonZero (TOP-REAL 2))) is set

K19(K20((NonZero (TOP-REAL 2)),(NonZero (TOP-REAL 2)))) is set

K0 is non empty set

f is Element of K0

g is Relation-like Function-like V45(2) FinSequence-like V119() V120() V121() Element of the carrier of (TOP-REAL 2)

g `2 is V28() real ext-real Element of REAL

K526(g,2) is V28() real ext-real Element of REAL

g `1 is V28() real ext-real Element of REAL

K526(g,1) is V28() real ext-real Element of REAL

- (g `1) is V28() real ext-real Element of REAL

1 / (g `1) is V28() real ext-real Element of REAL

(g `1) " is V28() real ext-real set

1 * ((g `1) ") is V28() real ext-real set

(g `2) / (g `1) is V28() real ext-real Element of REAL

(g `2) * ((g `1) ") is V28() real ext-real set

((g `2) / (g `1)) / (g `1) is V28() real ext-real Element of REAL

((g `2) / (g `1)) * ((g `1) ") is V28() real ext-real set

|[(1 / (g `1)),(((g `2) / (g `1)) / (g `1))]| is Relation-like Function-like V45(2) FinSequence-like V119() V120() V121() Element of the carrier of (TOP-REAL 2)

(1 / (g `1)) * (g `1) is V28() real ext-real Element of REAL

a is Element of K0

b is Relation-like Function-like V45(2) FinSequence-like V119() V120() V121() Element of the carrier of (TOP-REAL 2)

b `2 is V28() real ext-real Element of REAL

K526(b,2) is V28() real ext-real Element of REAL

b `1 is V28() real ext-real Element of REAL

K526(b,1) is V28() real ext-real Element of REAL

- (b `1) is V28() real ext-real Element of REAL

1 / (b `1) is V28() real ext-real Element of REAL

(b `1) " is V28() real ext-real set

1 * ((b `1) ") is V28() real ext-real set

(b `2) / (b `1) is V28() real ext-real Element of REAL

(b `2) * ((b `1) ") is V28() real ext-real set

((b `2) / (b `1)) / (b `1) is V28() real ext-real Element of REAL

((b `2) / (b `1)) * ((b `1) ") is V28() real ext-real set

|[(1 / (b `1)),(((b `2) / (b `1)) / (b `1))]| is Relation-like Function-like V45(2) FinSequence-like V119() V120() V121() Element of the carrier of (TOP-REAL 2)

(b `1) / (b `2) is V28() real ext-real Element of REAL

(b `2) " is V28() real ext-real set

(b `1) * ((b `2) ") is V28() real ext-real set

((b `1) / (b `2)) / (b `2) is V28() real ext-real Element of REAL

((b `1) / (b `2)) * ((b `2) ") is V28() real ext-real set

1 / (b `2) is V28() real ext-real Element of REAL

1 * ((b `2) ") is V28() real ext-real set

|[(((b `1) / (b `2)) / (b `2)),(1 / (b `2))]| is Relation-like Function-like V45(2) FinSequence-like V119() V120() V121() Element of the carrier of (TOP-REAL 2)

g is Relation-like Function-like V45(2) FinSequence-like V119() V120() V121() Element of the carrier of (TOP-REAL 2)

g `2 is V28() real ext-real Element of REAL

K526(g,2) is V28() real ext-real Element of REAL

g `1 is V28() real ext-real Element of REAL

K526(g,1) is V28() real ext-real Element of REAL

- (g `1) is V28() real ext-real Element of REAL

(g `1) / (g `2) is V28() real ext-real Element of REAL

(g `2) " is V28() real ext-real set

(g `1) * ((g `2) ") is V28() real ext-real set

((g `1) / (g `2)) / (g `2) is V28() real ext-real Element of REAL

((g `1) / (g `2)) * ((g `2) ") is V28() real ext-real set

1 / (g `2) is V28() real ext-real Element of REAL

1 * ((g `2) ") is V28() real ext-real set

|[(((g `1) / (g `2)) / (g `2)),(1 / (g `2))]| is Relation-like Function-like V45(2) FinSequence-like V119() V120() V121() Element of the carrier of (TOP-REAL 2)

(1 / (g `2)) * (g `2) is V28() real ext-real Element of REAL

a is Element of K0

b is Relation-like Function-like V45(2) FinSequence-like V119() V120() V121() Element of the carrier of (TOP-REAL 2)

b `2 is V28() real ext-real Element of REAL

K526(b,2) is V28() real ext-real Element of REAL

b `1 is V28() real ext-real Element of REAL

K526(b,1) is V28() real ext-real Element of REAL

- (b `1) is V28() real ext-real Element of REAL

1 / (b `1) is V28() real ext-real Element of REAL

(b `1) " is V28() real ext-real set

1 * ((b `1) ") is V28() real ext-real set

(b `2) / (b `1) is V28() real ext-real Element of REAL

(b `2) * ((b `1) ") is V28() real ext-real set

((b `2) / (b `1)) / (b `1) is V28() real ext-real Element of REAL

((b `2) / (b `1)) * ((b `1) ") is V28() real ext-real set

|[(1 / (b `1)),(((b `2) / (b `1)) / (b `1))]| is Relation-like Function-like V45(2) FinSequence-like V119() V120() V121() Element of the carrier of (TOP-REAL 2)

(b `1) / (b `2) is V28() real ext-real Element of REAL

(b `2) " is V28() real ext-real set

(b `1) * ((b `2) ") is V28() real ext-real set

((b `1) / (b `2)) / (b `2) is V28() real ext-real Element of REAL

((b `1) / (b `2)) * ((b `2) ") is V28() real ext-real set

1 / (b `2) is V28() real ext-real Element of REAL

1 * ((b `2) ") is V28() real ext-real set

|[(((b `1) / (b `2)) / (b `2)),(1 / (b `2))]| is Relation-like Function-like V45(2) FinSequence-like V119() V120() V121() Element of the carrier of (TOP-REAL 2)

g is Relation-like Function-like V45(2) FinSequence-like V119() V120() V121() Element of the carrier of (TOP-REAL 2)

g `2 is V28() real ext-real Element of REAL

K526(g,2) is V28() real ext-real Element of REAL

g `1 is V28() real ext-real Element of REAL

K526(g,1) is V28() real ext-real Element of REAL

- (g `1) is V28() real ext-real Element of REAL

g is Relation-like Function-like V45(2) FinSequence-like V119() V120() V121() Element of the carrier of (TOP-REAL 2)

g `2 is V28() real ext-real Element of REAL

K526(g,2) is V28() real ext-real Element of REAL

g `1 is V28() real ext-real Element of REAL

K526(g,1) is V28() real ext-real Element of REAL

- (g `1) is V28() real ext-real Element of REAL

a is Element of K0

b is Element of K0

K20(K0,K0) is set

K19(K20(K0,K0)) is set

f is Relation-like K0 -defined K0 -valued Function-like non empty total V18(K0,K0) Element of K19(K20(K0,K0))

f is Relation-like K0 -defined K0 -valued Function-like non empty total V18(K0,K0) Element of K19(K20(K0,K0))

g is Relation-like Function-like V45(2) FinSequence-like V119() V120() V121() Element of the carrier of (TOP-REAL 2)

g `2 is V28() real ext-real Element of REAL

K526(g,2) is V28() real ext-real Element of REAL

g `1 is V28() real ext-real Element of REAL

K526(g,1) is V28() real ext-real Element of REAL

- (g `1) is V28() real ext-real Element of REAL

f . g is set

1 / (g `1) is V28() real ext-real Element of REAL

(g `1) " is V28() real ext-real set

1 * ((g `1) ") is V28() real ext-real set

(g `2) / (g `1) is V28() real ext-real Element of REAL

(g `2) * ((g `1) ") is V28() real ext-real set

((g `2) / (g `1)) / (g `1) is V28() real ext-real Element of REAL

((g `2) / (g `1)) * ((g `1) ") is V28() real ext-real set

|[(1 / (g `1)),(((g `2) / (g `1)) / (g `1))]| is Relation-like Function-like V45(2) FinSequence-like V119() V120() V121() Element of the carrier of (TOP-REAL 2)

(g `1) / (g `2) is V28() real ext-real Element of REAL

(g `2) " is V28() real ext-real set

(g `1) * ((g `2) ") is V28() real ext-real set

((g `1) / (g `2)) / (g `2) is V28() real ext-real Element of REAL

((g `1) / (g `2)) * ((g `2) ") is V28() real ext-real set

1 / (g `2) is V28() real ext-real Element of REAL

1 * ((g `2) ") is V28() real ext-real set

|[(((g `1) / (g `2)) / (g `2)),(1 / (g `2))]| is Relation-like Function-like V45(2) FinSequence-like V119() V120() V121() Element of the carrier of (TOP-REAL 2)

K0 is Relation-like NonZero (TOP-REAL 2) -defined NonZero (TOP-REAL 2) -valued Function-like total V18( NonZero (TOP-REAL 2), NonZero (TOP-REAL 2)) Element of K19(K20((NonZero (TOP-REAL 2)),(NonZero (TOP-REAL 2))))

f is Relation-like NonZero (TOP-REAL 2) -defined NonZero (TOP-REAL 2) -valued Function-like total V18( NonZero (TOP-REAL 2), NonZero (TOP-REAL 2)) Element of K19(K20((NonZero (TOP-REAL 2)),(NonZero (TOP-REAL 2))))

g is set

K0 . g is set

f . g is set

a is Relation-like Function-like V45(2) FinSequence-like V119() V120() V121() Element of the carrier of (TOP-REAL 2)

a `2 is V28() real ext-real Element of REAL

K526(a,2) is V28() real ext-real Element of REAL

a `1 is V28() real ext-real Element of REAL

K526(a,1) is V28() real ext-real Element of REAL

- (a `1) is V28() real ext-real Element of REAL

K0 . a is set

1 / (a `1) is V28() real ext-real Element of REAL

(a `1) " is V28() real ext-real set

1 * ((a `1) ") is V28() real ext-real set

(a `2) / (a `1) is V28() real ext-real Element of REAL

(a `2) * ((a `1) ") is V28() real ext-real set

((a `2) / (a `1)) / (a `1) is V28() real ext-real Element of REAL

((a `2) / (a `1)) * ((a `1) ") is V28() real ext-real set

|[(1 / (a `1)),(((a `2) / (a `1)) / (a `1))]| is Relation-like Function-like V45(2) FinSequence-like V119() V120() V121() Element of the carrier of (TOP-REAL 2)

a `2 is V28() real ext-real Element of REAL

K526(a,2) is V28() real ext-real Element of REAL

a `1 is V28() real ext-real Element of REAL

K526(a,1) is V28() real ext-real Element of REAL

- (a `1) is V28() real ext-real Element of REAL

K0 . a is set

(a `1) / (a `2) is V28() real ext-real Element of REAL

(a `2) " is V28() real ext-real set

(a `1) * ((a `2) ") is V28() real ext-real set

((a `1) / (a `2)) / (a `2) is V28() real ext-real Element of REAL

((a `1) / (a `2)) * ((a `2) ") is V28() real ext-real set

1 / (a `2) is V28() real ext-real Element of REAL

1 * ((a `2) ") is V28() real ext-real set

|[(((a `1) / (a `2)) / (a `2)),(1 / (a `2))]| is Relation-like Function-like V45(2) FinSequence-like V119() V120() V121() Element of the carrier of (TOP-REAL 2)

a `2 is V28() real ext-real Element of REAL

K526(a,2) is V28() real ext-real Element of REAL

a `1 is V28() real ext-real Element of REAL

K526(a,1) is V28() real ext-real Element of REAL

- (a `1) is V28() real ext-real Element of REAL

a `2 is V28() real ext-real Element of REAL

K526(a,2) is V28() real ext-real Element of REAL

a `1 is V28() real ext-real Element of REAL

K526(a,1) is V28() real ext-real Element of REAL

- (a `1) is V28() real ext-real Element of REAL

() is Relation-like NonZero (TOP-REAL 2) -defined NonZero (TOP-REAL 2) -valued Function-like total V18( NonZero (TOP-REAL 2), NonZero (TOP-REAL 2)) Element of K19(K20((NonZero (TOP-REAL 2)),(NonZero (TOP-REAL 2))))

K0 is Relation-like Function-like V45(2) FinSequence-like V119() V120() V121() Element of the carrier of (TOP-REAL 2)

K0 `2 is V28() real ext-real Element of REAL

K526(K0,2) is V28() real ext-real Element of REAL

K0 `1 is V28() real ext-real Element of REAL

K526(K0,1) is V28() real ext-real Element of REAL

- (K0 `1) is V28() real ext-real Element of REAL

- (K0 `2) is V28() real ext-real Element of REAL

- (- (K0 `1)) is V28() real ext-real Element of REAL

K0 is Relation-like Function-like V45(2) FinSequence-like V119() V120() V121() Element of the carrier of (TOP-REAL 2)

K0 `1 is V28() real ext-real Element of REAL

K526(K0,1) is V28() real ext-real Element of REAL

K0 `2 is V28() real ext-real Element of REAL

K526(K0,2) is V28() real ext-real Element of REAL

- (K0 `2) is V28() real ext-real Element of REAL

() . K0 is set

(K0 `1) / (K0 `2) is V28() real ext-real Element of REAL

(K0 `2) " is V28() real ext-real set

(K0 `1) * ((K0 `2) ") is V28() real ext-real set

((K0 `1) / (K0 `2)) / (K0 `2) is V28() real ext-real Element of REAL

((K0 `1) / (K0 `2)) * ((K0 `2) ") is V28() real ext-real set

1 / (K0 `2) is V28() real ext-real Element of REAL

1 * ((K0 `2) ") is V28() real ext-real set

|[(((K0 `1) / (K0 `2)) / (K0 `2)),(1 / (K0 `2))]| is Relation-like Function-like V45(2) FinSequence-like V119() V120() V121() Element of the carrier of (TOP-REAL 2)

1 / (K0 `1) is V28() real ext-real Element of REAL

(K0 `1) " is V28() real ext-real set

1 * ((K0 `1) ") is V28() real ext-real set

(K0 `2) / (K0 `1) is V28() real ext-real Element of REAL

(K0 `2) * ((K0 `1) ") is V28() real ext-real set

((K0 `2) / (K0 `1)) / (K0 `1) is V28() real ext-real Element of REAL

((K0 `2) / (K0 `1)) * ((K0 `1) ") is V28() real ext-real set

|[(1 / (K0 `1)),(((K0 `2) / (K0 `1)) / (K0 `1))]| is Relation-like Function-like V45(2) FinSequence-like V119() V120() V121() Element of the carrier of (TOP-REAL 2)

- (K0 `1) is V28() real ext-real Element of REAL

- (- (K0 `1)) is V28() real ext-real Element of REAL

(K0 `2) / (K0 `2) is V28() real ext-real Element of REAL

(K0 `2) * ((K0 `2) ") is V28() real ext-real set

- ((K0 `2) / (K0 `2)) is V28() real ext-real Element of REAL

(- ((K0 `2) / (K0 `2))) / (K0 `2) is V28() real ext-real Element of REAL

(- ((K0 `2) / (K0 `2))) * ((K0 `2) ") is V28() real ext-real set

- 1 is V28() real ext-real non positive Element of REAL

(- 1) / (K0 `2) is V28() real ext-real Element of REAL

(- 1) * ((K0 `2) ") is V28() real ext-real set

- (1 / (K0 `1)) is V28() real ext-real Element of REAL

((K0 `2) / (K0 `1)) / (- (K0 `1)) is V28() real ext-real Element of REAL

(- (K0 `1)) " is V28() real ext-real set

((K0 `2) / (K0 `1)) * ((- (K0 `1)) ") is V28() real ext-real set

- (((K0 `2) / (K0 `1)) / (- (K0 `1))) is V28() real ext-real Element of REAL

- (((K0 `2) / (K0 `1)) / (K0 `1)) is V28() real ext-real Element of REAL

- (- (((K0 `2) / (K0 `1)) / (K0 `1))) is V28() real ext-real Element of REAL

- (K0 `1) is V28() real ext-real Element of REAL

- (- (K0 `1)) is V28() real ext-real Element of REAL

(K0 `2) / (K0 `2) is V28() real ext-real Element of REAL

(K0 `2) * ((K0 `2) ") is V28() real ext-real set

- ((K0 `2) / (K0 `2)) is V28() real ext-real Element of REAL

(- ((K0 `2) / (K0 `2))) / (K0 `2) is V28() real ext-real Element of REAL

(- ((K0 `2) / (K0 `2))) * ((K0 `2) ") is V28() real ext-real set

- 1 is V28() real ext-real non positive Element of REAL

(- 1) / (K0 `2) is V28() real ext-real Element of REAL

(- 1) * ((K0 `2) ") is V28() real ext-real set

- (((K0 `1) / (K0 `2)) / (K0 `2)) is V28() real ext-real Element of REAL

((K0 `2) / (K0 `1)) / (- (K0 `1)) is V28() real ext-real Element of REAL

(- (K0 `1)) " is V28() real ext-real set

((K0 `2) / (K0 `1)) * ((- (K0 `1)) ") is V28() real ext-real set

- (((K0 `2) / (K0 `1)) / (- (K0 `1))) is V28() real ext-real Element of REAL

- (((K0 `2) / (K0 `1)) / (K0 `1)) is V28() real ext-real Element of REAL

- (- (((K0 `2) / (K0 `1)) / (K0 `1))) is V28() real ext-real Element of REAL

- (K0 `1) is V28() real ext-real Element of REAL

- (- (K0 `2)) is V28() real ext-real Element of REAL

{ b

K0 is Element of K19( the carrier of (TOP-REAL 2))

(TOP-REAL 2) | K0 is strict TopSpace-like SubSpace of TOP-REAL 2

the carrier of ((TOP-REAL 2) | K0) is set

K19( the carrier of ((TOP-REAL 2) | K0)) is set

f is Element of K19( the carrier of ((TOP-REAL 2) | K0))

() | f is Relation-like NonZero (TOP-REAL 2) -defined NonZero (TOP-REAL 2) -valued Function-like Element of K19(K20((NonZero (TOP-REAL 2)),(NonZero (TOP-REAL 2))))

rng (() | f) is Element of K19((NonZero (TOP-REAL 2)))

K19((NonZero (TOP-REAL 2))) is set

((TOP-REAL 2) | K0) | f is strict TopSpace-like SubSpace of (TOP-REAL 2) | K0

the carrier of (((TOP-REAL 2) | K0) | f) is set

[#] ((TOP-REAL 2) | K0) is non proper open closed Element of K19( the carrier of ((TOP-REAL 2) | K0))

g is Element of K19( the carrier of (TOP-REAL 2))

(TOP-REAL 2) | g is strict TopSpace-like SubSpace of TOP-REAL 2

the carrier of ((TOP-REAL 2) | g) is set

a is Relation-like Function-like V45(2) FinSequence-like V119() V120() V121() Element of the carrier of (TOP-REAL 2)

a `1 is V28() real ext-real Element of REAL

K526(a,1) is V28() real ext-real Element of REAL

[#] ((TOP-REAL 2) | g) is non proper open closed Element of K19( the carrier of ((TOP-REAL 2) | g))

K19( the carrier of ((TOP-REAL 2) | g)) is set

a `2 is V28() real ext-real Element of REAL

K526(a,2) is V28() real ext-real Element of REAL

b is Relation-like Function-like V45(2) FinSequence-like V119() V120() V121() Element of the carrier of (TOP-REAL 2)

b `2 is V28() real ext-real Element of REAL

K526(b,2) is V28() real ext-real Element of REAL

b `1 is V28() real ext-real Element of REAL

K526(b,1) is V28() real ext-real Element of REAL

- (b `1) is V28() real ext-real Element of REAL

b is Relation-like Function-like V45(2) FinSequence-like V119() V120() V121() Element of the carrier of (TOP-REAL 2)

b `2 is V28() real ext-real Element of REAL

K526(b,2) is V28() real ext-real Element of REAL

b `1 is V28() real ext-real Element of REAL

K526(b,1) is V28() real ext-real Element of REAL

- (b `1) is V28() real ext-real Element of REAL

a is set

dom (() | f) is Element of K19((NonZero (TOP-REAL 2)))

b is set

(() | f) . b is set

dom () is Element of K19((NonZero (TOP-REAL 2)))

(dom ()) /\ f is Element of K19( the carrier of ((TOP-REAL 2) | K0))

c is Relation-like Function-like V45(2) FinSequence-like V119() V120() V121() Element of the carrier of (TOP-REAL 2)

() . c is set

c `1 is V28() real ext-real Element of REAL

K526(c,1) is V28() real ext-real Element of REAL

1 / (c `1) is V28() real ext-real Element of REAL

(c `1) " is V28() real ext-real set

1 * ((c `1) ") is V28() real ext-real set

c `2 is V28() real ext-real Element of REAL

K526(c,2) is V28() real ext-real Element of REAL

(c `2) / (c `1) is V28() real ext-real Element of REAL

(c `2) * ((c `1) ") is V28() real ext-real set

((c `2) / (c `1)) / (c `1) is V28() real ext-real Element of REAL

((c `2) / (c `1)) * ((c `1) ") is V28() real ext-real set

|[(1 / (c `1)),(((c `2) / (c `1)) / (c `1))]| is Relation-like Function-like V45(2) FinSequence-like V119() V120() V121() Element of the carrier of (TOP-REAL 2)

d is Relation-like Function-like V45(2) FinSequence-like V119() V120() V121() Element of the carrier of (TOP-REAL 2)

d `2 is V28() real ext-real Element of REAL

K526(d,2) is V28() real ext-real Element of REAL

d `1 is V28() real ext-real Element of REAL

K526(d,1) is V28() real ext-real Element of REAL

- (d `1) is V28() real ext-real Element of REAL

[#] ((TOP-REAL 2) | g) is non proper open closed Element of K19( the carrier of ((TOP-REAL 2) | g))

K19( the carrier of ((TOP-REAL 2) | g)) is set

|[(1 / (c `1)),(((c `2) / (c `1)) / (c `1))]| `1 is V28() real ext-real Element of REAL

K526(|[(1 / (c `1)),(((c `2) / (c `1)) / (c `1))]|,1) is V28() real ext-real Element of REAL

0 * (c `1) is V28() real ext-real Element of REAL

(1 / (c `1)) * (c `1) is V28() real ext-real Element of REAL

(c `1) / (c `1) is V28() real ext-real Element of REAL

(c `1) * ((c `1) ") is V28() real ext-real set

1 * (c `1) is V28() real ext-real Element of REAL

- (1 * (c `1)) is V28() real ext-real Element of REAL

(- (1 * (c `1))) / (c `1) is V28() real ext-real Element of REAL

(- (1 * (c `1))) * ((c `1) ") is V28() real ext-real set

O is Relation-like Function-like V45(2) FinSequence-like V119() V120() V121() Element of the carrier of (TOP-REAL 2)

O `2 is V28() real ext-real Element of REAL

K526(O,2) is V28() real ext-real Element of REAL

O `1 is V28() real ext-real Element of REAL

K526(O,1) is V28() real ext-real Element of REAL

- (O `1) is V28() real ext-real Element of REAL

- 1 is V28() real ext-real non positive Element of REAL

(- 1) * (c `1) is V28() real ext-real Element of REAL

((- 1) * (c `1)) / (c `1) is V28() real ext-real Element of REAL

((- 1) * (c `1)) * ((c `1) ") is V28() real ext-real set

(- 1) / (c `1) is V28() real ext-real Element of REAL

(- 1) * ((c `1) ") is V28() real ext-real set

- (1 / (c `1)) is V28() real ext-real Element of REAL

|[(1 / (c `1)),(((c `2) / (c `1)) / (c `1))]| `2 is V28() real ext-real Element of REAL

K526(|[(1 / (c `1)),(((c `2) / (c `1)) / (c `1))]|,2) is V28() real ext-real Element of REAL

- 1 is V28() real ext-real non positive Element of REAL

1 * (c `1) is V28() real ext-real Element of REAL

- (1 * (c `1)) is V28() real ext-real Element of REAL

(c `1) / (c `1) is V28() real ext-real Element of REAL

(c `1) * ((c `1) ") is V28() real ext-real set

(- (1 * (c `1))) / (c `1) is V28() real ext-real Element of REAL

(- (1 * (c `1))) * ((c `1) ") is V28() real ext-real set

O is Relation-like Function-like V45(2) FinSequence-like V119() V120() V121() Element of the carrier of (TOP-REAL 2)

O `2 is V28() real ext-real Element of REAL

K526(O,2) is V28() real ext-real Element of REAL

O `1 is V28() real ext-real Element of REAL

K526(O,1) is V28() real ext-real Element of REAL

- (O `1) is V28() real ext-real Element of REAL

(- 1) * (c `1) is V28() real ext-real Element of REAL

((- 1) * (c `1)) / (c `1) is V28() real ext-real Element of REAL

((- 1) * (c `1)) * ((c `1) ") is V28() real ext-real set

(- 1) / (c `1) is V28() real ext-real Element of REAL

(- 1) * ((c `1) ") is V28() real ext-real set

- (1 / (c `1)) is V28() real ext-real Element of REAL

|[(1 / (c `1)),(((c `2) / (c `1)) / (c `1))]| `2 is V28() real ext-real Element of REAL

K526(|[(1 / (c `1)),(((c `2) / (c `1)) / (c `1))]|,2) is V28() real ext-real Element of REAL

[#] (((TOP-REAL 2) | K0) | f) is non proper open closed Element of K19( the carrier of (((TOP-REAL 2) | K0) | f))

K19( the carrier of (((TOP-REAL 2) | K0) | f)) is set

{ b

K0 is Element of K19( the carrier of (TOP-REAL 2))

(TOP-REAL 2) | K0 is strict TopSpace-like SubSpace of TOP-REAL 2

the carrier of ((TOP-REAL 2) | K0) is set

K19( the carrier of ((TOP-REAL 2) | K0)) is set

f is Element of K19( the carrier of ((TOP-REAL 2) | K0))

() | f is Relation-like NonZero (TOP-REAL 2) -defined NonZero (TOP-REAL 2) -valued Function-like Element of K19(K20((NonZero (TOP-REAL 2)),(NonZero (TOP-REAL 2))))

rng (() | f) is Element of K19((NonZero (TOP-REAL 2)))

K19((NonZero (TOP-REAL 2))) is set

((TOP-REAL 2) | K0) | f is strict TopSpace-like SubSpace of (TOP-REAL 2) | K0

the carrier of (((TOP-REAL 2) | K0) | f) is set

[#] ((TOP-REAL 2) | K0) is non proper open closed Element of K19( the carrier of ((TOP-REAL 2) | K0))

g is Element of K19( the carrier of (TOP-REAL 2))

(TOP-REAL 2) | g is strict TopSpace-like SubSpace of TOP-REAL 2

the carrier of ((TOP-REAL 2) | g) is set

a is Relation-like Function-like V45(2) FinSequence-like V119() V120() V121() Element of the carrier of (TOP-REAL 2)

a `2 is V28() real ext-real Element of REAL

K526(a,2) is V28() real ext-real Element of REAL

[#] ((TOP-REAL 2) | g) is non proper open closed Element of K19( the carrier of ((TOP-REAL 2) | g))

K19( the carrier of ((TOP-REAL 2) | g)) is set

a `1 is V28() real ext-real Element of REAL

K526(a,1) is V28() real ext-real Element of REAL

b is Relation-like Function-like V45(2) FinSequence-like V119() V120() V121() Element of the carrier of (TOP-REAL 2)

b `1 is V28() real ext-real Element of REAL

K526(b,1) is V28() real ext-real Element of REAL

b `2 is V28() real ext-real Element of REAL

K526(b,2) is V28() real ext-real Element of REAL

- (b `2) is V28() real ext-real Element of REAL

b is Relation-like Function-like V45(2) FinSequence-like V119() V120() V121() Element of the carrier of (TOP-REAL 2)

b `1 is V28() real ext-real Element of REAL

K526(b,1) is V28() real ext-real Element of REAL

b `2 is V28() real ext-real Element of REAL

K526(b,2) is V28() real ext-real Element of REAL

- (b `2) is V28() real ext-real Element of REAL

a is set

dom (() | f) is Element of K19((NonZero (TOP-REAL 2)))

b is set

(() | f) . b is set

dom () is Element of K19((NonZero (TOP-REAL 2)))

(dom ()) /\ f is Element of K19( the carrier of ((TOP-REAL 2) | K0))

c is Relation-like Function-like V45(2) FinSequence-like V119() V120() V121() Element of the carrier of (TOP-REAL 2)

() . c is set

c `1 is V28() real ext-real Element of REAL

K526(c,1) is V28() real ext-real Element of REAL

c `2 is V28() real ext-real Element of REAL

K526(c,2) is V28() real ext-real Element of REAL

(c `1) / (c `2) is V28() real ext-real Element of REAL

(c `2) " is V28() real ext-real set

(c `1) * ((c `2) ") is V28() real ext-real set

((c `1) / (c `2)) / (c `2) is V28() real ext-real Element of REAL

((c `1) / (c `2)) * ((c `2) ") is V28() real ext-real set

1 / (c `2) is V28() real ext-real Element of REAL

1 * ((c `2) ") is V28() real ext-real set

|[(((c `1) / (c `2)) / (c `2)),(1 / (c `2))]| is Relation-like Function-like V45(2) FinSequence-like V119() V120() V121() Element of the carrier of (TOP-REAL 2)

d is Relation-like Function-like V45(2) FinSequence-like V119() V120() V121() Element of the carrier of (TOP-REAL 2)

d `1 is V28() real ext-real Element of REAL

K526(d,1) is V28() real ext-real Element of REAL

d `2 is V28() real ext-real Element of REAL

K526(d,2) is V28() real ext-real Element of REAL

- (d `2) is V28() real ext-real Element of REAL

[#] ((TOP-REAL 2) | g) is non proper open closed Element of K19( the carrier of ((TOP-REAL 2) | g))

K19( the carrier of ((TOP-REAL 2) | g)) is set

|[(((c `1) / (c `2)) / (c `2)),(1 / (c `2))]| `2 is V28() real ext-real Element of REAL

K526(|[(((c `1) / (c `2)) / (c `2)),(1 / (c `2))]|,2) is V28() real ext-real Element of REAL

0 * (c `2) is V28() real ext-real Element of REAL

(1 / (c `2)) * (c `2) is V28() real ext-real Element of REAL

(c `2) / (c `2) is V28() real ext-real Element of REAL

(c `2) * ((c `2) ") is V28() real ext-real set

1 * (c `2) is V28() real ext-real Element of REAL

- (1 * (c `2)) is V28() real ext-real Element of REAL

(- (1 * (c `2))) / (c `2) is V28() real ext-real Element of REAL

(- (1 * (c `2))) * ((c `2) ") is V28() real ext-real set

O is Relation-like Function-like V45(2) FinSequence-like V119() V120() V121() Element of the carrier of (TOP-REAL 2)

O `1 is V28() real ext-real Element of REAL

K526(O,1) is V28() real ext-real Element of REAL

O `2 is V28() real ext-real Element of REAL

K526(O,2) is V28() real ext-real Element of REAL

- (O `2) is V28() real ext-real Element of REAL

- 1 is V28() real ext-real non positive Element of REAL

(- 1) * (c `2) is V28() real ext-real Element of REAL

((- 1) * (c `2)) / (c `2) is V28() real ext-real Element of REAL

((- 1) * (c `2)) * ((c `2) ") is V28() real ext-real set

(- 1) / (c `2) is V28() real ext-real Element of REAL

(- 1) * ((c `2) ") is V28() real ext-real set

- (1 / (c `2)) is V28() real ext-real Element of REAL

|[(((c `1) / (c `2)) / (c `2)),(1 / (c `2))]| `1 is V28() real ext-real Element of REAL

K526(|[(((c `1) / (c `2)) / (c `2)),(1 / (c `2))]|,1) is V28() real ext-real Element of REAL

1 * (c `2) is V28() real ext-real Element of REAL

- (1 * (c `2)) is V28() real ext-real Element of REAL

(c `2) / (c `2) is V28() real ext-real Element of REAL

(c `2) * ((c `2) ") is V28() real ext-real set

(- (1 * (c `2))) / (c `2) is V28() real ext-real Element of REAL

(- (1 * (c `2))) * ((c `2) ") is V28() real ext-real set

O is Relation-like Function-like V45(2) FinSequence-like V119() V120() V121() Element of the carrier of (TOP-REAL 2)

O `1 is V28() real ext-real Element of REAL

K526(O,1) is V28() real ext-real Element of REAL

O `2 is V28() real ext-real Element of REAL

K526(O,2) is V28() real ext-real Element of REAL

- (O `2) is V28() real ext-real Element of REAL

- 1 is V28() real ext-real non positive Element of REAL

(- 1) * (c `2) is V28() real ext-real Element of REAL

((- 1) * (c `2)) / (c `2) is V28() real ext-real Element of REAL

((- 1) * (c `2)) * ((c `2) ") is V28() real ext-real set

(- 1) / (c `2) is V28() real ext-real Element of REAL

(- 1) * ((c `2) ") is V28() real ext-real set

- (1 / (c `2)) is V28() real ext-real Element of REAL

|[(((c `1) / (c `2)) / (c `2)),(1 / (c `2))]| `1 is V28() real ext-real Element of REAL

K526(|[(((c `1) / (c `2)) / (c `2)),(1 / (c `2))]|,1) is V28() real ext-real Element of REAL

[#] (((TOP-REAL 2) | K0) | f) is non proper open closed Element of K19( the carrier of (((TOP-REAL 2) | K0) | f))

K19( the carrier of (((TOP-REAL 2) | K0) | f)) is set

0.REAL 2 is Relation-like Function-like V45(2) FinSequence-like V119() V120() V121() Element of the carrier of (TOP-REAL 2)

2 |-> 0 is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V119() V120() V121() Element of 2 -tuples_on REAL

K0 is set

f is non empty Element of K19( the carrier of (TOP-REAL 2))

f ` is Element of K19( the carrier of (TOP-REAL 2))

(TOP-REAL 2) | f is non empty strict TopSpace-like SubSpace of TOP-REAL 2

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

K19( the carrier of ((TOP-REAL 2) | f)) is set

- ((1.REAL 2) `1) is V28() real ext-real Element of REAL

g is set

(f `) ` is Element of K19( the carrier of (TOP-REAL 2))

a is Relation-like Function-like V45(2) FinSequence-like V119() V120() V121() Element of the carrier of (TOP-REAL 2)

a `2 is V28() real ext-real Element of REAL

K526(a,2) is V28() real ext-real Element of REAL

a `1 is V28() real ext-real Element of REAL

K526(a,1) is V28() real ext-real Element of REAL

- (a `1) is V28() real ext-real Element of REAL

a is Relation-like Function-like V45(2) FinSequence-like V119() V120() V121() Element of the carrier of (TOP-REAL 2)

a `2 is V28() real ext-real Element of REAL

K526(a,2) is V28() real ext-real Element of REAL

a `1 is V28() real ext-real Element of REAL

K526(a,1) is V28() real ext-real Element of REAL

- (a `1) is V28() real ext-real Element of REAL

[#] ((TOP-REAL 2) | f) is non empty non proper open closed Element of K19( the carrier of ((TOP-REAL 2) | f))

K0 is set

f is non empty Element of K19( the carrier of (TOP-REAL 2))

f ` is Element of K19( the carrier of (TOP-REAL 2))

(TOP-REAL 2) | f is non empty strict TopSpace-like SubSpace of TOP-REAL 2

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

K19( the carrier of ((TOP-REAL 2) | f)) is set

- ((1.REAL 2) `2) is V28() real ext-real Element of REAL

g is set

(f `) ` is Element of K19( the carrier of (TOP-REAL 2))

a is Relation-like Function-like V45(2) FinSequence-like V119() V120() V121() Element of the carrier of (TOP-REAL 2)

a `1 is V28() real ext-real Element of REAL

K526(a,1) is V28() real ext-real Element of REAL

a `2 is V28() real ext-real Element of REAL

K526(a,2) is V28() real ext-real Element of REAL

- (a `2) is V28() real ext-real Element of REAL

a is Relation-like Function-like V45(2) FinSequence-like V119() V120() V121() Element of the carrier of (TOP-REAL 2)

a `1 is V28() real ext-real Element of REAL

K526(a,1) is V28() real ext-real Element of REAL

a `2 is V28() real ext-real Element of REAL

K526(a,2) is V28() real ext-real Element of REAL

- (a `2) is V28() real ext-real Element of REAL

[#] ((TOP-REAL 2) | f) is non empty non proper open closed Element of K19( the carrier of ((TOP-REAL 2) | f))

K0 is non empty TopSpace-like TopStruct

the carrier of K0 is non empty set

K20( the carrier of K0, the carrier of R^1) is V121() set

K19(K20( the carrier of K0, the carrier of R^1)) is set

f is Relation-like the carrier of K0 -defined the carrier of R^1 -valued Function-like non empty total V18( the carrier of K0, the carrier of R^1) V119() V120() V121() Element of K19(K20( the carrier of K0, the carrier of R^1))

g is Relation-like the carrier of K0 -defined the carrier of R^1 -valued Function-like non empty total V18( the carrier of K0, the carrier of R^1) V119() V120() V121() Element of K19(K20( the carrier of K0, the carrier of R^1))

a is Element of the carrier of K0

f . a is V28() real ext-real set

g . a is V28() real ext-real set

f . a is V28() real ext-real Element of the carrier of R^1

g . a is V28() real ext-real Element of the carrier of R^1

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

c is V28() real ext-real Element of REAL

b + c is V28() real ext-real Element of REAL

O is V28() real ext-real set

I is V28() real ext-real set

O + I is V28() real ext-real set

K20( the carrier of K0,REAL) is set

K19(K20( the carrier of K0,REAL)) is set

a is Relation-like the carrier of K0 -defined REAL -valued Function-like non empty total V18( the carrier of K0, REAL ) V119() V120() V121() Element of K19(K20( the carrier of K0,REAL))

a is Relation-like the carrier of K0 -defined REAL -valued Function-like non empty total V18( the carrier of K0, REAL ) V119() V120() V121() Element of K19(K20( the carrier of K0,REAL))

b is Relation-like the carrier of K0 -defined the carrier of R^1 -valued Function-like non empty total V18( the carrier of K0, the carrier of R^1) V119() V120() V121() Element of K19(K20( the carrier of K0, the carrier of R^1))

K19( the carrier of K0) is set

c is Element of the carrier of K0

b . c is V28() real ext-real Element of the carrier of R^1

d is Element of K19( the carrier of R^1)

f . c is V28() real ext-real Element of the carrier of R^1

g . c is V28() real ext-real Element of the carrier of R^1

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

B is V28() real ext-real Element of REAL

O - B is V28() real ext-real Element of REAL

- B is V28() real ext-real set

O + (- B) is V28() real ext-real set

O + B is V28() real ext-real Element of REAL

].(O - B),(O + B).[ is Element of K19(REAL)

I is V28() real ext-real Element of REAL

B / 2 is V28() real ext-real Element of REAL

2 " is non empty V28() real ext-real positive non negative set

B * (2 ") is V28() real ext-real set

I - (B / 2) is V28() real ext-real Element of REAL

- (B / 2) is V28() real ext-real set

I + (- (B / 2)) is V28() real ext-real set

I + (B / 2) is V28() real ext-real Element of REAL

].(I - (B / 2)),(I + (B / 2)).[ is Element of K19(REAL)

C is Element of K19( the carrier of R^1)

A is V28() real ext-real Element of REAL

A - (B / 2) is V28() real ext-real Element of REAL

A + (- (B / 2)) is V28() real ext-real set

A + (B / 2) is V28() real ext-real Element of REAL

].(A - (B / 2)),(A + (B / 2)).[ is Element of K19(REAL)

D is Element of K19( the carrier of R^1)

ff is Element of K19( the carrier of K0)

g .: ff is V129() V130() V131() Element of K19( the carrier of R^1)

f2 is Element of K19( the carrier of K0)

f .: f2 is V129() V130() V131() Element of K19( the carrier of R^1)

f2 /\ ff is Element of K19( the carrier of K0)

b .: (f2 /\ ff) is V129() V130() V131() Element of K19( the carrier of R^1)

y is set

dom b is Element of K19( the carrier of K0)

x is set

b . x is V28() real ext-real set

x2 is Element of the carrier of K0

g . x2 is V28() real ext-real Element of the carrier of R^1

f . x2 is V28() real ext-real Element of the carrier of R^1

dom g is Element of K19( the carrier of K0)

z is V28() real ext-real Element of REAL

dom f is Element of K19( the carrier of K0)

u is V28() real ext-real Element of REAL

u + z is V28() real ext-real Element of REAL

(I - (B / 2)) + (A - (B / 2)) is V28() real ext-real Element of REAL

I + A is V28() real ext-real Element of REAL

(B