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)
then RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) ;
then T1 |^ the carrier of S1 = T2 |^ the carrier of S2 by A1, WAYBEL27:15;
then reconsider C2 = ContMaps (S2,T2) as full SubRelStr of T1 |^ the carrier of S1 by WAYBEL24:def 3;
reconsider C1 = ContMaps (S1,T1) as full SubRelStr of T1 |^ the carrier of S1 by WAYBEL24:def 3;
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
A3: x = f and
A4: 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 6 :: 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 3;
then ([#] T2) \ P2 in the topology of T2 by PRE_TOPC:def 2;
then ([#] T1) \ P1 is open by A2, PRE_TOPC:def 2;
then P1 is closed by PRE_TOPC:def 3;
then f " P1 is closed by A4, PRE_TOPC:def 6;
then ([#] S1) \ (f " P1) is open by PRE_TOPC:def 3;
then ([#] S1) \ (f2 " P2) in the topology of S2 by A1, PRE_TOPC:def 2;
then ([#] S2) \ (f2 " P2) is open by A1, PRE_TOPC:def 2;
hence f2 " P2 is closed by PRE_TOPC:def 3; :: thesis: verum

end;

hence x in the carrier of (ContMaps (S2,T2)) by A3, 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 and
A6: 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 6 :: 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 3;
then ([#] T1) \ P2 in the topology of T2 by A2, PRE_TOPC:def 2;
then ([#] T2) \ P2 is open by A2, PRE_TOPC:def 2;
then P2 is closed by PRE_TOPC:def 3;
then f " P2 is closed by A6, PRE_TOPC:def 6;
then ([#] S2) \ (f " P2) is open by PRE_TOPC:def 3;
then ([#] S2) \ (f1 " P1) in the topology of S1 by A1, PRE_TOPC:def 2;
then ([#] S1) \ (f1 " P1) is open by A1, PRE_TOPC:def 2;
hence f1 " P1 is closed by PRE_TOPC:def 3; :: thesis: verum

end;

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

end;

then RelStr(# the carrier of C1, the InternalRel of C1 #) = RelStr(# the carrier of C2, the InternalRel of C2 #) by YELLOW_0:57;
hence ContMaps (S1,T1) = ContMaps (S2,T2) ; :: thesis: verum