:: TOPALG_3 semantic presentation

begin

theorem :: TOPALG_3:1
for A, B, a, b being ( ( ) ( ) set )
for f being ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of A : ( ( ) ( ) set ) ,B : ( ( ) ( ) set ) ) st a : ( ( ) ( ) set ) in A : ( ( ) ( ) set ) & b : ( ( ) ( ) set ) in B : ( ( ) ( ) set ) holds
f : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) ) +* (a : ( ( ) ( ) set ) .--> b : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like {b3 : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) -defined Function-like one-to-one ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) is ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of A : ( ( ) ( ) set ) ,B : ( ( ) ( ) set ) ) ;

theorem :: TOPALG_3:2
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function)
for X, x being ( ( ) ( ) set ) st f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) | X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like ) set ) is one-to-one & x : ( ( ) ( ) set ) in rng (f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) | X : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) holds
(f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) * ((f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) | X : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like Function-like ) set ) ") : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) ) : ( ( Relation-like ) ( Relation-like Function-like ) set ) . x : ( ( ) ( ) set ) : ( ( ) ( ) set ) = x : ( ( ) ( ) set ) ;

theorem :: TOPALG_3:3
for X, a, b being ( ( ) ( ) set )
for f being ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined {b2 : ( ( ) ( ) set ) ,b3 : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) -valued Function-like V26(b1 : ( ( ) ( ) set ) ) quasi_total ) Function of X : ( ( ) ( ) set ) ,{a : ( ( ) ( ) set ) ,b : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) ) holds X : ( ( ) ( ) set ) = (f : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined {b2 : ( ( ) ( ) set ) ,b3 : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) -valued Function-like V26(b1 : ( ( ) ( ) set ) ) quasi_total ) Function of b1 : ( ( ) ( ) set ) ,{b2 : ( ( ) ( ) set ) ,b3 : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) ) " {a : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) \/ (f : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined {b2 : ( ( ) ( ) set ) ,b3 : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) -valued Function-like V26(b1 : ( ( ) ( ) set ) ) quasi_total ) Function of b1 : ( ( ) ( ) set ) ,{b2 : ( ( ) ( ) set ) ,b3 : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) ) " {b : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: TOPALG_3:4
for S, T being ( ( non empty ) ( non empty ) 1-sorted )
for s being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for t being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds (S : ( ( non empty ) ( non empty ) 1-sorted ) --> t : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of bool [: the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) . s : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) = t : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ;

theorem :: TOPALG_3:5
for T being ( ( non empty ) ( non empty ) TopStruct )
for t being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) = {t : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty ) set ) holds
Sspace t : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( non empty strict ) ( non empty strict ) SubSpace of b1 : ( ( non empty ) ( non empty ) TopStruct ) ) = T : ( ( non empty ) ( non empty ) TopStruct ) | A : ( ( ) ( ) Subset of ) : ( ( strict ) ( strict ) SubSpace of b1 : ( ( non empty ) ( non empty ) TopStruct ) ) ;

theorem :: TOPALG_3:6
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for A, B being ( ( ) ( ) Subset of )
for C, D being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) = C : ( ( ) ( ) Subset of ) & B : ( ( ) ( ) Subset of ) = D : ( ( ) ( ) Subset of ) holds
( A : ( ( ) ( ) Subset of ) ,B : ( ( ) ( ) Subset of ) are_separated iff C : ( ( ) ( ) Subset of ) ,D : ( ( ) ( ) Subset of ) are_separated ) ;

