:: FINTOPO5 semantic presentation

begin

theorem :: FINTOPO5:1
for X being ( ( ) ( ) set )
for Y being ( ( non empty ) ( non empty ) set )
for f being ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like quasi_total ) Function of X : ( ( ) ( ) set ) ,Y : ( ( non empty ) ( non empty ) set ) )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) st f : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like quasi_total ) Function of b1 : ( ( ) ( ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) ) is one-to-one holds
(f : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like quasi_total ) Function of b1 : ( ( ) ( ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) ) ") : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) .: (f : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like quasi_total ) Function of b1 : ( ( ) ( ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) ) .: A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool b2 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) = A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FINTOPO5:2
for n being ( ( ) ( V4() V5() V6() V10() complex V12() ext-real non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) holds
( n : ( ( ) ( V4() V5() V6() V10() complex V12() ext-real non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) > 0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() complex V12() ext-real non positive non negative functional FinSequence-membered integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) iff Seg n : ( ( ) ( V4() V5() V6() V10() complex V12() ext-real non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V47() V54(b1 : ( ( ) ( V4() V5() V6() V10() complex V12() ext-real non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) ) Element of bool NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) <> {} : ( ( ) ( empty V4() V5() V6() V8() V9() V10() complex V12() ext-real non positive non negative functional FinSequence-membered integer ) set ) ) ;

definition
let FT1, FT2 be ( ( ) ( ) RelStr ) ;
let h be ( ( Function-like quasi_total ) ( Relation-like the carrier of FT1 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) -defined the carrier of FT2 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) ;
attr h is being_homeomorphism means :: FINTOPO5:def 1
( h : ( ( ) ( ) Element of FT1 : ( ( ) ( ) RelStr ) ) is one-to-one & h : ( ( ) ( ) Element of FT1 : ( ( ) ( ) RelStr ) ) is onto & ( for x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds h : ( ( ) ( ) Element of FT1 : ( ( ) ( ) RelStr ) ) .: (U_FT x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of bool the carrier of FT1 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of FT2 : ( ( ) ( Relation-like FT1 : ( ( ) ( ) RelStr ) -defined FT1 : ( ( ) ( ) RelStr ) -valued ) Element of bool [:FT1 : ( ( ) ( ) RelStr ) ,FT1 : ( ( ) ( ) RelStr ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = Im ( the InternalRel of FT2 : ( ( ) ( Relation-like FT1 : ( ( ) ( ) RelStr ) -defined FT1 : ( ( ) ( ) RelStr ) -valued ) Element of bool [:FT1 : ( ( ) ( ) RelStr ) ,FT1 : ( ( ) ( ) RelStr ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like the carrier of FT2 : ( ( ) ( Relation-like FT1 : ( ( ) ( ) RelStr ) -defined FT1 : ( ( ) ( ) RelStr ) -valued ) Element of bool [:FT1 : ( ( ) ( ) RelStr ) ,FT1 : ( ( ) ( ) RelStr ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) -defined the carrier of FT2 : ( ( ) ( Relation-like FT1 : ( ( ) ( ) RelStr ) -defined FT1 : ( ( ) ( ) RelStr ) -valued ) Element of bool [:FT1 : ( ( ) ( ) RelStr ) ,FT1 : ( ( ) ( ) RelStr ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) -valued ) Element of bool [: the carrier of FT2 : ( ( ) ( Relation-like FT1 : ( ( ) ( ) RelStr ) -defined FT1 : ( ( ) ( ) RelStr ) -valued ) Element of bool [:FT1 : ( ( ) ( ) RelStr ) ,FT1 : ( ( ) ( ) RelStr ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) , the carrier of FT2 : ( ( ) ( Relation-like FT1 : ( ( ) ( ) RelStr ) -defined FT1 : ( ( ) ( ) RelStr ) -valued ) Element of bool [:FT1 : ( ( ) ( ) RelStr ) ,FT1 : ( ( ) ( ) RelStr ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,(h : ( ( ) ( ) Element of FT1 : ( ( ) ( ) RelStr ) ) . x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) );
end;

theorem :: FINTOPO5:3
for FT1, FT2 being ( ( non empty ) ( non empty ) RelStr )
for h being ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st h : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is being_homeomorphism holds
ex g being ( ( Function-like quasi_total ) ( Relation-like the carrier of b2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st
( g : ( ( Function-like quasi_total ) ( Relation-like the carrier of b2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) = h : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) " : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) & g : ( ( Function-like quasi_total ) ( Relation-like the carrier of b2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is being_homeomorphism ) ;

theorem :: FINTOPO5:4
for FT1, FT2 being ( ( non empty ) ( non empty ) RelStr )
for h being ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) )
for n being ( ( ) ( V4() V5() V6() V10() complex V12() ext-real non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) )
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st h : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is being_homeomorphism & y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = h : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) holds
for z being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in U_FT (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,n : ( ( ) ( V4() V5() V6() V10() complex V12() ext-real non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) iff h : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) in U_FT (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,n : ( ( ) ( V4() V5() V6() V10() complex V12() ext-real non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of bool the carrier of b2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: FINTOPO5:5
for FT1, FT2 being ( ( non empty ) ( non empty ) RelStr )
for h being ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) )
for n being ( ( ) ( V4() V5() V6() V10() complex V12() ext-real non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) )
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st h : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is being_homeomorphism & y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = h : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) holds
for v being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( (h : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ") : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) . v : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) in U_FT (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,n : ( ( ) ( V4() V5() V6() V10() complex V12() ext-real non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) iff v : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in U_FT (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,n : ( ( ) ( V4() V5() V6() V10() complex V12() ext-real non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of bool the carrier of b2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: FINTOPO5:6
for n being ( ( non zero ) ( non zero V4() V5() V6() V10() complex V12() ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) )
for f being ( ( Function-like quasi_total ) ( Relation-like the carrier of (FTSL1 b1 : ( ( non zero ) ( non zero V4() V5() V6() V10() complex V12() ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (FTSL1 b1 : ( ( non zero ) ( non zero V4() V5() V6() V10() complex V12() ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st f : ( ( Function-like quasi_total ) ( Relation-like the carrier of (FTSL1 b1 : ( ( non zero ) ( non zero V4() V5() V6() V10() complex V12() ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (FTSL1 b1 : ( ( non zero ) ( non zero V4() V5() V6() V10() complex V12() ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is_continuous 0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() complex V12() ext-real non positive non negative functional FinSequence-membered integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) holds
ex p being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st f : ( ( Function-like quasi_total ) ( Relation-like the carrier of (FTSL1 b1 : ( ( non zero ) ( non zero V4() V5() V6() V10() complex V12() ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (FTSL1 b1 : ( ( non zero ) ( non zero V4() V5() V6() V10() complex V12() ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (FTSL1 b1 : ( ( non zero ) ( non zero V4() V5() V6() V10() complex V12() ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) in U_FT (p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() complex V12() ext-real non positive non negative functional FinSequence-membered integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of bool the carrier of (FTSL1 b1 : ( ( non zero ) ( non zero V4() V5() V6() V10() complex V12() ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FINTOPO5:7
for T being ( ( non empty ) ( non empty ) RelStr )
for p being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for k being ( ( ) ( V4() V5() V6() V10() complex V12() ext-real non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) st T : ( ( non empty ) ( non empty ) RelStr ) is filled holds
U_FT (p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,k : ( ( ) ( V4() V5() V6() V10() complex V12() ext-real non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) c= U_FT (p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,(k : ( ( ) ( V4() V5() V6() V10() complex V12() ext-real non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FINTOPO5:8
for T being ( ( non empty ) ( non empty ) RelStr )
for p being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for k being ( ( ) ( V4() V5() V6() V10() complex V12() ext-real non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) st T : ( ( non empty ) ( non empty ) RelStr ) is filled holds
U_FT (p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() complex V12() ext-real non positive non negative functional FinSequence-membered integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) c= U_FT (p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,k : ( ( ) ( V4() V5() V6() V10() complex V12() ext-real non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FINTOPO5:9
for n being ( ( non zero V10() ) ( non zero V4() V5() V6() V10() complex V12() ext-real positive non negative integer ) Nat)
for jn, j, k being ( ( V10() ) ( V4() V5() V6() V10() complex V12() ext-real non negative integer ) Nat)
for p being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = jn : ( ( V10() ) ( V4() V5() V6() V10() complex V12() ext-real non negative integer ) Nat) holds
( j : ( ( V10() ) ( V4() V5() V6() V10() complex V12() ext-real non negative integer ) Nat) in U_FT (p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,k : ( ( V10() ) ( V4() V5() V6() V10() complex V12() ext-real non negative integer ) Nat) ) : ( ( ) ( ) Element of bool the carrier of (FTSL1 b1 : ( ( non zero V10() ) ( non zero V4() V5() V6() V10() complex V12() ext-real positive non negative integer ) Nat) ) : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) iff ( j : ( ( V10() ) ( V4() V5() V6() V10() complex V12() ext-real non negative integer ) Nat) in Seg n : ( ( non zero V10() ) ( non zero V4() V5() V6() V10() complex V12() ext-real positive non negative integer ) Nat) : ( ( ) ( non empty V47() V54(b1 : ( ( non zero V10() ) ( non zero V4() V5() V6() V10() complex V12() ext-real positive non negative integer ) Nat) ) ) Element of bool NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) & abs (jn : ( ( V10() ) ( V4() V5() V6() V10() complex V12() ext-real non negative integer ) Nat) - j : ( ( V10() ) ( V4() V5() V6() V10() complex V12() ext-real non negative integer ) Nat) ) : ( ( ) ( complex V12() ext-real integer ) set ) : ( ( ) ( complex V12() ext-real ) Element of REAL : ( ( ) ( ) set ) ) <= k : ( ( V10() ) ( V4() V5() V6() V10() complex V12() ext-real non negative integer ) Nat) + 1 : ( ( ) ( non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) ) ;

theorem :: FINTOPO5:10
for kc, km being ( ( ) ( V4() V5() V6() V10() complex V12() ext-real non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) )
for n being ( ( non zero ) ( non zero V4() V5() V6() V10() complex V12() ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) )
for f being ( ( Function-like quasi_total ) ( Relation-like the carrier of (FTSL1 b3 : ( ( non zero ) ( non zero V4() V5() V6() V10() complex V12() ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (FTSL1 b3 : ( ( non zero ) ( non zero V4() V5() V6() V10() complex V12() ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st f : ( ( Function-like quasi_total ) ( Relation-like the carrier of (FTSL1 b3 : ( ( non zero ) ( non zero V4() V5() V6() V10() complex V12() ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (FTSL1 b3 : ( ( non zero ) ( non zero V4() V5() V6() V10() complex V12() ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is_continuous kc : ( ( ) ( V4() V5() V6() V10() complex V12() ext-real non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) & km : ( ( ) ( V4() V5() V6() V10() complex V12() ext-real non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) = [/(kc : ( ( ) ( V4() V5() V6() V10() complex V12() ext-real non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) / 2 : ( ( ) ( non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( complex V12() ext-real non negative ) Element of COMPLEX : ( ( ) ( ) set ) ) \] : ( ( integer ) ( complex V12() ext-real integer ) set ) holds
ex p being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st f : ( ( Function-like quasi_total ) ( Relation-like the carrier of (FTSL1 b3 : ( ( non zero ) ( non zero V4() V5() V6() V10() complex V12() ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (FTSL1 b3 : ( ( non zero ) ( non zero V4() V5() V6() V10() complex V12() ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (FTSL1 b3 : ( ( non zero ) ( non zero V4() V5() V6() V10() complex V12() ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) in U_FT (p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,km : ( ( ) ( V4() V5() V6() V10() complex V12() ext-real non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of bool the carrier of (FTSL1 b3 : ( ( non zero ) ( non zero V4() V5() V6() V10() complex V12() ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

definition
let A, B be ( ( ) ( ) set ) ;
let R be ( ( ) ( Relation-like A : ( ( ) ( ) set ) -defined B : ( ( ) ( ) set ) -valued ) Relation of ,) ;
let x be ( ( ) ( ) set ) ;
:: original: Im
redefine func Im (R,x) -> ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;
end;

definition
let n, m be ( ( ) ( V4() V5() V6() V10() complex V12() ext-real non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ;
func Nbdl2 (n,m) -> ( ( ) ( Relation-like [:(Seg n : ( ( ) ( ) RelStr ) ) : ( ( ) ( ) Element of bool NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,(Seg m : ( ( ) ( Relation-like n : ( ( ) ( ) RelStr ) -defined n : ( ( ) ( ) RelStr ) -valued ) Element of bool [:n : ( ( ) ( ) RelStr ) ,n : ( ( ) ( ) RelStr ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( ) set ) -defined [:(Seg n : ( ( ) ( ) RelStr ) ) : ( ( ) ( ) Element of bool NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,(Seg m : ( ( ) ( Relation-like n : ( ( ) ( ) RelStr ) -defined n : ( ( ) ( ) RelStr ) -valued ) Element of bool [:n : ( ( ) ( ) RelStr ) ,n : ( ( ) ( ) RelStr ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( ) set ) -valued ) Relation of ) means :: FINTOPO5:def 2
 for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in [:(Seg n : ( ( ) ( ) RelStr ) ) : ( ( ) ( ) Element of bool NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,(Seg m : ( ( ) ( Relation-like n : ( ( ) ( ) RelStr ) -defined n : ( ( ) ( ) RelStr ) -valued ) Element of bool [:n : ( ( ) ( ) RelStr ) ,n : ( ( ) ( ) RelStr ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( ) set ) holds
for i, j being ( ( ) ( V4() V5() V6() V10() complex V12() ext-real non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) st x : ( ( ) ( ) set ) = [i : ( ( ) ( V4() V5() V6() V10() complex V12() ext-real non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,j : ( ( ) ( V4() V5() V6() V10() complex V12() ext-real non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ] : ( ( ) ( ) set ) holds
Im (it : ( ( ) ( ) Element of n : ( ( ) ( ) RelStr ) ) ,x : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like Seg n : ( ( ) ( ) RelStr ) : ( ( ) ( ) Element of bool NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -defined Seg m : ( ( ) ( Relation-like n : ( ( ) ( ) RelStr ) -defined n : ( ( ) ( ) RelStr ) -valued ) Element of bool [:n : ( ( ) ( ) RelStr ) ,n : ( ( ) ( ) RelStr ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -valued ) Subset of ( ( ) ( non empty ) set ) ) = [:(Im ((Nbdl1 n : ( ( ) ( ) RelStr ) ) : ( ( ) ( Relation-like Seg n : ( ( ) ( ) RelStr ) : ( ( ) ( ) Element of bool NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -defined Seg n : ( ( ) ( ) RelStr ) : ( ( ) ( ) Element of bool NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -valued ) Element of bool [:(Seg n : ( ( ) ( ) RelStr ) ) : ( ( ) ( ) Element of bool NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,(Seg n : ( ( ) ( ) RelStr ) ) : ( ( ) ( ) Element of bool NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,i : ( ( ) ( V4() V5() V6() V10() complex V12() ext-real non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ,(Im ((Nbdl1 m : ( ( ) ( Relation-like n : ( ( ) ( ) RelStr ) -defined n : ( ( ) ( ) RelStr ) -valued ) Element of bool [:n : ( ( ) ( ) RelStr ) ,n : ( ( ) ( ) RelStr ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like Seg m : ( ( ) ( Relation-like n : ( ( ) ( ) RelStr ) -defined n : ( ( ) ( ) RelStr ) -valued ) Element of bool [:n : ( ( ) ( ) RelStr ) ,n : ( ( ) ( ) RelStr ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -defined Seg m : ( ( ) ( Relation-like n : ( ( ) ( ) RelStr ) -defined n : ( ( ) ( ) RelStr ) -valued ) Element of bool [:n : ( ( ) ( ) RelStr ) ,n : ( ( ) ( ) RelStr ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -valued ) Element of bool [:(Seg m : ( ( ) ( Relation-like n : ( ( ) ( ) RelStr ) -defined n : ( ( ) ( ) RelStr ) -valued ) Element of bool [:n : ( ( ) ( ) RelStr ) ,n : ( ( ) ( ) RelStr ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,(Seg m : ( ( ) ( Relation-like n : ( ( ) ( ) RelStr ) -defined n : ( ( ) ( ) RelStr ) -valued ) Element of bool [:n : ( ( ) ( ) RelStr ) ,n : ( ( ) ( ) RelStr ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,j : ( ( ) ( V4() V5() V6() V10() complex V12() ext-real non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( ) set ) ;
end;

definition
let n, m be ( ( ) ( V4() V5() V6() V10() complex V12() ext-real non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ;
func FTSL2 (n,m) -> ( ( strict ) ( strict ) RelStr ) equals :: FINTOPO5:def 3
 RelStr(# [:(Seg n : ( ( ) ( ) RelStr ) ) : ( ( ) ( ) Element of bool NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,(Seg m : ( ( ) ( Relation-like n : ( ( ) ( ) RelStr ) -defined n : ( ( ) ( ) RelStr ) -valued ) Element of bool [:n : ( ( ) ( ) RelStr ) ,n : ( ( ) ( ) RelStr ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( ) set ) ,(Nbdl2 (n : ( ( ) ( ) RelStr ) ,m : ( ( ) ( Relation-like n : ( ( ) ( ) RelStr ) -defined n : ( ( ) ( ) RelStr ) -valued ) Element of bool [:n : ( ( ) ( ) RelStr ) ,n : ( ( ) ( ) RelStr ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) )) : ( ( ) ( Relation-like [:(Seg n : ( ( ) ( ) RelStr ) ) : ( ( ) ( ) Element of bool NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,(Seg m : ( ( ) ( Relation-like n : ( ( ) ( ) RelStr ) -defined n : ( ( ) ( ) RelStr ) -valued ) Element of bool [:n : ( ( ) ( ) RelStr ) ,n : ( ( ) ( ) RelStr ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( ) set ) -defined [:(Seg n : ( ( ) ( ) RelStr ) ) : ( ( ) ( ) Element of bool NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,(Seg m : ( ( ) ( Relation-like n : ( ( ) ( ) RelStr ) -defined n : ( ( ) ( ) RelStr ) -valued ) Element of bool [:n : ( ( ) ( ) RelStr ) ,n : ( ( ) ( ) RelStr ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( ) set ) -valued ) Relation of ) #) : ( ( strict ) ( strict ) RelStr ) ;
end;

registration
let n, m be ( ( non zero ) ( non zero V4() V5() V6() V10() complex V12() ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ;
cluster FTSL2 (n : ( ( non zero ) ( non zero V4() V5() V6() V10() complex V12() ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,m : ( ( non zero ) ( non zero V4() V5() V6() V10() complex V12() ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( strict ) RelStr ) -> non empty strict ;
end;

theorem :: FINTOPO5:11
for n, m being ( ( non zero ) ( non zero V4() V5() V6() V10() complex V12() ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) holds FTSL2 (n : ( ( non zero ) ( non zero V4() V5() V6() V10() complex V12() ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,m : ( ( non zero ) ( non zero V4() V5() V6() V10() complex V12() ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty strict ) RelStr ) is filled ;

theorem :: FINTOPO5:12
for n, m being ( ( non zero ) ( non zero V4() V5() V6() V10() complex V12() ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) holds FTSL2 (n : ( ( non zero ) ( non zero V4() V5() V6() V10() complex V12() ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,m : ( ( non zero ) ( non zero V4() V5() V6() V10() complex V12() ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty strict ) RelStr ) is symmetric ;

theorem :: FINTOPO5:13
for n being ( ( non zero ) ( non zero V4() V5() V6() V10() complex V12() ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ex h being ( ( Function-like quasi_total ) ( Relation-like the carrier of (FTSL2 (b1 : ( ( non zero ) ( non zero V4() V5() V6() V10() complex V12() ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (FTSL1 b1 : ( ( non zero ) ( non zero V4() V5() V6() V10() complex V12() ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st h : ( ( Function-like quasi_total ) ( Relation-like the carrier of (FTSL2 (b1 : ( ( non zero ) ( non zero V4() V5() V6() V10() complex V12() ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (FTSL1 b1 : ( ( non zero ) ( non zero V4() V5() V6() V10() complex V12() ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is being_homeomorphism ;

definition
let n, m be ( ( ) ( V4() V5() V6() V10() complex V12() ext-real non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ;
func Nbds2 (n,m) -> ( ( ) ( Relation-like [:(Seg n : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,(Seg m : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( ) set ) -defined [:(Seg n : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,(Seg m : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( ) set ) -valued ) Relation of ) means :: FINTOPO5:def 4
 for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in [:(Seg n : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,(Seg m : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( ) set ) holds
for i, j being ( ( ) ( V4() V5() V6() V10() complex V12() ext-real non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) st x : ( ( ) ( ) set ) = [i : ( ( ) ( V4() V5() V6() V10() complex V12() ext-real non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,j : ( ( ) ( V4() V5() V6() V10() complex V12() ext-real non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ] : ( ( ) ( ) set ) holds
Im (it : ( ( ) ( ) Element of n : ( ( ) ( ) set ) ) ,x : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like Seg n : ( ( ) ( ) set ) : ( ( ) ( ) Element of bool NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -defined Seg m : ( ( ) ( ) set ) : ( ( ) ( ) Element of bool NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -valued ) Subset of ( ( ) ( non empty ) set ) ) = [:{i : ( ( ) ( V4() V5() V6() V10() complex V12() ext-real non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty ) set ) ,(Im ((Nbdl1 m : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like Seg m : ( ( ) ( ) set ) : ( ( ) ( ) Element of bool NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -defined Seg m : ( ( ) ( ) set ) : ( ( ) ( ) Element of bool NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -valued ) Element of bool [:(Seg m : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,(Seg m : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,j : ( ( ) ( V4() V5() V6() V10() complex V12() ext-real non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( ) set ) \/ [:(Im ((Nbdl1 n : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like Seg n : ( ( ) ( ) set ) : ( ( ) ( ) Element of bool NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -defined Seg n : ( ( ) ( ) set ) : ( ( ) ( ) Element of bool NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -valued ) Element of bool [:(Seg n : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,(Seg n : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,i : ( ( ) ( V4() V5() V6() V10() complex V12() ext-real non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ,{j : ( ( ) ( V4() V5() V6() V10() complex V12() ext-real non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;
end;

definition
let n, m be ( ( ) ( V4() V5() V6() V10() complex V12() ext-real non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ;
func FTSS2 (n,m) -> ( ( strict ) ( strict ) RelStr ) equals :: FINTOPO5:def 5
 RelStr(# [:(Seg n : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,(Seg m : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( ) set ) ,(Nbds2 (n : ( ( ) ( ) set ) ,m : ( ( ) ( ) set ) )) : ( ( ) ( Relation-like [:(Seg n : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,(Seg m : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( ) set ) -defined [:(Seg n : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,(Seg m : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( ) set ) -valued ) Relation of ) #) : ( ( strict ) ( strict ) RelStr ) ;
end;

registration
let n, m be ( ( non zero ) ( non zero V4() V5() V6() V10() complex V12() ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ;
cluster FTSS2 (n : ( ( non zero ) ( non zero V4() V5() V6() V10() complex V12() ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,m : ( ( non zero ) ( non zero V4() V5() V6() V10() complex V12() ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( strict ) RelStr ) -> non empty strict ;
end;

theorem :: FINTOPO5:14
for n, m being ( ( non zero ) ( non zero V4() V5() V6() V10() complex V12() ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) holds FTSS2 (n : ( ( non zero ) ( non zero V4() V5() V6() V10() complex V12() ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,m : ( ( non zero ) ( non zero V4() V5() V6() V10() complex V12() ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty strict ) RelStr ) is filled ;

theorem :: FINTOPO5:15
for n, m being ( ( non zero ) ( non zero V4() V5() V6() V10() complex V12() ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) holds FTSS2 (n : ( ( non zero ) ( non zero V4() V5() V6() V10() complex V12() ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,m : ( ( non zero ) ( non zero V4() V5() V6() V10() complex V12() ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty strict ) RelStr ) is symmetric ;

theorem :: FINTOPO5:16
for n being ( ( non zero ) ( non zero V4() V5() V6() V10() complex V12() ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ex h being ( ( Function-like quasi_total ) ( Relation-like the carrier of (FTSS2 (b1 : ( ( non zero ) ( non zero V4() V5() V6() V10() complex V12() ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (FTSL1 b1 : ( ( non zero ) ( non zero V4() V5() V6() V10() complex V12() ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st h : ( ( Function-like quasi_total ) ( Relation-like the carrier of (FTSS2 (b1 : ( ( non zero ) ( non zero V4() V5() V6() V10() complex V12() ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty V4() V5() V6() V10() complex V12() ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (FTSL1 b1 : ( ( non zero ) ( non zero V4() V5() V6() V10() complex V12() ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is being_homeomorphism ;