let T1, T2 be TopSpace; :: thesis: for S1 being Subset of T1
for S2 being Subset of T2 st S1 is compact & S2 is compact holds
[:S1,S2:] is compact Subset of [:T1,T2:]
let S1 be Subset of T1; :: thesis: for S2 being Subset of T2 st S1 is compact & S2 is compact holds
[:S1,S2:] is compact Subset of [:T1,T2:]
let S2 be Subset of T2; :: thesis: ( S1 is compact & S2 is compact implies [:S1,S2:] is compact Subset of [:T1,T2:] )
assume that
A1: S1 is compact and
A2: S2 is compact ; :: thesis: [:S1,S2:] is compact Subset of [:T1,T2:]

per cases ( ( not S1 is empty & not S2 is empty ) or ( S1 is empty & not S2 is empty ) or ( not S1 is empty & S2 is empty ) or ( S1 is empty & S2 is empty ) ) ;

suppose A3: ( not S1 is empty & not S2 is empty ) ; :: thesis: [:S1,S2:] is compact Subset of [:T1,T2:]

then ( ex x being object st x in S1 & ex y being object st y in S2 ) ;
then reconsider T1 = T1, T2 = T2 as non empty TopSpace ;
reconsider S2 = S2 as non empty compact Subset of T2 by A2, A3;
reconsider S1 = S1 as non empty compact Subset of T1 by A1, A3;
reconsider X = [:S1,S2:] as Subset of [:T1,T2:] ;
TopStruct(# the carrier of [:(T1 | S1),(T2 | S2):], the topology of [:(T1 | S1),(T2 | S2):] #) = TopStruct(# the carrier of ([:T1,T2:] | X), the topology of ([:T1,T2:] | X) #) by Th22;
hence [:S1,S2:] is compact Subset of [:T1,T2:] by COMPTS_1:3; :: thesis: verum

end;

suppose ( S1 is empty & not S2 is empty ) ; :: thesis: [:S1,S2:] is compact Subset of [:T1,T2:]

then reconsider S1 = S1 as empty Subset of T1 ;
[:S1,S2:] = {} [:T1,T2:] ;
hence [:S1,S2:] is compact Subset of [:T1,T2:] ; :: thesis: verum

end;

suppose ( not S1 is empty & S2 is empty ) ; :: thesis: [:S1,S2:] is compact Subset of [:T1,T2:]

then reconsider S2 = S2 as empty Subset of T2 ;
[:S1,S2:] = {} [:T1,T2:] ;
hence [:S1,S2:] is compact Subset of [:T1,T2:] ; :: thesis: verum

end;

suppose ( S1 is empty & S2 is empty ) ; :: thesis: [:S1,S2:] is compact Subset of [:T1,T2:]

then reconsider S2 = S2 as empty Subset of T2 ;
[:S1,S2:] = {} [:T1,T2:] ;
hence [:S1,S2:] is compact Subset of [:T1,T2:] ; :: thesis: verum

end;

end;