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
{ b1 where b1 is V28() V29() ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
[.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
{ b1 where b1 is V28() V29() ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 / 2 ) } is set
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
{ b1 where b1 is V28() V29() ext-real Element of REAL : ( 1 / 2 <= b1 & b1 <= 1 ) } is set
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
{ b1 where b1 is V28() V29() ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 / 2 ) } is set
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
{ b1 where b1 is V28() V29() ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 / 2 ) } is set
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
{ b1 where b1 is V28() V29() ext-real Element of REAL : ( 1 / 2 <= b1 & b1 <= 1 ) } is set
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
{ b1 where b1 is V28() V29() ext-real Element of REAL : ( 1 / 2 <= b1 & b1 <= 1 ) } is set
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