let S1, S2 be TopStruct ; :: thesis: ( TopStruct(# the carrier of S1,the topology of S1 #) = TopStruct(# the carrier of S2,the topology of S2 #) implies for T1, T2 being non empty TopRelStr st TopRelStr(# the carrier of T1,the InternalRel of T1,the topology of T1 #) = TopRelStr(# the carrier of T2,the InternalRel of T2,the topology of T2 #) holds
ContMaps S1,T1 = ContMaps S2,T2 )
assume A1: TopStruct(# the carrier of S1,the topology of S1 #) = TopStruct(# the carrier of S2,the topology of S2 #) ; :: thesis: for T1, T2 being non empty TopRelStr st TopRelStr(# the carrier of T1,the InternalRel of T1,the topology of T1 #) = TopRelStr(# the carrier of T2,the InternalRel of T2,the topology of T2 #) holds
ContMaps S1,T1 = ContMaps S2,T2
let T1, T2 be non empty TopRelStr ; :: thesis: ( TopRelStr(# the carrier of T1,the InternalRel of T1,the topology of T1 #) = TopRelStr(# the carrier of T2,the InternalRel of T2,the topology of T2 #) implies ContMaps S1,T1 = ContMaps S2,T2 )
assume A2: TopRelStr(# the carrier of T1,the InternalRel of T1,the topology of T1 #) = TopRelStr(# the carrier of T2,the InternalRel of T2,the topology of T2 #) ; :: thesis: ContMaps S1,T1 = ContMaps S2,T2
A3: the carrier of (ContMaps S1,T1) = the carrier of (ContMaps S2,T2)

proof

thus the carrier of (ContMaps S1,T1) c= the carrier of (ContMaps S2,T2) :: according to XBOOLE_0:def 10 :: thesis: the carrier of (ContMaps S2,T2) c= the carrier of (ContMaps S1,T1)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (ContMaps S1,T1) or x in the carrier of (ContMaps S2,T2) )
assume x in the carrier of (ContMaps S1,T1) ; :: thesis: x in the carrier of (ContMaps S2,T2)
then consider f being Function of S1,T1 such that
A4: ( x = f & f is continuous ) by WAYBEL24:def 3;
reconsider f2 = f as Function of S2,T2 by A1, A2;
f2 is continuous

proof

let P2 be Subset of T2; :: according to PRE_TOPC:def 12 :: thesis: ( not P2 is closed or f2 " P2 is closed )
reconsider P1 = P2 as Subset of T1 by A2;
assume P2 is closed ; :: thesis: f2 " P2 is closed
then ([#] T2) \ P2 is open by PRE_TOPC:def 6;
then ([#] T2) \ P2 in the topology of T2 by PRE_TOPC:def 5;
then ([#] T1) \ P1 is open by A2, PRE_TOPC:def 5;
then P1 is closed by PRE_TOPC:def 6;
then f " P1 is closed by A4, PRE_TOPC:def 12;
then ([#] S1) \ (f " P1) is open by PRE_TOPC:def 6;
then ([#] S1) \ (f2 " P2) in the topology of S2 by A1, PRE_TOPC:def 5;
then ([#] S2) \ (f2 " P2) is open by A1, PRE_TOPC:def 5;
hence f2 " P2 is closed by PRE_TOPC:def 6; :: thesis: verum

end;

hence x in the carrier of (ContMaps S2,T2) by A4, WAYBEL24:def 3; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (ContMaps S2,T2) or x in the carrier of (ContMaps S1,T1) )
assume x in the carrier of (ContMaps S2,T2) ; :: thesis: x in the carrier of (ContMaps S1,T1)
then consider f being Function of S2,T2 such that
A5: ( x = f & f is continuous ) by WAYBEL24:def 3;
reconsider f1 = f as Function of S1,T1 by A1, A2;
f1 is continuous

proof

let P1 be Subset of T1; :: according to PRE_TOPC:def 12 :: thesis: ( not P1 is closed or f1 " P1 is closed )
reconsider P2 = P1 as Subset of T2 by A2;
assume P1 is closed ; :: thesis: f1 " P1 is closed
then ([#] T1) \ P1 is open by PRE_TOPC:def 6;
then ([#] T1) \ P2 in the topology of T2 by A2, PRE_TOPC:def 5;
then ([#] T2) \ P2 is open by A2, PRE_TOPC:def 5;
then P2 is closed by PRE_TOPC:def 6;
then f " P2 is closed by A5, PRE_TOPC:def 12;
then ([#] S2) \ (f " P2) is open by PRE_TOPC:def 6;
then ([#] S2) \ (f1 " P1) in the topology of S1 by A1, PRE_TOPC:def 5;
then ([#] S1) \ (f1 " P1) is open by A1, PRE_TOPC:def 5;
hence f1 " P1 is closed by PRE_TOPC:def 6; :: thesis: verum

end;

hence x in the carrier of (ContMaps S1,T1) by A5, WAYBEL24:def 3; :: thesis: verum

end;

reconsider C1 = ContMaps S1,T1 as full SubRelStr of T1 |^ the carrier of S1 by WAYBEL24:def 3;
( RelStr(# the carrier of T1,the InternalRel of T1 #) = RelStr(# the carrier of T2,the InternalRel of T2 #) & the carrier of S1 = the carrier of S2 ) by A1, A2;
then T1 |^ the carrier of S1 = T2 |^ the carrier of S2 by WAYBEL27:15;
then reconsider C2 = ContMaps S2,T2 as full SubRelStr of T1 |^ the carrier of S1 by WAYBEL24:def 3;
RelStr(# the carrier of C1,the InternalRel of C1 #) = RelStr(# the carrier of C2,the InternalRel of C2 #) by A3, YELLOW_0:58;
hence ContMaps S1,T1 = ContMaps S2,T2 ; :: thesis: verum