let S1, S2, T1, T2 be non empty TopSpace; :: thesis: ( TopStruct(# the carrier of S1,the topology of S1 #) = TopStruct(# the carrier of S2,the topology of S2 #) & TopStruct(# the carrier of T1,the topology of T1 #) = TopStruct(# the carrier of T2,the topology of T2 #) implies oContMaps S1,T1 = oContMaps S2,T2 )
assume A1: ( TopStruct(# the carrier of S1,the topology of S1 #) = TopStruct(# the carrier of S2,the topology of S2 #) & TopStruct(# the carrier of T1,the topology of T1 #) = TopStruct(# the carrier of T2,the topology of T2 #) ) ; :: thesis: oContMaps S1,T1 = oContMaps S2,T2
then A2: Omega T1 = Omega T2 by WAYBEL25:13;
oContMaps S1,T1 = ContMaps S1,(Omega T1) by WAYBEL26:def 1;
then reconsider oCM1 = oContMaps S1,T1 as full SubRelStr of (Omega T1) |^ the carrier of S1 by WAYBEL24:def 3;
oContMaps S2,T2 = ContMaps S2,(Omega T2) by WAYBEL26:def 1;
then reconsider oCM2 = oContMaps S2,T2 as full SubRelStr of (Omega T1) |^ the carrier of S1 by A1, A2, WAYBEL24:def 3;
the carrier of oCM1 = the carrier of oCM2

proof

thus the carrier of oCM1 c= the carrier of oCM2 :: according to XBOOLE_0:def 10 :: thesis: the carrier of oCM2 c= the carrier of oCM1

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of oCM1 or x in the carrier of oCM2 )
assume x in the carrier of oCM1 ; :: thesis: x in the carrier of oCM2
then x in the carrier of (ContMaps S1,(Omega T1)) by WAYBEL26:def 1;
then consider f being Function of S1,(Omega T1) such that
A3: ( x = f & f is continuous ) by WAYBEL24:def 3;
A4: ( TopStruct(# the carrier of (Omega T1),the topology of (Omega T1) #) = TopStruct(# the carrier of T1,the topology of T1 #) & TopStruct(# the carrier of (Omega T2),the topology of (Omega T2) #) = TopStruct(# the carrier of T2,the topology of T2 #) ) by WAYBEL25:def 2;
then reconsider f1 = f as Function of S2,(Omega T2) by A1;
for P1 being Subset of (Omega T2) st P1 is closed holds
f1 " P1 is closed

proof

let P1 be Subset of (Omega T2); :: thesis: ( P1 is closed implies f1 " P1 is closed )
assume A5: P1 is closed ; :: thesis: f1 " P1 is closed
reconsider P = P1 as Subset of (Omega T1) by A1, A4;
P is closed by A1, A4, A5, TOPS_3:79;
then f " P is closed by A3, PRE_TOPC:def 12;
hence f1 " P1 is closed by A1, TOPS_3:79; :: thesis: verum

end;

then f1 is continuous by PRE_TOPC:def 12;
then x in the carrier of (ContMaps S2,(Omega T2)) by A3, WAYBEL24:def 3;
hence x in the carrier of oCM2 by WAYBEL26:def 1; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of oCM2 or x in the carrier of oCM1 )
assume x in the carrier of oCM2 ; :: thesis: x in the carrier of oCM1
then x in the carrier of (ContMaps S2,(Omega T2)) by WAYBEL26:def 1;
then consider f being Function of S2,(Omega T2) such that
A6: ( x = f & f is continuous ) by WAYBEL24:def 3;
A7: ( TopStruct(# the carrier of (Omega T2),the topology of (Omega T2) #) = TopStruct(# the carrier of T2,the topology of T2 #) & TopStruct(# the carrier of (Omega T1),the topology of (Omega T1) #) = TopStruct(# the carrier of T1,the topology of T1 #) ) by WAYBEL25:def 2;
then reconsider f1 = f as Function of S1,(Omega T1) by A1;
for P1 being Subset of (Omega T1) st P1 is closed holds
f1 " P1 is closed

proof

let P1 be Subset of (Omega T1); :: thesis: ( P1 is closed implies f1 " P1 is closed )
assume A8: P1 is closed ; :: thesis: f1 " P1 is closed
reconsider P = P1 as Subset of (Omega T2) by A1, A7;
P is closed by A1, A7, A8, TOPS_3:79;
then f " P is closed by A6, PRE_TOPC:def 12;
hence f1 " P1 is closed by A1, TOPS_3:79; :: thesis: verum

end;

then f1 is continuous by PRE_TOPC:def 12;
then x in the carrier of (ContMaps S1,(Omega T1)) by A6, WAYBEL24:def 3;
hence x in the carrier of oCM1 by WAYBEL26:def 1; :: thesis: verum

end;

hence oContMaps S1,T1 = oContMaps S2,T2 by YELLOW_0:58; :: thesis: verum