:: TOPMETR2 semantic presentation

REAL is non empty V30() V31() V32() V36() V43() V120() V121() V123() set

NAT is V30() V31() V32() V33() V34() V35() V36() V120() Element of K19(REAL)

K19(REAL) is set

NAT is V30() V31() V32() V33() V34() V35() V36() V120() set

K19(NAT) is set

K225() is non empty strict TopSpace-like V117() TopStruct

the carrier of K225() is non empty V30() V31() V32() set

1 is non empty V27() V28() V29() V30() V31() V32() V33() V34() V35() ext-real positive V118() V120() 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(REAL,REAL) is set

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

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

2 is non empty V27() V28() V29() V30() V31() V32() V33() V34() V35() ext-real positive V118() V120() 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 non empty strict Reflexive discerning V110() triangle Discerning V117() MetrStruct

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

{} is empty V30() V31() V32() V33() V34() V35() V36() V120() V123() set

0 is empty V27() V28() V29() V30() V31() V32() V33() V34() V35() V36() ext-real V120() V123() Element of NAT

[.0,1.] is V30() V31() V32() V123() Element of K19(REAL)

TopSpaceMetr RealSpace is non empty strict TopSpace-like TopStruct

the carrier of R^1 is non empty V30() V31() V32() set

K19( the carrier of R^1) is set

Closed-Interval-TSpace (0,1) is non empty strict TopSpace-like V117() SubSpace of R^1

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

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

T is Relation-like Function-like set

dom T is set

pp is Relation-like Function-like set

dom pp is set

(dom T) \ (dom pp) is Element of K19((dom T))

K19((dom T)) is set

T +* pp is Relation-like Function-like set

PP is set

dom (T +* pp) is set

T1 is set

(T +* pp) . PP is set

(T +* pp) . T1 is set

(dom T) \/ (dom pp) is set

((dom T) \ (dom pp)) \/ (dom pp) is set

T . PP is set

T . T1 is set

pp . T1 is set

T . T1 is set

pp . PP is set

pp . T1 is set

pp . PP is set

T is Relation-like Function-like set

dom T is set

rng T is set

pp is Relation-like Function-like set

dom pp is set

(dom T) /\ (dom pp) is set

T .: ((dom T) /\ (dom pp)) is set

rng pp is set

(rng T) \ (rng pp) is Element of K19((rng T))

K19((rng T)) is set

T +* pp is Relation-like Function-like set

rng (T +* pp) is set

PP is set

T1 is set

T . T1 is set

(dom T) \/ (dom pp) is set

dom (T +* pp) is set

(T +* pp) . T1 is set

T is Relation-like Function-like set

dom T is set

rng T is set

pp is Relation-like Function-like set

dom pp is set

(dom T) /\ (dom pp) is set

T .: ((dom T) /\ (dom pp)) is set

rng pp is set

(rng T) \/ (rng pp) is set

T +* pp is Relation-like Function-like set

rng (T +* pp) is set

(rng T) \ (rng pp) is Element of K19((rng T))

K19((rng T)) is set

((rng T) \ (rng pp)) \/ (rng pp) is set

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

the carrier of I[01] is non empty V30() V31() V32() set

T is TopSpace-like T_0 T_1 T_2 TopStruct

the carrier of T is set

K19( the carrier of T) is set

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

