let S1, S2 be TopStruct ; ( 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 #)
; 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 ; ( 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 #)
; 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))
XBOOLE_0:def 10 the carrier of (ContMaps (S2,T2)) c= the carrier of (ContMaps (S1,T1))
let x be
object ;
TARSKI:def 3 ( 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))
;
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
hence
x in the
carrier of
(ContMaps (S1,T1))
by A5, WAYBEL24:def 3;
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)
; verum