theorem :: TOPALG_3:7
for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) holds
( T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is connected iff for f being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of (1TopSp {0 : ( ( ) ( empty V10() V11() V12() Relation-like non-empty empty-yielding Function-like one-to-one constant functional ext-real V168() V169() V192() V193() V194() V195() V196() V197() V198() Function-yielding V258() ) Element of K32() : ( ( ) ( V192() V193() V194() V195() V196() V197() V198() ) Element of bool K28() : ( ( ) ( V192() V193() V194() V198() ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty V10() V11() V12() ext-real V168() V169() V192() V193() V194() V195() V196() V197() ) Element of K32() : ( ( ) ( V192() V193() V194() V195() V196() V197() V198() ) Element of bool K28() : ( ( ) ( V192() V193() V194() V198() ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty V192() V193() V194() V195() V196() V197() ) set ) ) : ( ( ) ( non empty strict TopSpace-like V156() ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) holds
( not f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of (1TopSp {0 : ( ( ) ( empty V10() V11() V12() Relation-like non-empty empty-yielding Function-like one-to-one constant functional ext-real V168() V169() V192() V193() V194() V195() V196() V197() V198() Function-yielding V258() ) Element of K32() : ( ( ) ( V192() V193() V194() V195() V196() V197() V198() ) Element of bool K28() : ( ( ) ( V192() V193() V194() V198() ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty V10() V11() V12() ext-real V168() V169() V192() V193() V194() V195() V196() V197() ) Element of K32() : ( ( ) ( V192() V193() V194() V195() V196() V197() V198() ) Element of bool K28() : ( ( ) ( V192() V193() V194() V198() ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty V192() V193() V194() V195() V196() V197() ) set ) ) : ( ( ) ( non empty strict TopSpace-like V156() ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is continuous or not f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of (1TopSp {0 : ( ( ) ( empty V10() V11() V12() Relation-like non-empty empty-yielding Function-like one-to-one constant functional ext-real V168() V169() V192() V193() V194() V195() V196() V197() V198() Function-yielding V258() ) Element of K32() : ( ( ) ( V192() V193() V194() V195() V196() V197() V198() ) Element of bool K28() : ( ( ) ( V192() V193() V194() V198() ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty V10() V11() V12() ext-real V168() V169() V192() V193() V194() V195() V196() V197() ) Element of K32() : ( ( ) ( V192() V193() V194() V195() V196() V197() V198() ) Element of bool K28() : ( ( ) ( V192() V193() V194() V198() ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty V192() V193() V194() V195() V196() V197() ) set ) ) : ( ( ) ( non empty strict TopSpace-like V156() ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is onto ) ) ;

registration
cluster empty -> connected for ( ( ) ( ) TopStruct ) ;
end;

theorem :: TOPALG_3:8
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) st TopStruct(# the carrier of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the topology of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty open ) Element of bool (bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict TopSpace-like ) TopStruct ) is connected holds
T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) is connected ;

registration
let T be ( ( TopSpace-like connected ) ( TopSpace-like connected ) TopSpace) ;
cluster TopStruct(# the carrier of T : ( ( TopSpace-like connected ) ( TopSpace-like connected ) TopStruct ) : ( ( ) ( ) set ) , the topology of T : ( ( TopSpace-like connected ) ( TopSpace-like connected ) TopStruct ) : ( ( ) ( non empty open ) Element of bool (bool the carrier of T : ( ( TopSpace-like connected ) ( TopSpace-like connected ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict TopSpace-like ) TopStruct ) -> strict connected ;
end;

theorem :: TOPALG_3:9
for S, T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) st S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) are_homeomorphic & S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is pathwise_connected holds
T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is pathwise_connected ;

registration
cluster non empty trivial TopSpace-like -> non empty TopSpace-like pathwise_connected for ( ( ) ( ) TopStruct ) ;
end;

theorem :: TOPALG_3:10
for T being ( ( ) ( TopSpace-like ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty V10() V11() V12() ext-real V168() V169() V192() V193() V194() V195() V196() V197() ) Element of K32() : ( ( ) ( V192() V193() V194() V195() V196() V197() V198() ) Element of bool K28() : ( ( ) ( V192() V193() V194() V198() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( V207() ) ( non empty TopSpace-like V89() V117() V118() V119() V120() V121() V122() V123() V207() ) L18()) ) st the carrier of T : ( ( ) ( TopSpace-like ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty V10() V11() V12() ext-real V168() V169() V192() V193() V194() V195() V196() V197() ) Element of K32() : ( ( ) ( V192() V193() V194() V195() V196() V197() V198() ) Element of bool K28() : ( ( ) ( V192() V193() V194() V198() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( V207() ) ( non empty TopSpace-like V89() V117() V118() V119() V120() V121() V122() V123() V207() ) L18()) ) : ( ( ) ( ) set ) is ( ( being_simple_closed_curve ) ( non empty compact being_simple_closed_curve ) Simple_closed_curve) holds
T : ( ( ) ( TopSpace-like ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty V10() V11() V12() ext-real V168() V169() V192() V193() V194() V195() V196() V197() ) Element of K32() : ( ( ) ( V192() V193() V194() V195() V196() V197() V198() ) Element of bool K28() : ( ( ) ( V192() V193() V194() V198() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( V207() ) ( non empty TopSpace-like V89() V117() V118() V119() V120() V121() V122() V123() V207() ) L18()) ) is pathwise_connected ;

theorem :: TOPALG_3:11
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ex F being ( ( ) ( ) Subset-Family of ) st
( F : ( ( ) ( ) Subset-Family of ) = { the carrier of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) & F : ( ( ) ( ) Subset-Family of ) is ( ( ) ( ) Cover of ( ( ) ( ) set ) ) & F : ( ( ) ( ) Subset-Family of ) is open ) ;

registration
let T be ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ;
cluster non empty open closed mutually-disjoint for ( ( ) ( ) Element of bool (bool the carrier of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

theorem :: TOPALG_3:12
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for D being ( ( open mutually-disjoint ) ( open mutually-disjoint ) Subset-Family of )
for A being ( ( ) ( ) Subset of )
for X being ( ( ) ( ) set ) st A : ( ( ) ( ) Subset of ) is connected & X : ( ( ) ( ) set ) in D : ( ( open mutually-disjoint ) ( open mutually-disjoint ) Subset-Family of ) & X : ( ( ) ( ) set ) meets A : ( ( ) ( ) Subset of ) & D : ( ( open mutually-disjoint ) ( open mutually-disjoint ) Subset-Family of ) is ( ( ) ( ) Cover of A : ( ( ) ( ) Subset of ) ) holds
A : ( ( ) ( ) Subset of ) c= X : ( ( ) ( ) set ) ;

begin

theorem :: TOPALG_3:13
for S, T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) holds TopStruct(# the carrier of [:S : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ,T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( strict TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) , the topology of [:S : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ,T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty open ) Element of bool (bool the carrier of [:b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ,b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( strict TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict TopSpace-like ) TopStruct ) = [:TopStruct(# the carrier of S : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the topology of S : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty open ) Element of bool (bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict TopSpace-like ) TopStruct ) ,TopStruct(# the carrier of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the topology of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty open ) Element of bool (bool the carrier of b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict TopSpace-like ) TopStruct ) :] : ( ( strict TopSpace-like ) ( strict TopSpace-like ) TopStruct ) ;

theorem :: TOPALG_3:14
for S, T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for A being ( ( ) ( ) Subset of )
for B being ( ( ) ( ) Subset of ) holds Cl [:A : ( ( ) ( ) Subset of ) ,B : ( ( ) ( ) Subset of ) :] : ( ( ) ( Relation-like ) Element of bool the carrier of [:b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ,b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( strict TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( closed ) Element of bool the carrier of [:b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ,b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( strict TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = [:(Cl A : ( ( ) ( ) Subset of ) ) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,(Cl B : ( ( ) ( ) Subset of ) ) : ( ( ) ( closed ) Element of bool the carrier of b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( Relation-like ) Element of bool the carrier of [:b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ,b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( strict TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: TOPALG_3:15
for S, T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for A being ( ( closed ) ( closed ) Subset of )
for B being ( ( closed ) ( closed ) Subset of ) holds [:A : ( ( closed ) ( closed ) Subset of ) ,B : ( ( closed ) ( closed ) Subset of ) :] : ( ( ) ( Relation-like ) Element of bool the carrier of [:b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ,b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( strict TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) is closed ;

registration
let A, B be ( ( TopSpace-like connected ) ( TopSpace-like connected ) TopSpace) ;
cluster [:A : ( ( TopSpace-like connected ) ( TopSpace-like connected ) TopStruct ) ,B : ( ( TopSpace-like connected ) ( TopSpace-like connected ) TopStruct ) :] : ( ( strict TopSpace-like ) ( strict TopSpace-like ) TopStruct ) -> strict TopSpace-like connected ;
end;

theorem :: TOPALG_3:16
for S, T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for A being ( ( ) ( ) Subset of )
for B being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is connected & B : ( ( ) ( ) Subset of ) is connected holds
[:A : ( ( ) ( ) Subset of ) ,B : ( ( ) ( ) Subset of ) :] : ( ( ) ( Relation-like ) Element of bool the carrier of [:b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ,b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( strict TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) is connected ;

theorem :: TOPALG_3:17
for S, T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for Y being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for A being ( ( ) ( ) Subset of )
for f being ( ( Function-like quasi_total ) ( Relation-like the carrier of [:b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ,b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( strict TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of [:b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ,b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( strict TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) ) quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) )
for g being ( ( Function-like quasi_total ) ( Relation-like the carrier of [:(b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) | b4 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) ,b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( strict TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of [:(b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) | b4 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) ,b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( strict TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) ) quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) st g : ( ( Function-like quasi_total ) ( Relation-like the carrier of [:(b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) | b4 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) ,b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( strict TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of [:(b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) | b4 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) ,b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( strict TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) ) quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) = f : ( ( Function-like quasi_total ) ( Relation-like the carrier of [:b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ,b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( strict TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of [:b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ,b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( strict TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) ) quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) | [:A : ( ( ) ( ) Subset of ) , the carrier of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( Function-like ) ( Relation-like [:b4 : ( ( ) ( ) Subset of ) , the carrier of b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) -defined the carrier of [:b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ,b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( strict TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of bool [: the carrier of [:b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ,b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( strict TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) , the carrier of b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) & f : ( ( Function-like quasi_total ) ( Relation-like the carrier of [:b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ,b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( strict TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of [:b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ,b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( strict TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) ) quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) is continuous holds
g : ( ( Function-like quasi_total ) ( Relation-like the carrier of [:(b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) | b4 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) ,b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( strict TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of [:(b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) | b4 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) ,b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( strict TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) ) quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) is continuous ;

theorem :: TOPALG_3:18
for S, T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for Y being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for A being ( ( ) ( ) Subset of )
for f being ( ( Function-like quasi_total ) ( Relation-like the carrier of [:b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ,b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( strict TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of [:b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ,b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( strict TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) ) quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) )
for g being ( ( Function-like quasi_total ) ( Relation-like the carrier of [:b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ,(b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) | b4 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) :] : ( ( strict TopSpace-like ) ( strict TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of [:b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ,(b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) | b4 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) :] : ( ( strict TopSpace-like ) ( strict TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) ) quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) st g : ( ( Function-like quasi_total ) ( Relation-like the carrier of [:b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ,(b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) | b4 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) :] : ( ( strict TopSpace-like ) ( strict TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of [:b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ,(b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) | b4 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) :] : ( ( strict TopSpace-like ) ( strict TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) ) quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) = f : ( ( Function-like quasi_total ) ( Relation-like the carrier of [:b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ,b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( strict TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of [:b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ,b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( strict TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) ) quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) | [: the carrier of S : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ,A : ( ( ) ( ) Subset of ) :] : ( ( ) ( Relation-like ) set ) : ( ( Function-like ) ( Relation-like [: the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ,b4 : ( ( ) ( ) Subset of ) :] : ( ( ) ( Relation-like ) set ) -defined the carrier of [:b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ,b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( strict TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of bool [: the carrier of [:b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ,b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( strict TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) , the carrier of b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) & f : ( ( Function-like quasi_total ) ( Relation-like the carrier of [:b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ,b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( strict TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of [:b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ,b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( strict TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) ) quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) is continuous holds
g : ( ( Function-like quasi_total ) ( Relation-like the carrier of [:b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ,(b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) | b4 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) :] : ( ( strict TopSpace-like ) ( strict TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of [:b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ,(b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) | b4 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) :] : ( ( strict TopSpace-like ) ( strict TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) ) quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) is continuous ;

theorem :: TOPALG_3:19
for S, T, T1, T2, Y being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f being ( ( Function-like quasi_total ) ( Relation-like the carrier of [:b5 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) )
for g being ( ( Function-like quasi_total ) ( Relation-like the carrier of [:b5 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b4 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) )
for F1, F2 being ( ( closed ) ( closed ) Subset of ) st T1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is ( ( ) ( TopSpace-like ) SubSpace of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) & T2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is ( ( ) ( TopSpace-like ) SubSpace of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) & F1 : ( ( closed ) ( closed ) Subset of ) = [#] T1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty non proper open closed ) Element of bool the carrier of b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) & F2 : ( ( closed ) ( closed ) Subset of ) = [#] T2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty non proper open closed ) Element of bool the carrier of b4 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) & ([#] T1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty non proper open closed ) Element of bool the carrier of b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) \/ ([#] T2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty non proper open closed ) Element of bool the carrier of b4 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) = [#] T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty non proper open closed ) Element of bool the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) & f : ( ( Function-like quasi_total ) ( Relation-like the carrier of [:b5 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is continuous & g : ( ( Function-like quasi_total ) ( Relation-like the carrier of [:b5 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b4 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is continuous & ( for p being ( ( ) ( ) set ) st p : ( ( Function-like quasi_total ) ( Relation-like the carrier of [:b5 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) in ([#] [:Y : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,T1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty non proper open closed ) Element of bool the carrier of [:b5 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) /\ ([#] [:Y : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,T2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty non proper open closed ) Element of bool the carrier of [:b5 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b4 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of [:b5 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b4 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) holds
f : ( ( Function-like quasi_total ) ( Relation-like the carrier of [:b5 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . p : ( ( Function-like quasi_total ) ( Relation-like the carrier of [:b5 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) = g : ( ( Function-like quasi_total ) ( Relation-like the carrier of [:b5 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b4 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . p : ( ( Function-like quasi_total ) ( Relation-like the carrier of [:b5 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) holds
ex h being ( ( Function-like quasi_total ) ( Relation-like the carrier of [:b5 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( 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 [:b5 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) = f : ( ( Function-like quasi_total ) ( Relation-like the carrier of [:b5 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) +* g : ( ( Function-like quasi_total ) ( Relation-like the carrier of [:b5 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b4 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( 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 ) & h : ( ( Function-like quasi_total ) ( Relation-like the carrier of [:b5 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is continuous ) ;

theorem :: TOPALG_3:20
for S, T, T1, T2, Y being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f being ( ( Function-like quasi_total ) ( Relation-like the carrier of [:b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b5 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) )
for g being ( ( Function-like quasi_total ) ( Relation-like the carrier of [:b4 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b5 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) )
for F1, F2 being ( ( closed ) ( closed ) Subset of ) st T1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is ( ( ) ( TopSpace-like ) SubSpace of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) & T2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is ( ( ) ( TopSpace-like ) SubSpace of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) & F1 : ( ( closed ) ( closed ) Subset of ) = [#] T1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty non proper open closed ) Element of bool the carrier of b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) & F2 : ( ( closed ) ( closed ) Subset of ) = [#] T2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty non proper open closed ) Element of bool the carrier of b4 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) & ([#] T1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty non proper open closed ) Element of bool the carrier of b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) \/ ([#] T2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty non proper open closed ) Element of bool the carrier of b4 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) = [#] T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty non proper open closed ) Element of bool the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) & f : ( ( Function-like quasi_total ) ( Relation-like the carrier of [:b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b5 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is continuous & g : ( ( Function-like quasi_total ) ( Relation-like the carrier of [:b4 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b5 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is continuous & ( for p being ( ( ) ( ) set ) st p : ( ( Function-like quasi_total ) ( Relation-like the carrier of [:b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b5 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) in ([#] [:T1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,Y : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty non proper open closed ) Element of bool the carrier of [:b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b5 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) /\ ([#] [:T2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,Y : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty non proper open closed ) Element of bool the carrier of [:b4 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b5 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of [:b4 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b5 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) holds
f : ( ( Function-like quasi_total ) ( Relation-like the carrier of [:b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b5 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . p : ( ( Function-like quasi_total ) ( Relation-like the carrier of [:b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b5 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) = g : ( ( Function-like quasi_total ) ( Relation-like the carrier of [:b4 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b5 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . p : ( ( Function-like quasi_total ) ( Relation-like the carrier of [:b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b5 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) holds
ex h being ( ( Function-like quasi_total ) ( Relation-like the carrier of [:b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b5 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( 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 [:b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b5 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) = f : ( ( Function-like quasi_total ) ( Relation-like the carrier of [:b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b5 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) +* g : ( ( Function-like quasi_total ) ( Relation-like the carrier of [:b4 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b5 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( 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 ) & h : ( ( Function-like quasi_total ) ( Relation-like the carrier of [:b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b5 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is continuous ) ;

begin

registration
let T be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
let t be ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ;
cluster -> continuous for ( ( ) ( ) Path of t : ( ( non empty V260() V261() ) ( non empty V260() V261() ) L9()) ,t : ( ( non empty V260() V261() ) ( non empty V260() V261() ) L9()) ) ;
end;

theorem :: TOPALG_3:21
for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for t being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for x being ( ( ) ( V11() V12() ext-real ) Point of ( ( ) ( non empty V192() V193() V194() ) set ) )
for P being ( ( constant ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like constant V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total continuous ) Loop of t : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) holds P : ( ( constant ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like constant V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total continuous ) Loop of b2 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) . x : ( ( ) ( V11() V12() ext-real ) Point of ( ( ) ( non empty V192() V193() V194() ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) = t : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ;

theorem :: TOPALG_3:22
for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for t being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for P being ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total continuous ) Loop of t : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) holds
( P : ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total continuous ) Loop of b2 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) . 0 : ( ( ) ( empty V10() V11() V12() Relation-like non-empty empty-yielding Function-like one-to-one constant functional ext-real V168() V169() V192() V193() V194() V195() V196() V197() V198() Function-yielding V258() ) Element of K32() : ( ( ) ( V192() V193() V194() V195() V196() V197() V198() ) Element of bool K28() : ( ( ) ( V192() V193() V194() V198() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) = t : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) & P : ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total continuous ) Loop of b2 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) . 1 : ( ( ) ( non empty V10() V11() V12() ext-real V168() V169() V192() V193() V194() V195() V196() V197() ) Element of K32() : ( ( ) ( V192() V193() V194() V195() V196() V197() V198() ) Element of bool K28() : ( ( ) ( V192() V193() V194() V198() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) = t : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ;

theorem :: TOPALG_3:23
for S, T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f being ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) )
for a, b being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) are_connected holds
f : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ,f : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) are_connected ;

theorem :: TOPALG_3:24
for S, T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f being ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) )
for a, b being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for P being ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total ) Path of a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) st a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) are_connected holds
f : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) * P : ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total ) Path of b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b5 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total ) Element of bool [: the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) is ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total ) Path of f : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ,f : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: TOPALG_3:25
for S being ( ( non empty TopSpace-like pathwise_connected ) ( non empty TopSpace-like connected pathwise_connected ) TopSpace)
for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f being ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like pathwise_connected ) ( non empty TopSpace-like connected pathwise_connected ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like pathwise_connected ) ( non empty TopSpace-like connected pathwise_connected ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) )
for a, b being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for P being ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like pathwise_connected ) ( non empty TopSpace-like connected pathwise_connected ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total continuous ) Path of a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) holds f : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like pathwise_connected ) ( non empty TopSpace-like connected pathwise_connected ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like pathwise_connected ) ( non empty TopSpace-like connected pathwise_connected ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) * P : ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like pathwise_connected ) ( non empty TopSpace-like connected pathwise_connected ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total continuous ) Path of b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b5 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total continuous ) Element of bool [: the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) is ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total ) Path of f : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like pathwise_connected ) ( non empty TopSpace-like connected pathwise_connected ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like pathwise_connected ) ( non empty TopSpace-like connected pathwise_connected ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ,f : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like pathwise_connected ) ( non empty TopSpace-like connected pathwise_connected ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like pathwise_connected ) ( non empty TopSpace-like connected pathwise_connected ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) ;

definition
let S be ( ( non empty TopSpace-like pathwise_connected ) ( non empty TopSpace-like connected pathwise_connected ) TopSpace) ;
let T be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
let a, b be ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ;
let P be ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of S : ( ( non empty TopSpace-like pathwise_connected ) ( non empty TopSpace-like connected pathwise_connected ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total continuous ) Path of a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ;
let f be ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of S : ( ( non empty TopSpace-like pathwise_connected ) ( non empty TopSpace-like connected pathwise_connected ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of S : ( ( non empty TopSpace-like pathwise_connected ) ( non empty TopSpace-like connected pathwise_connected ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ;
:: original: *
redefine func f * P -> ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of T : ( ( non empty V260() V261() ) ( non empty V260() V261() ) L9()) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total ) Path of f : ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of S : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total continuous ) Path of a : ( ( ) ( ) Element of S : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) ,b : ( ( ) ( ) set ) ) . a : ( ( ) ( ) Element of S : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( ) Element of the carrier of T : ( ( non empty V260() V261() ) ( non empty V260() V261() ) L9()) : ( ( ) ( non empty ) set ) ) ,f : ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of S : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total continuous ) Path of a : ( ( ) ( ) Element of S : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) ,b : ( ( ) ( ) set ) ) . b : ( ( ) ( ) set ) : ( ( ) ( ) Element of the carrier of T : ( ( non empty V260() V261() ) ( non empty V260() V261() ) L9()) : ( ( ) ( non empty ) set ) ) ) ;
end;

theorem :: TOPALG_3:26
for S, T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f being ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) )
for a being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for P being ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total continuous ) Loop of a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) holds f : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) * P : ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total continuous ) Loop of b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total continuous ) Element of bool [: the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) is ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total continuous ) Loop of f : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) ;

definition
let S, T be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
let a be ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ;
let P be ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total continuous ) Loop of a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ;
let f be ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ;
:: original: *
redefine func f * P -> ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of T : ( ( non empty V260() V261() ) ( non empty V260() V261() ) L9()) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total continuous ) Loop of f : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total continuous ) Element of bool [: the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) , the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) . a : ( ( ) ( ) Element of S : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( ) Element of the carrier of T : ( ( non empty V260() V261() ) ( non empty V260() V261() ) L9()) : ( ( ) ( non empty ) set ) ) ) ;
end;

theorem :: TOPALG_3:27
for S, T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f being ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) )
for a, b being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for P, Q being ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total ) Path of a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) )
for P1, Q1 being ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total ) Path of f : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ,f : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) st P : ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total ) Path of b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b5 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ,Q : ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total ) Path of b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b5 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) are_homotopic & P1 : ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total ) Path of b3 : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ,b3 : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . b5 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) = f : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) * P : ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total ) Path of b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b5 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total ) Element of bool [: the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) & Q1 : ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total ) Path of b3 : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ,b3 : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . b5 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) = f : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) * Q : ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total ) Path of b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b5 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total ) Element of bool [: the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) holds
P1 : ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total ) Path of b3 : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ,b3 : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . b5 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) ,Q1 : ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total ) Path of b3 : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ,b3 : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . b5 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) are_homotopic ;

theorem :: TOPALG_3:28
for S, T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f being ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) )
for a, b being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for P, Q being ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total ) Path of a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) )
for P1, Q1 being ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total ) Path of f : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ,f : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) )
for F being ( ( ) ( non empty Relation-like the carrier of [:K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) ,K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of [:K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) ,K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected ) TopStruct ) : ( ( ) ( non empty ) set ) ) quasi_total ) Homotopy of P : ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total ) Path of b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b5 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ,Q : ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total ) Path of b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b5 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ) st P : ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total ) Path of b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b5 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ,Q : ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total ) Path of b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b5 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) are_homotopic & P1 : ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total ) Path of b3 : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ,b3 : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . b5 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) = f : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) * P : ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total ) Path of b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b5 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total ) Element of bool [: the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) & Q1 : ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total ) Path of b3 : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ,b3 : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . b5 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) = f : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) * Q : ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total ) Path of b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b5 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total ) Element of bool [: the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) holds
f : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) * F : ( ( ) ( non empty Relation-like the carrier of [:K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) ,K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of [:K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) ,K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected ) TopStruct ) : ( ( ) ( non empty ) set ) ) quasi_total ) Homotopy of b6 : ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total ) Path of b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b5 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ,b7 : ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total ) Path of b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b5 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ) : ( ( Function-like ) ( non empty Relation-like the carrier of [:K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) ,K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of [:K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) ,K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected ) TopStruct ) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of bool [: the carrier of [:K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) ,K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected ) TopStruct ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) is ( ( ) ( non empty Relation-like the carrier of [:K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) ,K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of [:K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) ,K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected ) TopStruct ) : ( ( ) ( non empty ) set ) ) quasi_total ) Homotopy of P1 : ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total ) Path of b3 : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ,b3 : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . b5 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) ,Q1 : ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total ) Path of b3 : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ,b3 : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . b5 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: TOPALG_3:29
for S, T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f being ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) )
for a, b, c being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for P being ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total ) Path of a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) )
for Q being ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total ) Path of b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) )
for P1 being ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total ) Path of f : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ,f : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) )
for Q1 being ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total ) Path of f : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ,f : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . c : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) st a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) are_connected & b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) are_connected & P1 : ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total ) Path of b3 : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ,b3 : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . b5 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) = f : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) * P : ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total ) Path of b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b5 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total ) Element of bool [: the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) & Q1 : ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total ) Path of b3 : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . b5 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ,b3 : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . b6 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) = f : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) * Q : ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total ) Path of b5 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b6 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total ) Element of bool [: the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) holds
P1 : ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total ) Path of b3 : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ,b3 : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . b5 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) + Q1 : ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total ) Path of b3 : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . b5 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ,b3 : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . b6 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total ) Path of b3 : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ,b3 : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . b6 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) = f : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) * (P : ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total ) Path of b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b5 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) + Q : ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total ) Path of b5 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b6 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total ) Path of b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b6 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total ) Element of bool [: the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ;

definition
let S, T be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
let s be ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ;
let f be ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ;
assume f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is continuous ;
func FundGrIso (f,s) -> ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (pi_1 (S : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ,s : ( ( ) ( ) Element of S : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) )) : ( ( strict ) ( strict ) L9()) : ( ( ) ( ) set ) -defined the carrier of (pi_1 (T : ( ( non empty V260() V261() ) ( non empty V260() V261() ) L9()) ,(f : ( ( ) ( ) set ) . s : ( ( ) ( ) Element of S : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) ) : ( ( ) ( ) Element of the carrier of T : ( ( non empty V260() V261() ) ( non empty V260() V261() ) L9()) : ( ( ) ( non empty ) set ) ) )) : ( ( strict ) ( strict ) L9()) : ( ( ) ( ) set ) -valued Function-like V26( the carrier of (pi_1 (S : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ,s : ( ( ) ( ) Element of S : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) )) : ( ( strict ) ( strict ) L9()) : ( ( ) ( ) set ) ) quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) means :: TOPALG_3:def 1
 for x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) ex ls being ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of S : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total continuous ) Loop of s : ( ( ) ( ) Element of S : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) ) st
( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = Class ((EqRel (S : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ,s : ( ( ) ( ) Element of S : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) )) : ( ( ) ( Relation-like Loops s : ( ( ) ( ) Element of S : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( ) set ) -defined Loops s : ( ( ) ( ) Element of S : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( ) set ) -valued ) Element of bool [:(Loops s : ( ( ) ( ) Element of S : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) ) : ( ( ) ( ) set ) ,(Loops s : ( ( ) ( ) Element of S : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ,ls : ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total continuous ) Loop of s : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of bool (Loops s : ( ( ) ( ) Element of S : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) & it : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total continuous ) Element of bool [: the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) , the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (pi_1 (T : ( ( non empty V260() V261() ) ( non empty V260() V261() ) L9()) ,(f : ( ( ) ( ) set ) . s : ( ( ) ( ) Element of S : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) ) : ( ( ) ( ) Element of the carrier of T : ( ( non empty V260() V261() ) ( non empty V260() V261() ) L9()) : ( ( ) ( non empty ) set ) ) )) : ( ( strict ) ( strict ) L9()) : ( ( ) ( ) set ) ) = Class ((EqRel (T : ( ( non empty V260() V261() ) ( non empty V260() V261() ) L9()) ,(f : ( ( ) ( ) set ) . s : ( ( ) ( ) Element of S : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) ) : ( ( ) ( ) Element of the carrier of T : ( ( non empty V260() V261() ) ( non empty V260() V261() ) L9()) : ( ( ) ( non empty ) set ) ) )) : ( ( ) ( Relation-like Loops (f : ( ( ) ( ) set ) . s : ( ( ) ( ) Element of S : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) ) : ( ( ) ( ) Element of the carrier of T : ( ( non empty V260() V261() ) ( non empty V260() V261() ) L9()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) -defined Loops (f : ( ( ) ( ) set ) . s : ( ( ) ( ) Element of S : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) ) : ( ( ) ( ) Element of the carrier of T : ( ( non empty V260() V261() ) ( non empty V260() V261() ) L9()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) -valued ) Element of bool [:(Loops (f : ( ( ) ( ) set ) . s : ( ( ) ( ) Element of S : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) ) : ( ( ) ( ) Element of the carrier of T : ( ( non empty V260() V261() ) ( non empty V260() V261() ) L9()) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ,(Loops (f : ( ( ) ( ) set ) . s : ( ( ) ( ) Element of S : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) ) : ( ( ) ( ) Element of the carrier of T : ( ( non empty V260() V261() ) ( non empty V260() V261() ) L9()) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ,(f : ( ( ) ( ) set ) * ls : ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total continuous ) Loop of s : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ) : ( ( Function-like ) ( Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of T : ( ( non empty V260() V261() ) ( non empty V260() V261() ) L9()) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of bool [: the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) , the carrier of T : ( ( non empty V260() V261() ) ( non empty V260() V261() ) L9()) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool (Loops (f : ( ( ) ( ) set ) . s : ( ( ) ( ) Element of S : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) ) : ( ( ) ( ) Element of the carrier of T : ( ( non empty V260() V261() ) ( non empty V260() V261() ) L9()) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) );
end;

theorem :: TOPALG_3:30
for S, T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for s being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for f being ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) )
for ls being ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total continuous ) Loop of s : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) holds (FundGrIso (f : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ,s : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (pi_1 (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) )) : ( ( strict ) ( non empty strict V260() V261() ) L9()) : ( ( ) ( non empty ) set ) -defined the carrier of (pi_1 (b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,(b4 : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) )) : ( ( strict ) ( non empty strict V260() V261() ) L9()) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of (pi_1 (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) )) : ( ( strict ) ( non empty strict V260() V261() ) L9()) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . (Class ((EqRel (S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,s : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( non empty Relation-like Loops b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) -defined Loops b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) -valued V26( Loops b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) quasi_total V240() V245() ) Element of bool [:(Loops b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) ,(Loops b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ,ls : ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total continuous ) Loop of b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) )) : ( ( ) ( ) Element of bool (Loops b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) = Class ((EqRel (T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,(f : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . s : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) )) : ( ( ) ( non empty Relation-like Loops (b4 : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) -defined Loops (b4 : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) -valued V26( Loops (b4 : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) quasi_total V240() V245() ) Element of bool [:(Loops (b4 : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) ,(Loops (b4 : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ,(f : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) * ls : ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total continuous ) Loop of b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total continuous ) Loop of b4 : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of bool (Loops (b4 : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

registration
let S, T be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
let s be ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ;
let f be ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ;
cluster FundGrIso (f : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Element of bool [: the carrier of S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ,s : ( ( ) ( ) Element of the carrier of S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (pi_1 (S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ,s : ( ( ) ( ) Element of the carrier of S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) )) : ( ( strict ) ( non empty strict V260() V261() ) L9()) : ( ( ) ( non empty ) set ) -defined the carrier of (pi_1 (T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ,(f : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Element of bool [: the carrier of S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) . s : ( ( ) ( ) Element of the carrier of S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) )) : ( ( strict ) ( non empty strict V260() V261() ) L9()) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of (pi_1 (S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ,s : ( ( ) ( ) Element of the carrier of S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) )) : ( ( strict ) ( non empty strict V260() V261() ) L9()) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) -> Function-like quasi_total multiplicative ;
end;

theorem :: TOPALG_3:31
for S, T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for s being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for f being ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st f : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is being_homeomorphism holds
FundGrIso (f : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ,s : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (pi_1 (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) )) : ( ( strict ) ( non empty strict V260() V261() ) L9()) : ( ( ) ( non empty ) set ) -defined the carrier of (pi_1 (b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,(b4 : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) )) : ( ( strict ) ( non empty strict V260() V261() ) L9()) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of (pi_1 (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) )) : ( ( strict ) ( non empty strict V260() V261() ) L9()) : ( ( ) ( non empty ) set ) ) quasi_total V264( pi_1 (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty strict V260() V261() ) L9()) , pi_1 (b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,(b4 : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty strict V260() V261() ) L9()) ) multiplicative ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is bijective ;

theorem :: TOPALG_3:32
for S, T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for s being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for t being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for f being ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) )
for P being ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total ) Path of t : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,f : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . s : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) )
for h being ( ( Function-like quasi_total multiplicative ) ( non empty Relation-like the carrier of (pi_1 (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) )) : ( ( strict ) ( non empty strict V260() V261() ) L9()) : ( ( ) ( non empty ) set ) -defined the carrier of (pi_1 (b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) )) : ( ( strict ) ( non empty strict V260() V261() ) L9()) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of (pi_1 (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) )) : ( ( strict ) ( non empty strict V260() V261() ) L9()) : ( ( ) ( non empty ) set ) ) quasi_total V264( pi_1 (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty strict V260() V261() ) L9()) , pi_1 (b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty strict V260() V261() ) L9()) ) multiplicative ) Homomorphism of pi_1 (S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,s : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty strict V260() V261() ) L9()) , pi_1 (T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,t : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty strict V260() V261() ) L9()) ) st f : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is being_homeomorphism & f : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . s : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ,t : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) are_connected & h : ( ( Function-like quasi_total multiplicative ) ( non empty Relation-like the carrier of (pi_1 (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) )) : ( ( strict ) ( non empty strict V260() V261() ) L9()) : ( ( ) ( non empty ) set ) -defined the carrier of (pi_1 (b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) )) : ( ( strict ) ( non empty strict V260() V261() ) L9()) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of (pi_1 (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) )) : ( ( strict ) ( non empty strict V260() V261() ) L9()) : ( ( ) ( non empty ) set ) ) quasi_total V264( pi_1 (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty strict V260() V261() ) L9()) , pi_1 (b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty strict V260() V261() ) L9()) ) multiplicative ) Homomorphism of pi_1 (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty strict V260() V261() ) L9()) , pi_1 (b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty strict V260() V261() ) L9()) ) = (pi_1-iso P : ( ( ) ( non empty Relation-like the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of K527() : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected ) SubSpace of K525() : ( ( TopSpace-like ) ( non empty strict TopSpace-like V255() ) TopStruct ) ) : ( ( ) ( non empty V192() V193() V194() ) set ) ) quasi_total ) Path of b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b5 : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (FundamentalGroup (b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,(b5 : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) )) : ( ( strict ) ( non empty strict V260() V261() ) L9()) : ( ( ) ( non empty ) set ) -defined the carrier of (FundamentalGroup (b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) )) : ( ( strict ) ( non empty strict V260() V261() ) L9()) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of (FundamentalGroup (b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,(b5 : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) )) : ( ( strict ) ( non empty strict V260() V261() ) L9()) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of bool [: the carrier of (FundamentalGroup (b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,(b5 : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) )) : ( ( strict ) ( non empty strict V260() V261() ) L9()) : ( ( ) ( non empty ) set ) , the carrier of (FundamentalGroup (b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) )) : ( ( strict ) ( non empty strict V260() V261() ) L9()) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) * (FundGrIso (f : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ,s : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (pi_1 (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) )) : ( ( strict ) ( non empty strict V260() V261() ) L9()) : ( ( ) ( non empty ) set ) -defined the carrier of (pi_1 (b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,(b5 : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) )) : ( ( strict ) ( non empty strict V260() V261() ) L9()) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of (pi_1 (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) )) : ( ( strict ) ( non empty strict V260() V261() ) L9()) : ( ( ) ( non empty ) set ) ) quasi_total V264( pi_1 (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty strict V260() V261() ) L9()) , pi_1 (b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,(b5 : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty strict V260() V261() ) L9()) ) multiplicative ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( Function-like ) ( non empty Relation-like the carrier of (pi_1 (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) )) : ( ( strict ) ( non empty strict V260() V261() ) L9()) : ( ( ) ( non empty ) set ) -defined the carrier of (FundamentalGroup (b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) )) : ( ( strict ) ( non empty strict V260() V261() ) L9()) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of (pi_1 (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) )) : ( ( strict ) ( non empty strict V260() V261() ) L9()) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of bool [: the carrier of (pi_1 (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) )) : ( ( strict ) ( non empty strict V260() V261() ) L9()) : ( ( ) ( non empty ) set ) , the carrier of (FundamentalGroup (b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) )) : ( ( strict ) ( non empty strict V260() V261() ) L9()) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) holds
h : ( ( Function-like quasi_total multiplicative ) ( non empty Relation-like the carrier of (pi_1 (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) )) : ( ( strict ) ( non empty strict V260() V261() ) L9()) : ( ( ) ( non empty ) set ) -defined the carrier of (pi_1 (b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) )) : ( ( strict ) ( non empty strict V260() V261() ) L9()) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of (pi_1 (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) )) : ( ( strict ) ( non empty strict V260() V261() ) L9()) : ( ( ) ( non empty ) set ) ) quasi_total V264( pi_1 (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty strict V260() V261() ) L9()) , pi_1 (b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty strict V260() V261() ) L9()) ) multiplicative ) Homomorphism of pi_1 (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty strict V260() V261() ) L9()) , pi_1 (b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty strict V260() V261() ) L9()) ) is bijective ;

theorem :: TOPALG_3:33
for S being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for T being ( ( non empty TopSpace-like pathwise_connected ) ( non empty TopSpace-like connected pathwise_connected ) TopSpace)
for s being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for t being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,T : ( ( non empty TopSpace-like pathwise_connected ) ( non empty TopSpace-like connected pathwise_connected ) TopSpace) are_homeomorphic holds
pi_1 (S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,s : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty strict V260() V261() ) L9()) , pi_1 (T : ( ( non empty TopSpace-like pathwise_connected ) ( non empty TopSpace-like connected pathwise_connected ) TopSpace) ,t : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty strict V260() V261() ) L9()) are_isomorphic ;