:: TOPMETR2 semantic presentation

begin

theorem :: TOPMETR2:1
for f, g being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) is one-to-one & g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) is one-to-one & ( for x1, x2 being ( ( ) ( ) set ) st x1 : ( ( ) ( ) set ) in dom g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) & x2 : ( ( ) ( ) set ) in (dom f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( ) ( ) set ) \ (dom g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( ) ( ) set ) : ( ( ) ( ) Element of K19((dom b1 : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) holds
g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . x1 : ( ( ) ( ) set ) : ( ( ) ( ) set ) <> f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . x2 : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) holds
f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) +* g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) is one-to-one ;

theorem :: TOPMETR2:2
for f, g being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) .: ((dom f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( ) ( ) set ) /\ (dom g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) c= rng g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) holds
(rng f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( ) ( ) set ) \/ (rng g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) = rng (f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) +* g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) ;

theorem :: TOPMETR2:3
for T being ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace)
for P, Q being ( ( ) ( ) Subset of )
for p being ( ( ) ( ) Point of ( ( ) ( ) set ) )
for f being ( ( Function-like V18( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V117() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V117() ) TopStruct ) ) : ( ( ) ( non empty V30() V31() V32() ) set ) , the carrier of (b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | b2 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V117() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V117() ) TopStruct ) ) : ( ( ) ( non empty V30() V31() V32() ) set ) -defined the carrier of (b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | b2 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) ) : ( ( ) ( ) set ) -valued Function-like V18( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V117() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V117() ) TopStruct ) ) : ( ( ) ( non empty V30() V31() V32() ) set ) , the carrier of (b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | b2 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) ) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( non empty V30() V31() V32() ) set ) , ( ( ) ( ) set ) )
for g being ( ( Function-like V18( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V117() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V117() ) TopStruct ) ) : ( ( ) ( non empty V30() V31() V32() ) set ) , the carrier of (b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | b3 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V117() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V117() ) TopStruct ) ) : ( ( ) ( non empty V30() V31() V32() ) set ) -defined the carrier of (b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | b3 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) ) : ( ( ) ( ) set ) -valued Function-like V18( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V117() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V117() ) TopStruct ) ) : ( ( ) ( non empty V30() V31() V32() ) set ) , the carrier of (b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | b3 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) ) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( non empty V30() V31() V32() ) set ) , ( ( ) ( ) set ) ) st P : ( ( ) ( ) Subset of ) /\ Q : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K19( the carrier of b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = {p : ( ( ) ( ) Point of ( ( ) ( ) set ) ) } : ( ( ) ( non empty ) set ) & f : ( ( Function-like V18( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V117() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V117() ) TopStruct ) ) : ( ( ) ( non empty V30() V31() V32() ) set ) , the carrier of (b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | b2 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V117() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V117() ) TopStruct ) ) : ( ( ) ( non empty V30() V31() V32() ) set ) -defined the carrier of (b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | b2 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) ) : ( ( ) ( ) set ) -valued Function-like V18( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V117() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V117() ) TopStruct ) ) : ( ( ) ( non empty V30() V31() V32() ) set ) , the carrier of (b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | b2 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) ) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( non empty V30() V31() V32() ) set ) , ( ( ) ( ) set ) ) is being_homeomorphism & f : ( ( Function-like V18( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V117() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V117() ) TopStruct ) ) : ( ( ) ( non empty V30() V31() V32() ) set ) , the carrier of (b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | b2 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V117() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V117() ) TopStruct ) ) : ( ( ) ( non empty V30() V31() V32() ) set ) -defined the carrier of (b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | b2 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) ) : ( ( ) ( ) set ) -valued Function-like V18( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V117() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V117() ) TopStruct ) ) : ( ( ) ( non empty V30() V31() V32() ) set ) , the carrier of (b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | b2 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) ) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( non empty V30() V31() V32() ) set ) , ( ( ) ( ) set ) ) . 1 : ( ( ) ( non empty V27() V28() V29() V30() V31() V32() V33() V34() V35() ext-real positive V118() V120() ) Element of NAT : ( ( ) ( V30() V31() V32() V33() V34() V35() V36() V120() ) Element of K19(REAL : ( ( ) ( non empty V30() V31() V32() V36() V43() V120() V121() V123() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) = p : ( ( ) ( ) Point of ( ( ) ( ) set ) ) & g : ( ( Function-like V18( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V117() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V117() ) TopStruct ) ) : ( ( ) ( non empty V30() V31() V32() ) set ) , the carrier of (b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | b3 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V117() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V117() ) TopStruct ) ) : ( ( ) ( non empty V30() V31() V32() ) set ) -defined the carrier of (b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | b3 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) ) : ( ( ) ( ) set ) -valued Function-like V18( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V117() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V117() ) TopStruct ) ) : ( ( ) ( non empty V30() V31() V32() ) set ) , the carrier of (b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | b3 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) ) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( non empty V30() V31() V32() ) set ) , ( ( ) ( ) set ) ) is being_homeomorphism & g : ( ( Function-like V18( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V117() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V117() ) TopStruct ) ) : ( ( ) ( non empty V30() V31() V32() ) set ) , the carrier of (b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | b3 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V117() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V117() ) TopStruct ) ) : ( ( ) ( non empty V30() V31() V32() ) set ) -defined the carrier of (b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | b3 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) ) : ( ( ) ( ) set ) -valued Function-like V18( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V117() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V117() ) TopStruct ) ) : ( ( ) ( non empty V30() V31() V32() ) set ) , the carrier of (b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | b3 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) ) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( non empty V30() V31() V32() ) set ) , ( ( ) ( ) set ) ) . 0 : ( ( ) ( empty V27() V28() V29() V30() V31() V32() V33() V34() V35() V36() ext-real V120() V123() ) Element of NAT : ( ( ) ( V30() V31() V32() V33() V34() V35() V36() V120() ) Element of K19(REAL : ( ( ) ( non empty V30() V31() V32() V36() V43() V120() V121() V123() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) = p : ( ( ) ( ) Point of ( ( ) ( ) set ) ) holds
ex h being ( ( Function-like V18( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V117() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V117() ) TopStruct ) ) : ( ( ) ( non empty V30() V31() V32() ) set ) , the carrier of (b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | (b2 : ( ( ) ( ) Subset of ) \/ b3 : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of K19( the carrier of b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V117() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V117() ) TopStruct ) ) : ( ( ) ( non empty V30() V31() V32() ) set ) -defined the carrier of (b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | (b2 : ( ( ) ( ) Subset of ) \/ b3 : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of K19( the carrier of b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) ) : ( ( ) ( ) set ) -valued Function-like V18( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V117() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V117() ) TopStruct ) ) : ( ( ) ( non empty V30() V31() V32() ) set ) , the carrier of (b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | (b2 : ( ( ) ( ) Subset of ) \/ b3 : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of K19( the carrier of b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) ) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( non empty V30() V31() V32() ) set ) , ( ( ) ( ) set ) ) st
( h : ( ( Function-like V18( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V117() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V117() ) TopStruct ) ) : ( ( ) ( non empty V30() V31() V32() ) set ) , the carrier of (b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | (b2 : ( ( ) ( ) Subset of ) \/ b3 : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of K19( the carrier of b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V117() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V117() ) TopStruct ) ) : ( ( ) ( non empty V30() V31() V32() ) set ) -defined the carrier of (b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | (b2 : ( ( ) ( ) Subset of ) \/ b3 : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of K19( the carrier of b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) ) : ( ( ) ( ) set ) -valued Function-like V18( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V117() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V117() ) TopStruct ) ) : ( ( ) ( non empty V30() V31() V32() ) set ) , the carrier of (b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | (b2 : ( ( ) ( ) Subset of ) \/ b3 : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of K19( the carrier of b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) ) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( non empty V30() V31() V32() ) set ) , ( ( ) ( ) set ) ) is being_homeomorphism & h : ( ( Function-like V18( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V117() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V117() ) TopStruct ) ) : ( ( ) ( non empty V30() V31() V32() ) set ) , the carrier of (b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | (b2 : ( ( ) ( ) Subset of ) \/ b3 : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of K19( the carrier of b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V117() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V117() ) TopStruct ) ) : ( ( ) ( non empty V30() V31() V32() ) set ) -defined the carrier of (b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | (b2 : ( ( ) ( ) Subset of ) \/ b3 : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of K19( the carrier of b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) ) : ( ( ) ( ) set ) -valued Function-like V18( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V117() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V117() ) TopStruct ) ) : ( ( ) ( non empty V30() V31() V32() ) set ) , the carrier of (b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | (b2 : ( ( ) ( ) Subset of ) \/ b3 : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of K19( the carrier of b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) ) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( non empty V30() V31() V32() ) set ) , ( ( ) ( ) set ) ) . 0 : ( ( ) ( empty V27() V28() V29() V30() V31() V32() V33() V34() V35() V36() ext-real V120() V123() ) Element of NAT : ( ( ) ( V30() V31() V32() V33() V34() V35() V36() V120() ) Element of K19(REAL : ( ( ) ( non empty V30() V31() V32() V36() V43() V120() V121() V123() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) = f : ( ( Function-like V18( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V117() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V117() ) TopStruct ) ) : ( ( ) ( non empty V30() V31() V32() ) set ) , the carrier of (b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | b2 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V117() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V117() ) TopStruct ) ) : ( ( ) ( non empty V30() V31() V32() ) set ) -defined the carrier of (b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | b2 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) ) : ( ( ) ( ) set ) -valued Function-like V18( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V117() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V117() ) TopStruct ) ) : ( ( ) ( non empty V30() V31() V32() ) set ) , the carrier of (b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | b2 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) ) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( non empty V30() V31() V32() ) set ) , ( ( ) ( ) set ) ) . 0 : ( ( ) ( empty V27() V28() V29() V30() V31() V32() V33() V34() V35() V36() ext-real V120() V123() ) Element of NAT : ( ( ) ( V30() V31() V32() V33() V34() V35() V36() V120() ) Element of K19(REAL : ( ( ) ( non empty V30() V31() V32() V36() V43() V120() V121() V123() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) & h : ( ( Function-like V18( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V117() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V117() ) TopStruct ) ) : ( ( ) ( non empty V30() V31() V32() ) set ) , the carrier of (b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | (b2 : ( ( ) ( ) Subset of ) \/ b3 : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of K19( the carrier of b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V117() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V117() ) TopStruct ) ) : ( ( ) ( non empty V30() V31() V32() ) set ) -defined the carrier of (b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | (b2 : ( ( ) ( ) Subset of ) \/ b3 : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of K19( the carrier of b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) ) : ( ( ) ( ) set ) -valued Function-like V18( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V117() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V117() ) TopStruct ) ) : ( ( ) ( non empty V30() V31() V32() ) set ) , the carrier of (b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | (b2 : ( ( ) ( ) Subset of ) \/ b3 : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of K19( the carrier of b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) ) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( non empty V30() V31() V32() ) set ) , ( ( ) ( ) set ) ) . 1 : ( ( ) ( non empty V27() V28() V29() V30() V31() V32() V33() V34() V35() ext-real positive V118() V120() ) Element of NAT : ( ( ) ( V30() V31() V32() V33() V34() V35() V36() V120() ) Element of K19(REAL : ( ( ) ( non empty V30() V31() V32() V36() V43() V120() V121() V123() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) = g : ( ( Function-like V18( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V117() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V117() ) TopStruct ) ) : ( ( ) ( non empty V30() V31() V32() ) set ) , the carrier of (b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | b3 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V117() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V117() ) TopStruct ) ) : ( ( ) ( non empty V30() V31() V32() ) set ) -defined the carrier of (b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | b3 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) ) : ( ( ) ( ) set ) -valued Function-like V18( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V117() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V117() ) TopStruct ) ) : ( ( ) ( non empty V30() V31() V32() ) set ) , the carrier of (b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | b3 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) ) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( non empty V30() V31() V32() ) set ) , ( ( ) ( ) set ) ) . 1 : ( ( ) ( non empty V27() V28() V29() V30() V31() V32() V33() V34() V35() ext-real positive V118() V120() ) Element of NAT : ( ( ) ( V30() V31() V32() V33() V34() V35() V36() V120() ) Element of K19(REAL : ( ( ) ( non empty V30() V31() V32() V36() V43() V120() V121() V123() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) ;