{ b

[.0,(1 / 2).] is V30() V31() V32() V123() Element of K19(REAL)

[.(1 / 2),1.] is V30() V31() V32() V123() Element of K19(REAL)

Closed-Interval-TSpace ((1 / 2),1) is non empty strict TopSpace-like V117() SubSpace of R^1

the carrier of (Closed-Interval-TSpace ((1 / 2),1)) is non empty V30() V31() V32() set

Closed-Interval-TSpace (0,(1 / 2)) is non empty strict TopSpace-like V117() SubSpace of R^1

the carrier of (Closed-Interval-TSpace (0,(1 / 2))) is non empty V30() V31() V32() set

P is Element of K19( the carrier of T)

T | P is strict TopSpace-like SubSpace of T

the carrier of (T | P) is set

K20( the carrier of I[01], the carrier of (T | P)) is set

K19(K20( the carrier of I[01], the carrier of (T | P))) is set

Q is Element of K19( the carrier of T)

T | Q is strict TopSpace-like SubSpace of T

the carrier of (T | Q) is set

K20( the carrier of I[01], the carrier of (T | Q)) is set

K19(K20( the carrier of I[01], the carrier of (T | Q))) is set

P /\ Q is Element of K19( the carrier of T)

P \/ Q is Element of K19( the carrier of T)

T | (P \/ Q) is strict TopSpace-like SubSpace of T

the carrier of (T | (P \/ Q)) is set

K20( the carrier of I[01], the carrier of (T | (P \/ Q))) is set

K19(K20( the carrier of I[01], the carrier of (T | (P \/ Q)))) is set

p is Element of the carrier of T

{p} is non empty set

f is Relation-like the carrier of I[01] -defined the carrier of (T | P) -valued Function-like V18( the carrier of I[01], the carrier of (T | P)) Element of K19(K20( the carrier of I[01], the carrier of (T | P)))

f . 1 is set

f . 0 is set

g is Relation-like the carrier of I[01] -defined the carrier of (T | Q) -valued Function-like V18( the carrier of I[01], the carrier of (T | Q)) Element of K19(K20( the carrier of I[01], the carrier of (T | Q)))

g . 0 is set

g . 1 is set

[#] (T | Q) is non proper closed Element of K19( the carrier of (T | Q))

K19( the carrier of (T | Q)) is set

rng g is Element of K19( the carrier of (T | Q))

M is non empty TopSpace-like TopStruct

the carrier of M is non empty set

K19( the carrier of M) is set

P9 is non empty Element of K19( the carrier of M)

Q9 is non empty Element of K19( the carrier of M)

P9 \/ Q9 is non empty Element of K19( the carrier of M)

M | P9 is non empty strict TopSpace-like SubSpace of M

R is non empty Element of K19( the carrier of M)

M | R is non empty strict TopSpace-like SubSpace of M

K19(K20(REAL,REAL)) is set

f3 is Relation-like REAL -defined REAL -valued Function-like non empty V14( REAL ) V18( REAL , REAL ) Element of K19(K20(REAL,REAL))

[#] (M | R) is non empty non proper closed Element of K19( the carrier of (M | R))

the carrier of (M | R) is non empty set

K19( the carrier of (M | R)) is set

dom g is V30() V31() V32() Element of K19( the carrier of I[01])

K19( the carrier of I[01]) is set

K20( the carrier of I[01], the carrier of (M | R)) is set

K19(K20( the carrier of I[01], the carrier of (M | R))) is set

M | Q9 is non empty strict TopSpace-like SubSpace of M

g9 is Relation-like the carrier of I[01] -defined the carrier of (M | R) -valued Function-like non empty V14( the carrier of I[01]) V18( the carrier of I[01], the carrier of (M | R)) Element of K19(K20( the carrier of I[01], the carrier of (M | R)))

PP is V30() V31() V32() Element of K19( the carrier of R^1)

T1 is TopSpace-like V117() SubSpace of I[01]

T2 is TopSpace-like V117() SubSpace of I[01]

[#] (T | P) is non proper closed Element of K19( the carrier of (T | P))

K19( the carrier of (T | P)) is set

rng f is Element of K19( the carrier of (T | P))

dom f is V30() V31() V32() Element of K19( the carrier of I[01])

ff is Relation-like the carrier of I[01] -defined the carrier of (M | R) -valued Function-like non empty V14( the carrier of I[01]) V18( the carrier of I[01], the carrier of (M | R)) Element of K19(K20( the carrier of I[01], the carrier of (M | R)))

f3 is Relation-like the carrier of R^1 -defined the carrier of R^1 -valued Function-like non empty V14( the carrier of R^1) V18( the carrier of R^1, the carrier of R^1) Element of K19(K20( the carrier of R^1, the carrier of R^1))

f3 | [.0,(1 / 2).] is Relation-like the carrier of R^1 -defined the carrier of R^1 -valued Function-like Element of K19(K20( the carrier of R^1, the carrier of R^1))

dom (f3 | [.0,(1 / 2).]) is V30() V31() V32() Element of K19( the carrier of R^1)

dom f3 is V30() V31() V32() Element of K19( the carrier of R^1)

(dom f3) /\ [.0,(1 / 2).] is V30() V31() V32() Element of K19(REAL)

REAL /\ [.0,(1 / 2).] is V30() V31() V32() V123() Element of K19(REAL)

the carrier of T1 is V30() V31() V32() set

rng (f3 | [.0,(1 / 2).]) is V30() V31() V32() Element of K19( the carrier of R^1)

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

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

PP is non empty V30() V31() V32() Element of K19( the carrier of R^1)

f3 | PP is Relation-like the carrier of R^1 -defined the carrier of R^1 -valued Function-like Element of K19(K20( the carrier of R^1, the carrier of R^1))

f39 is Relation-like the carrier of T1 -defined the carrier of R^1 -valued Function-like V14( the carrier of T1) V18( the carrier of T1, the carrier of R^1) Element of K19(K20( the carrier of T1, the carrier of R^1))

dom f39 is V30() V31() V32() Element of K19( the carrier of T1)

K19( the carrier of T1) is set

rng f39 is V30() V31() V32() Element of K19( the carrier of R^1)

f4 is set

PP is set

f39 . PP is set

{ b

PP is V28() V29() ext-real Element of REAL

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

2 * PP is V28() V29() ext-real Element of REAL

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

f3 . PP is set

K20( the carrier of T1, the carrier of I[01]) is set

K19(K20( the carrier of T1, the carrier of I[01])) is set

R^1 | PP is non empty strict TopSpace-like V117() SubSpace of R^1

PP is V28() V29() ext-real Element of REAL

f3 . PP is set

2 * PP is V28() V29() ext-real Element of REAL

(2 * PP) + 0 is V28() V29() ext-real Element of REAL

f4 is Relation-like the carrier of T1 -defined the carrier of I[01] -valued Function-like V14( the carrier of T1) V18( the carrier of T1, the carrier of I[01]) Element of K19(K20( the carrier of T1, the carrier of I[01]))

PP is V30() V31() V32() Element of K19( the carrier of R^1)

g3 is Relation-like REAL -defined REAL -valued Function-like non empty V14( REAL ) V18( REAL , REAL ) Element of K19(K20(REAL,REAL))

g3 is Relation-like the carrier of R^1 -defined the carrier of R^1 -valued Function-like non empty V14( the carrier of R^1) V18( the carrier of R^1, the carrier of R^1) Element of K19(K20( the carrier of R^1, the carrier of R^1))

g3 | [.(1 / 2),1.] is Relation-like the carrier of R^1 -defined the carrier of R^1 -valued Function-like Element of K19(K20( the carrier of R^1, the carrier of R^1))

dom (g3 | [.(1 / 2),1.]) is V30() V31() V32() Element of K19( the carrier of R^1)

dom g3 is V30() V31() V32() Element of K19( the carrier of R^1)

(dom g3) /\ [.(1 / 2),1.] is V30() V31() V32() Element of K19(REAL)

REAL /\ [.(1 / 2),1.] is V30() V31() V32() V123() Element of K19(REAL)

the carrier of T2 is V30() V31() V32() set

rng (g3 | [.(1 / 2),1.]) is V30() V31() V32() Element of K19( the carrier of R^1)

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

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

PP is non empty V30() V31() V32() Element of K19( the carrier of R^1)

g3 | PP is Relation-like the carrier of R^1 -defined the carrier of R^1 -valued Function-like Element of K19(K20( the carrier of R^1, the carrier of R^1))

g39 is Relation-like the carrier of T2 -defined the carrier of R^1 -valued Function-like V14( the carrier of T2) V18( the carrier of T2, the carrier of R^1) Element of K19(K20( the carrier of T2, the carrier of R^1))

dom g39 is V30() V31() V32() Element of K19( the carrier of T2)

K19( the carrier of T2) is set

rng g39 is V30() V31() V32() Element of K19( the carrier of R^1)

g4 is set

f2 is set

g39 . f2 is set

{ b

f1 is V28() V29() ext-real Element of REAL

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

2 * f1 is V28() V29() ext-real Element of REAL

1 - 1 is V28() V29() ext-real Element of REAL

(2 * f1) - 1 is V28() V29() ext-real Element of REAL

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

1 + 1 is V28() V29() ext-real Element of REAL

(1 + 1) - 1 is V28() V29() ext-real Element of REAL

g3 . f2 is set

K20( the carrier of T2, the carrier of I[01]) is set

K19(K20( the carrier of T2, the carrier of I[01])) is set

[#] T1 is non proper V30() V31() V32() closed Element of K19( the carrier of T1)

[#] T2 is non proper V30() V31() V32() closed Element of K19( the carrier of T2)

([#] T1) \/ ([#] T2) is V30() V31() V32() set

[#] I[01] is non empty non proper V30() V31() V32() closed Element of K19( the carrier of I[01])

([#] T1) /\ ([#] T2) is V30() V31() V32() Element of K19( the carrier of T2)

pp is V28() V29() ext-real Element of the carrier of I[01]

{pp} is non empty V30() V31() V32() set

- 1 is V28() V29() ext-real Element of REAL

f2 is V28() V29() ext-real Element of REAL

g3 . f2 is set

2 * f2 is V28() V29() ext-real Element of REAL

(2 * f2) + (- 1) is V28() V29() ext-real Element of REAL

(2 * f2) - 1 is V28() V29() ext-real Element of REAL

R^1 | PP is non empty strict TopSpace-like V117() SubSpace of R^1

g4 is Relation-like the carrier of T2 -defined the carrier of I[01] -valued Function-like V14( the carrier of T2) V18( the carrier of T2, the carrier of I[01]) Element of K19(K20( the carrier of T2, the carrier of I[01]))

f2 is set

{ b

f1 is V28() V29() ext-real Element of REAL

2 * f1 is V28() V29() ext-real Element of REAL

f . (2 * f1) is set

g2 is V28() V29() ext-real Element of REAL

2 * g2 is V28() V29() ext-real Element of REAL

f . (2 * g2) is set

f2 is Relation-like Function-like set

dom f2 is set

the carrier of (M | P9) is non empty set

K20( the carrier of I[01], the carrier of (M | P9)) is set

K19(K20( the carrier of I[01], the carrier of (M | P9))) is set

f1 is set

rng f2 is set

g2 is set

f2 . g2 is set

{ b

g1 is V28() V29() ext-real Element of REAL

2 * g1 is V28() V29() ext-real Element of REAL

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

f . (2 * g1) is set

K20( the carrier of T1, the carrier of (M | R)) is set

K19(K20( the carrier of T1, the carrier of (M | R))) is set

f1 is Relation-like the carrier of T1 -defined the carrier of (M | R) -valued Function-like V14( the carrier of T1) V18( the carrier of T1, the carrier of (M | R)) Element of K19(K20( the carrier of T1, the carrier of (M | R)))

ff * f4 is Relation-like the carrier of T1 -defined the carrier of (M | R) -valued Function-like V14( the carrier of T1) V18( the carrier of T1, the carrier of (M | R)) Element of K19(K20( the carrier of T1, the carrier of (M | R)))

g2 is set

f1 . g2 is set

(ff * f4) . g2 is set

g1 is V28() V29() ext-real Element of REAL

2 * g1 is V28() V29() ext-real Element of REAL

f . (2 * g1) is set

f3 . g1 is set

f . (f3 . g1) is set

f4 . g2 is set

f . (f4 . g2) is set

g2 is V28() V29() ext-real Element of REAL

g1 is V28() V29() ext-real Element of REAL

2 * g1 is V28() V29() ext-real Element of REAL

2 * g2 is V28() V29() ext-real Element of REAL

g2 is set

{ b

g1 is V28() V29() ext-real Element of REAL

2 * g1 is V28() V29() ext-real Element of REAL

(2 * g1) - 1 is V28() V29() ext-real Element of REAL

g . ((2 * g1) - 1) is set

h is V28() V29() ext-real Element of REAL

2 * h is V28() V29() ext-real Element of REAL

(2 * h) - 1 is V28() V29() ext-real Element of REAL

g . ((2 * h) - 1) is set

g2 is Relation-like Function-like set

dom g2 is set

the carrier of (M | Q9) is non empty set

K20( the carrier of I[01], the carrier of (M | Q9)) is set

K19(K20( the carrier of I[01], the carrier of (M | Q9))) is set

g1 is set

rng g2 is set

h is set

g2 . h is set

{ b

h9 is V28() V29() ext-real Element of REAL

2 * h9 is V28() V29() ext-real Element of REAL

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

(2 * h9) - 1 is V28() V29() ext-real Element of REAL

1 + 1 is V28() V29() ext-real Element of REAL

(1 + 1) - 1 is V28() V29() ext-real Element of REAL

1 - 1 is V28() V29() ext-real Element of REAL

g . ((2 * h9) - 1) is set

g1 is set

h is set

g . h is set

h9 is V28() V29() ext-real Element of REAL

h9 + 1 is V28() V29() ext-real Element of REAL

(h9 + 1) / 2 is V28() V29() ext-real Element of REAL

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

0 + 1 is V28() V29() ext-real Element of REAL

2 * ((h9 + 1) / 2) is V28() V29() ext-real Element of REAL

(2 * ((h9 + 1) / 2)) - 1 is V28() V29() ext-real Element of REAL

g . ((2 * ((h9 + 1) / 2)) - 1) is set

g2 . ((h9 + 1) / 2) is set

g1 is V28() V29() ext-real Element of REAL

h is V28() V29() ext-real Element of REAL

2 * h is V28() V29() ext-real Element of REAL

(2 * h) - 1 is V28() V29() ext-real Element of REAL

2 * g1 is V28() V29() ext-real Element of REAL

(2 * g1) - 1 is V28() V29() ext-real Element of REAL

K20( the carrier of T2, the carrier of (M | R)) is set

K19(K20( the carrier of T2, the carrier of (M | R))) is set

g1 is Relation-like the carrier of T2 -defined the carrier of (M | R) -valued Function-like V14( the carrier of T2) V18( the carrier of T2, the carrier of (M | R)) Element of K19(K20( the carrier of T2, the carrier of (M | R)))

g9 * g4 is Relation-like the carrier of T2 -defined the carrier of (M | R) -valued Function-like V14( the carrier of T2) V18( the carrier of T2, the carrier of (M | R)) Element of K19(K20( the carrier of T2, the carrier of (M | R)))

h is set

g1 . h is set

(g9 * g4) . h is set

h9 is V28() V29() ext-real Element of REAL

2 * h9 is V28() V29() ext-real Element of REAL

(2 * h9) - 1 is V28() V29() ext-real Element of REAL

g . ((2 * h9) - 1) is set

g3 . h9 is set

g . (g3 . h9) is set

g4 . h is set

g . (g4 . h) is set

f1 . pp is set

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

g . ((2 * (1 / 2)) - 1) is set

g1 . pp is set

f2 +* g2 is Relation-like Function-like set

h9 is set

h is Relation-like the carrier of I[01] -defined the carrier of (M | R) -valued Function-like non empty V14( the carrier of I[01]) V18( the carrier of I[01], the carrier of (M | R)) continuous Element of K19(K20( the carrier of I[01], the carrier of (M | R)))

dom h is V30() V31() V32() Element of K19( the carrier of I[01])

a is set

h . h9 is set

h . a is set

(dom f2) \/ (dom g2) is set

x is V28() V29() ext-real Element of REAL

2 * x is V28() V29() ext-real Element of REAL

x9 is V28() V29() ext-real Element of REAL

2 * x9 is V28() V29() ext-real Element of REAL

f . (2 * x) is set

f2 . h9 is set

f2 . a is set

f . (2 * x9) is set

(dom f2) \/ (dom g2) is set

x is V28() V29() ext-real Element of REAL

2 * x is V28() V29() ext-real Element of REAL

f . (2 * x) is set

x9 is V28() V29() ext-real Element of REAL

2 * x9 is V28() V29() ext-real Element of REAL

(2 * x9) - 1 is V28() V29() ext-real Element of REAL

g . ((2 * x9) - 1) is set

f2 . h9 is set

g2 . a is set

((2 * x9) - 1) + 1 is V28() V29() ext-real Element of REAL

0 + 1 is V28() V29() ext-real Element of REAL

(1 / 2) * (2 * x) is V28() V29() ext-real Element of REAL

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

(dom f2) \/ (dom g2) is set

x is V28() V29() ext-real Element of REAL

2 * x is V28() V29() ext-real Element of REAL

f . (2 * x) is set

x9 is V28() V29() ext-real Element of REAL

2 * x9 is V28() V29() ext-real Element of REAL

(2 * x9) - 1 is V28() V29() ext-real Element of REAL

g . ((2 * x9) - 1) is set

f2 . a is set

g2 . h9 is set

((2 * x9) - 1) + 1 is V28() V29() ext-real Element of REAL

0 + 1 is V28() V29() ext-real Element of REAL

(1 / 2) * (2 * x) is V28() V29() ext-real Element of REAL

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

x is V28() V29() ext-real Element of REAL

2 * x is V28() V29() ext-real Element of REAL

(2 * x) - 1 is V28() V29() ext-real Element of REAL

x9 is V28() V29() ext-real Element of REAL

2 * x9 is V28() V29() ext-real Element of REAL

(2 * x9) - 1 is V28() V29() ext-real Element of REAL

g . ((2 * x9) - 1) is set

g2 . h9 is set

g2 . a is set

g . ((2 * x) - 1) is set

((2 * x9) - 1) + 1 is V28() V29() ext-real Element of REAL

((2 * x) - 1) + 1 is V28() V29() ext-real Element of REAL

h9 is Relation-like the carrier of I[01] -defined the carrier of (T | (P \/ Q)) -valued Function-like V18( the carrier of I[01], the carrier of (T | (P \/ Q))) Element of K19(K20( the carrier of I[01], the carrier of (T | (P \/ Q))))

h9 . 0 is set

h9 . 1 is set

a is set

x is set

f . x is set

x9 is V28() V29() ext-real Element of REAL

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

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

2 * (x9 / 2) is V28() V29() ext-real Element of REAL

f . (2 * (x9 / 2)) is set

f2 . (x9 / 2) is set

rng h is Element of K19( the carrier of (M | R))

a is set

x is set

f2 . x is set

[.0,(1 / 2).] /\ [.(1 / 2),1.] is V30() V31() V32() V123() Element of K19(REAL)

{(1 / 2)} is non empty V30() V31() V32() set

(dom f2) \/ (dom g2) is set

h . x is set

g2 . x is set

f2 . (1 / 2) is set

(dom f2) \/ (dom g2) is set

h . x is set

(rng f2) \/ (rng g2) is set

f2 . 0 is set

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

f . (2 * 0) is set

g2 . 1 is set

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

g . ((2 * 1) - 1) is set