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 that
A1: TopStruct(# the carrier of S1,the topology of S1 #) = TopStruct(# the carrier of S2,the topology of S2 #) and
A2: 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
A3: oContMaps S2,T2 = ContMaps S2,(Omega T2) by WAYBEL26:def 1;
Omega T1 = Omega T2 by A2, WAYBEL25:13;
then reconsider oCM2 = oContMaps S2,T2 as full SubRelStr of (Omega T1) |^ the carrier of S1 by A3, A1, WAYBEL24:def 3;
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;
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 )
A4: TopStruct(# the carrier of (Omega T2),the topology of (Omega T2) #) = TopStruct(# the carrier of T2,the topology of T2 #) by WAYBEL25:def 2;
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
A5: x = f and
A6: f is continuous by WAYBEL24:def 3;
A7: 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 S2,(Omega T2) by A4, A1, A2;
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 )
reconsider P = P1 as Subset of (Omega T1) by A2, A7, A4;
assume P1 is closed ; :: thesis: f1 " P1 is closed
then P is closed by A2, A7, A4, 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 S2,(Omega T2)) by A5, 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 )
A8: TopStruct(# the carrier of (Omega T1),the topology of (Omega T1) #) = TopStruct(# the carrier of T1,the topology of T1 #) by WAYBEL25:def 2;
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
A9: x = f and
A10: f is continuous by WAYBEL24:def 3;
A11: 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 S1,(Omega T1) by A8, A1, A2;
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 )
reconsider P = P1 as Subset of (Omega T2) by A2, A11, A8;
assume P1 is closed ; :: thesis: f1 " P1 is closed
then P is closed by A2, A11, A8, TOPS_3:79;
then f " P is closed by A10, 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 A9, 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