:: DECOMP_1 semantic presentation

begin

definition
let T be ( ( ) ( ) TopStruct ) ;
mode alpha-set of T -> ( ( ) ( ) Subset of ) means :: DECOMP_1:def 1
it : ( ( ) ( ) Element of K10(K10(T : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) c= Int (Cl (Int it : ( ( ) ( ) Element of K10(K10(T : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K10( the U1 of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K10( the U1 of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K10( the U1 of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ;
let IT be ( ( ) ( ) Subset of ) ;
attr IT is semi-open means :: DECOMP_1:def 2
IT : ( ( ) ( ) Element of K10(K10(T : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) c= Cl (Int IT : ( ( ) ( ) Element of K10(K10(T : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K10( the U1 of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K10( the U1 of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ;
attr IT is pre-open means :: DECOMP_1:def 3
IT : ( ( ) ( ) Element of K10(K10(T : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) c= Int (Cl IT : ( ( ) ( ) Element of K10(K10(T : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K10( the U1 of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K10( the U1 of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ;
attr IT is pre-semi-open means :: DECOMP_1:def 4
IT : ( ( ) ( ) Element of K10(K10(T : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) c= Cl (Int (Cl IT : ( ( ) ( ) Element of K10(K10(T : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K10( the U1 of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K10( the U1 of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K10( the U1 of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ;
attr IT is semi-pre-open means :: DECOMP_1:def 5
IT : ( ( ) ( ) Element of K10(K10(T : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) c= (Cl (Int IT : ( ( ) ( ) Element of K10(K10(T : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K10( the U1 of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K10( the U1 of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) \/ (Int (Cl IT : ( ( ) ( ) Element of K10(K10(T : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K10( the U1 of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K10( the U1 of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K10( the U1 of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ;
end;

definition
let T be ( ( ) ( ) TopStruct ) ;
let B be ( ( ) ( ) Subset of ) ;
func sInt B -> ( ( ) ( ) Subset of ) equals :: DECOMP_1:def 6
B : ( ( ) ( ) Element of K10(K10(T : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) /\ (Cl (Int B : ( ( ) ( ) Element of K10(K10(T : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K10( the U1 of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K10( the U1 of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K10( the U1 of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ;
func pInt B -> ( ( ) ( ) Subset of ) equals :: DECOMP_1:def 7
B : ( ( ) ( ) Element of K10(K10(T : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) /\ (Int (Cl B : ( ( ) ( ) Element of K10(K10(T : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K10( the U1 of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K10( the U1 of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K10( the U1 of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ;
func alphaInt B -> ( ( ) ( ) Subset of ) equals :: DECOMP_1:def 8
B : ( ( ) ( ) Element of K10(K10(T : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) /\ (Int (Cl (Int B : ( ( ) ( ) Element of K10(K10(T : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K10( the U1 of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K10( the U1 of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K10( the U1 of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K10( the U1 of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ;
func psInt B -> ( ( ) ( ) Subset of ) equals :: DECOMP_1:def 9
B : ( ( ) ( ) Element of K10(K10(T : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) /\ (Cl (Int (Cl B : ( ( ) ( ) Element of K10(K10(T : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K10( the U1 of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K10( the U1 of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K10( the U1 of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K10( the U1 of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ;
end;

definition
let T be ( ( ) ( ) TopStruct ) ;
let B be ( ( ) ( ) Subset of ) ;
func spInt B -> ( ( ) ( ) Subset of ) equals :: DECOMP_1:def 10
(sInt B : ( ( ) ( ) Element of K10(K10(T : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ) \/ (pInt B : ( ( ) ( ) Element of K10(K10(T : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K10( the U1 of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ;
end;

definition
let T be ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ;
func T ^alpha -> ( ( ) ( ) Subset-Family of ) equals :: DECOMP_1:def 11
 { B : ( ( ) ( ) Subset of ) where B is ( ( ) ( ) Subset of ) : B : ( ( ) ( ) Subset of ) is ( ( ) ( ) alpha-set of T : ( ( ) ( ) TopStruct ) ) } ;
func SO T -> ( ( ) ( ) Subset-Family of ) equals :: DECOMP_1:def 12
 { B : ( ( ) ( ) Subset of ) where B is ( ( ) ( ) Subset of ) : B : ( ( ) ( ) Subset of ) is semi-open } ;
func PO T -> ( ( ) ( ) Subset-Family of ) equals :: DECOMP_1:def 13
 { B : ( ( ) ( ) Subset of ) where B is ( ( ) ( ) Subset of ) : B : ( ( ) ( ) Subset of ) is pre-open } ;
func SPO T -> ( ( ) ( ) Subset-Family of ) equals :: DECOMP_1:def 14
 { B : ( ( ) ( ) Subset of ) where B is ( ( ) ( ) Subset of ) : B : ( ( ) ( ) Subset of ) is semi-pre-open } ;
func PSO T -> ( ( ) ( ) Subset-Family of ) equals :: DECOMP_1:def 15
 { B : ( ( ) ( ) Subset of ) where B is ( ( ) ( ) Subset of ) : B : ( ( ) ( ) Subset of ) is pre-semi-open } ;
func D(c,alpha) T -> ( ( ) ( ) Subset-Family of ) equals :: DECOMP_1:def 16
 { B : ( ( ) ( ) Subset of ) where B is ( ( ) ( ) Subset of ) : Int B : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K10( the U1 of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) = alphaInt B : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) } ;
func D(c,p) T -> ( ( ) ( ) Subset-Family of ) equals :: DECOMP_1:def 17
 { B : ( ( ) ( ) Subset of ) where B is ( ( ) ( ) Subset of ) : Int B : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K10( the U1 of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) = pInt B : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) } ;
func D(c,s) T -> ( ( ) ( ) Subset-Family of ) equals :: DECOMP_1:def 18
 { B : ( ( ) ( ) Subset of ) where B is ( ( ) ( ) Subset of ) : Int B : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K10( the U1 of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) = sInt B : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) } ;
func D(c,ps) T -> ( ( ) ( ) Subset-Family of ) equals :: DECOMP_1:def 19
 { B : ( ( ) ( ) Subset of ) where B is ( ( ) ( ) Subset of ) : Int B : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K10( the U1 of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) = psInt B : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) } ;
func D(alpha,p) T -> ( ( ) ( ) Subset-Family of ) equals :: DECOMP_1:def 20
 { B : ( ( ) ( ) Subset of ) where B is ( ( ) ( ) Subset of ) : alphaInt B : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) = pInt B : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) } ;
func D(alpha,s) T -> ( ( ) ( ) Subset-Family of ) equals :: DECOMP_1:def 21
 { B : ( ( ) ( ) Subset of ) where B is ( ( ) ( ) Subset of ) : alphaInt B : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) = sInt B : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) } ;
func D(alpha,ps) T -> ( ( ) ( ) Subset-Family of ) equals :: DECOMP_1:def 22
 { B : ( ( ) ( ) Subset of ) where B is ( ( ) ( ) Subset of ) : alphaInt B : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) = psInt B : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) } ;
func D(p,sp) T -> ( ( ) ( ) Subset-Family of ) equals :: DECOMP_1:def 23
 { B : ( ( ) ( ) Subset of ) where B is ( ( ) ( ) Subset of ) : pInt B : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) = spInt B : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) } ;
func D(p,ps) T -> ( ( ) ( ) Subset-Family of ) equals :: DECOMP_1:def 24
 { B : ( ( ) ( ) Subset of ) where B is ( ( ) ( ) Subset of ) : pInt B : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) = psInt B : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) } ;
func D(sp,ps) T -> ( ( ) ( ) Subset-Family of ) equals :: DECOMP_1:def 25
 { B : ( ( ) ( ) Subset of ) where B is ( ( ) ( ) Subset of ) : spInt B : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) = psInt B : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) } ;
end;

theorem :: DECOMP_1:1
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for B being ( ( ) ( ) Subset of ) holds
( alphaInt B : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) = pInt B : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) iff sInt B : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) = psInt B : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) ) ;

theorem :: DECOMP_1:2
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for B being ( ( ) ( ) Subset of ) holds
( B : ( ( ) ( ) Subset of ) is ( ( ) ( ) alpha-set of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) iff B : ( ( ) ( ) Subset of ) = alphaInt B : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) ) ;

theorem :: DECOMP_1:3
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for B being ( ( ) ( ) Subset of ) holds
( B : ( ( ) ( ) Subset of ) is semi-open iff B : ( ( ) ( ) Subset of ) = sInt B : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) ) ;

theorem :: DECOMP_1:4
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for B being ( ( ) ( ) Subset of ) holds
( B : ( ( ) ( ) Subset of ) is pre-open iff B : ( ( ) ( ) Subset of ) = pInt B : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) ) ;

theorem :: DECOMP_1:5
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for B being ( ( ) ( ) Subset of ) holds
( B : ( ( ) ( ) Subset of ) is pre-semi-open iff B : ( ( ) ( ) Subset of ) = psInt B : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) ) ;

theorem :: DECOMP_1:6
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for B being ( ( ) ( ) Subset of ) holds
( B : ( ( ) ( ) Subset of ) is semi-pre-open iff B : ( ( ) ( ) Subset of ) = spInt B : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) ) ;

theorem :: DECOMP_1:7
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) holds (T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ^alpha) : ( ( ) ( ) Subset-Family of ) /\ (D(c,alpha) T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Element of K10(K10( the U1 of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = the topology of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Element of K10(K10( the U1 of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: DECOMP_1:8
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) holds (SO T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( ) Subset-Family of ) /\ (D(c,s) T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Element of K10(K10( the U1 of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = the topology of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Element of K10(K10( the U1 of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: DECOMP_1:9
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) holds (PO T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( ) Subset-Family of ) /\ (D(c,p) T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Element of K10(K10( the U1 of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = the topology of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Element of K10(K10( the U1 of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: DECOMP_1:10
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) holds (PSO T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( ) Subset-Family of ) /\ (D(c,ps) T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Element of K10(K10( the U1 of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = the topology of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Element of K10(K10( the U1 of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: DECOMP_1:11
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) holds (PO T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( ) Subset-Family of ) /\ (D(alpha,p) T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Element of K10(K10( the U1 of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ^alpha : ( ( ) ( ) Subset-Family of ) ;

theorem :: DECOMP_1:12
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) holds (SO T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( ) Subset-Family of ) /\ (D(alpha,s) T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Element of K10(K10( the U1 of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ^alpha : ( ( ) ( ) Subset-Family of ) ;

theorem :: DECOMP_1:13
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) holds (PSO T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( ) Subset-Family of ) /\ (D(alpha,ps) T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Element of K10(K10( the U1 of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ^alpha : ( ( ) ( ) Subset-Family of ) ;

theorem :: DECOMP_1:14
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) holds (SPO T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( ) Subset-Family of ) /\ (D(p,sp) T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Element of K10(K10( the U1 of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = PO T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) Subset-Family of ) ;

theorem :: DECOMP_1:15
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) holds (PSO T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( ) Subset-Family of ) /\ (D(p,ps) T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Element of K10(K10( the U1 of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = PO T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) Subset-Family of ) ;

theorem :: DECOMP_1:16
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) holds (PSO T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( ) Subset-Family of ) /\ (D(alpha,p) T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Element of K10(K10( the U1 of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = SO T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) Subset-Family of ) ;

theorem :: DECOMP_1:17
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) holds (PSO T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( ) Subset-Family of ) /\ (D(sp,ps) T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Element of K10(K10( the U1 of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = SPO T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) Subset-Family of ) ;

definition
let X, Y be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
let f be ( ( V9() V18( the U1 of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of Y : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ( V9() V18( the U1 of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of Y : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) ;
attr f is s-continuous means :: DECOMP_1:def 26
 for G being ( ( ) ( ) Subset of ) st G : ( ( ) ( ) Subset of ) is open holds
f : ( ( ) ( ) Element of K10(K11(X : ( ( ) ( ) TopStruct ) ,Y : ( ( ) ( ) Element of K10(K10(X : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) " G : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K10( the U1 of X : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) in SO X : ( ( ) ( ) TopStruct ) : ( ( ) ( ) Subset-Family of ) ;
attr f is p-continuous means :: DECOMP_1:def 27
 for G being ( ( ) ( ) Subset of ) st G : ( ( ) ( ) Subset of ) is open holds
f : ( ( ) ( ) Element of K10(K11(X : ( ( ) ( ) TopStruct ) ,Y : ( ( ) ( ) Element of K10(K10(X : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) " G : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K10( the U1 of X : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) in PO X : ( ( ) ( ) TopStruct ) : ( ( ) ( ) Subset-Family of ) ;
attr f is alpha-continuous means :: DECOMP_1:def 28
 for G being ( ( ) ( ) Subset of ) st G : ( ( ) ( ) Subset of ) is open holds
f : ( ( ) ( ) Element of K10(K11(X : ( ( ) ( ) TopStruct ) ,Y : ( ( ) ( ) Element of K10(K10(X : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) " G : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K10( the U1 of X : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) in X : ( ( ) ( ) TopStruct ) ^alpha : ( ( ) ( ) Subset-Family of ) ;
attr f is ps-continuous means :: DECOMP_1:def 29
 for G being ( ( ) ( ) Subset of ) st G : ( ( ) ( ) Subset of ) is open holds
f : ( ( ) ( ) Element of K10(K11(X : ( ( ) ( ) TopStruct ) ,Y : ( ( ) ( ) Element of K10(K10(X : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) " G : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K10( the U1 of X : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) in PSO X : ( ( ) ( ) TopStruct ) : ( ( ) ( ) Subset-Family of ) ;
attr f is sp-continuous means :: DECOMP_1:def 30
 for G being ( ( ) ( ) Subset of ) st G : ( ( ) ( ) Subset of ) is open holds
f : ( ( ) ( ) Element of K10(K11(X : ( ( ) ( ) TopStruct ) ,Y : ( ( ) ( ) Element of K10(K10(X : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) " G : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K10( the U1 of X : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) in SPO X : ( ( ) ( ) TopStruct ) : ( ( ) ( ) Subset-Family of ) ;
attr f is (c,alpha)-continuous means :: DECOMP_1:def 31
 for G being ( ( ) ( ) Subset of ) st G : ( ( ) ( ) Subset of ) is open holds
f : ( ( ) ( ) Element of K10(K11(X : ( ( ) ( ) TopStruct ) ,Y : ( ( ) ( ) Element of K10(K10(X : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) " G : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K10( the U1 of X : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) in D(c,alpha) X : ( ( ) ( ) TopStruct ) : ( ( ) ( ) Subset-Family of ) ;
attr f is (c,s)-continuous means :: DECOMP_1:def 32
 for G being ( ( ) ( ) Subset of ) st G : ( ( ) ( ) Subset of ) is open holds
f : ( ( ) ( ) Element of K10(K11(X : ( ( ) ( ) TopStruct ) ,Y : ( ( ) ( ) Element of K10(K10(X : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) " G : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K10( the U1 of X : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) in D(c,s) X : ( ( ) ( ) TopStruct ) : ( ( ) ( ) Subset-Family of ) ;
attr f is (c,p)-continuous means :: DECOMP_1:def 33
 for G being ( ( ) ( ) Subset of ) st G : ( ( ) ( ) Subset of ) is open holds
f : ( ( ) ( ) Element of K10(K11(X : ( ( ) ( ) TopStruct ) ,Y : ( ( ) ( ) Element of K10(K10(X : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) " G : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K10( the U1 of X : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) in D(c,p) X : ( ( ) ( ) TopStruct ) : ( ( ) ( ) Subset-Family of ) ;
attr f is (c,ps)-continuous means :: DECOMP_1:def 34
 for G being ( ( ) ( ) Subset of ) st G : ( ( ) ( ) Subset of ) is open holds
f : ( ( ) ( ) Element of K10(K11(X : ( ( ) ( ) TopStruct ) ,Y : ( ( ) ( ) Element of K10(K10(X : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) " G : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K10( the U1 of X : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) in D(c,ps) X : ( ( ) ( ) TopStruct ) : ( ( ) ( ) Subset-Family of ) ;
attr f is (alpha,p)-continuous means :: DECOMP_1:def 35
 for G being ( ( ) ( ) Subset of ) st G : ( ( ) ( ) Subset of ) is open holds
f : ( ( ) ( ) Element of K10(K11(X : ( ( ) ( ) TopStruct ) ,Y : ( ( ) ( ) Element of K10(K10(X : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) " G : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K10( the U1 of X : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) in D(alpha,p) X : ( ( ) ( ) TopStruct ) : ( ( ) ( ) Subset-Family of ) ;
attr f is (alpha,s)-continuous means :: DECOMP_1:def 36
 for G being ( ( ) ( ) Subset of ) st G : ( ( ) ( ) Subset of ) is open holds
f : ( ( ) ( ) Element of K10(K11(X : ( ( ) ( ) TopStruct ) ,Y : ( ( ) ( ) Element of K10(K10(X : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) " G : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K10( the U1 of X : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) in D(alpha,s) X : ( ( ) ( ) TopStruct ) : ( ( ) ( ) Subset-Family of ) ;
attr f is (alpha,ps)-continuous means :: DECOMP_1:def 37
 for G being ( ( ) ( ) Subset of ) st G : ( ( ) ( ) Subset of ) is open holds
f : ( ( ) ( ) Element of K10(K11(X : ( ( ) ( ) TopStruct ) ,Y : ( ( ) ( ) Element of K10(K10(X : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) " G : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K10( the U1 of X : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) in D(alpha,ps) X : ( ( ) ( ) TopStruct ) : ( ( ) ( ) Subset-Family of ) ;
attr f is (p,ps)-continuous means :: DECOMP_1:def 38
 for G being ( ( ) ( ) Subset of ) st G : ( ( ) ( ) Subset of ) is open holds
f : ( ( ) ( ) Element of K10(K11(X : ( ( ) ( ) TopStruct ) ,Y : ( ( ) ( ) Element of K10(K10(X : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) " G : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K10( the U1 of X : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) in D(p,ps) X : ( ( ) ( ) TopStruct ) : ( ( ) ( ) Subset-Family of ) ;
attr f is (p,sp)-continuous means :: DECOMP_1:def 39
 for G being ( ( ) ( ) Subset of ) st G : ( ( ) ( ) Subset of ) is open holds
f : ( ( ) ( ) Element of K10(K11(X : ( ( ) ( ) TopStruct ) ,Y : ( ( ) ( ) Element of K10(K10(X : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) " G : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K10( the U1 of X : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) in D(p,sp) X : ( ( ) ( ) TopStruct ) : ( ( ) ( ) Subset-Family of ) ;
attr f is (sp,ps)-continuous means :: DECOMP_1:def 40
 for G being ( ( ) ( ) Subset of ) st G : ( ( ) ( ) Subset of ) is open holds
f : ( ( ) ( ) Element of K10(K11(X : ( ( ) ( ) TopStruct ) ,Y : ( ( ) ( ) Element of K10(K10(X : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) " G : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K10( the U1 of X : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) in D(sp,ps) X : ( ( ) ( ) TopStruct ) : ( ( ) ( ) Subset-Family of ) ;
end;

theorem :: DECOMP_1:18
for X, Y being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f being ( ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) holds
( f : ( ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) is alpha-continuous iff ( f : ( ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) is p-continuous & f : ( ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) is (alpha,p)-continuous ) ) ;

theorem :: DECOMP_1:19
for X, Y being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f being ( ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) holds
( f : ( ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) is alpha-continuous iff ( f : ( ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) is s-continuous & f : ( ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) is (alpha,s)-continuous ) ) ;

theorem :: DECOMP_1:20
for X, Y being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f being ( ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) holds
( f : ( ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) is alpha-continuous iff ( f : ( ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) is ps-continuous & f : ( ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) is (alpha,ps)-continuous ) ) ;

theorem :: DECOMP_1:21
for X, Y being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f being ( ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) holds
( f : ( ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) is p-continuous iff ( f : ( ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) is sp-continuous & f : ( ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) is (p,sp)-continuous ) ) ;

theorem :: DECOMP_1:22
for X, Y being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f being ( ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) holds
( f : ( ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) is p-continuous iff ( f : ( ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) is ps-continuous & f : ( ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) is (p,ps)-continuous ) ) ;

theorem :: DECOMP_1:23
for X, Y being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f being ( ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) holds
( f : ( ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) is s-continuous iff ( f : ( ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) is ps-continuous & f : ( ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) is (alpha,p)-continuous ) ) ;

theorem :: DECOMP_1:24
for X, Y being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f being ( ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) holds
( f : ( ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) is sp-continuous iff ( f : ( ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) is ps-continuous & f : ( ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) is (sp,ps)-continuous ) ) ;

theorem :: DECOMP_1:25
for X, Y being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f being ( ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) holds
( f : ( ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) is continuous iff ( f : ( ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) is alpha-continuous & f : ( ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) is (c,alpha)-continuous ) ) ;

theorem :: DECOMP_1:26
for X, Y being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f being ( ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) holds
( f : ( ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) is continuous iff ( f : ( ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) is s-continuous & f : ( ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) is (c,s)-continuous ) ) ;

theorem :: DECOMP_1:27
for X, Y being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f being ( ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) holds
( f : ( ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) is continuous iff ( f : ( ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) is p-continuous & f : ( ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) is (c,p)-continuous ) ) ;

theorem :: DECOMP_1:28
for X, Y being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f being ( ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) holds
( f : ( ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) is continuous iff ( f : ( ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) is ps-continuous & f : ( ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ( V9() V18( the U1 of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) is (c,ps)-continuous ) ) ;