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))

hence ContMaps (S1,T1) = ContMaps (S2,T2) ; :: thesis: verum

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

then
RelStr(# the carrier of C1, the InternalRel of C1 #) = RelStr(# the carrier of C2, the InternalRel of C2 #)
by YELLOW_0:57;
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))

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

end;proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (ContMaps (S2,T2)) or x in the carrier of (ContMaps (S1,T1)) )
let x be object ; :: 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

end;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

hence
x in the carrier of (ContMaps (S2,T2))
by A3, WAYBEL24:def 3; :: thesis: verum
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 ;

then ([#] T2) \ P2 in the topology of T2 ;

then ([#] T1) \ P1 is open by A2;

then P1 is closed ;

then f " P1 is closed by A4;

then ([#] S1) \ (f " P1) is open ;

then ([#] S1) \ (f2 " P2) in the topology of S2 by A1;

then ([#] S2) \ (f2 " P2) is open by A1;

hence f2 " P2 is closed ; :: thesis: verum

end;reconsider P1 = P2 as Subset of T1 by A2;

assume P2 is closed ; :: thesis: f2 " P2 is closed

then ([#] T2) \ P2 is open ;

then ([#] T2) \ P2 in the topology of T2 ;

then ([#] T1) \ P1 is open by A2;

then P1 is closed ;

then f " P1 is closed by A4;

then ([#] S1) \ (f " P1) is open ;

then ([#] S1) \ (f2 " P2) in the topology of S2 by A1;

then ([#] S2) \ (f2 " P2) is open by A1;

hence f2 " P2 is closed ; :: thesis: verum

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

hence
x in the carrier of (ContMaps (S1,T1))
by A5, WAYBEL24:def 3; :: thesis: verum
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 ;

then ([#] T1) \ P2 in the topology of T2 by A2;

then ([#] T2) \ P2 is open by A2;

then P2 is closed ;

then f " P2 is closed by A6;

then ([#] S2) \ (f " P2) is open ;

then ([#] S2) \ (f1 " P1) in the topology of S1 by A1;

then ([#] S1) \ (f1 " P1) is open by A1;

hence f1 " P1 is closed ; :: thesis: verum

end;reconsider P2 = P1 as Subset of T2 by A2;

assume P1 is closed ; :: thesis: f1 " P1 is closed

then ([#] T1) \ P1 is open ;

then ([#] T1) \ P2 in the topology of T2 by A2;

then ([#] T2) \ P2 is open by A2;

then P2 is closed ;

then f " P2 is closed by A6;

then ([#] S2) \ (f " P2) is open ;

then ([#] S2) \ (f1 " P1) in the topology of S1 by A1;

then ([#] S1) \ (f1 " P1) is open by A1;

hence f1 " P1 is closed ; :: thesis: verum

hence ContMaps (S1,T1) = ContMaps (S2,T2) ; :: thesis: verum