let S1, S2, T1, T2 be non empty TopSpace; ( 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 #)
; 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
XBOOLE_0:def 10 the carrier of oCM2 c= the carrier of oCM1proof
let x be
object ;
TARSKI:def 3 ( 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
;
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
then
f1 is
continuous
by PRE_TOPC:def 6;
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;
verum
end;
let x be
object ;
TARSKI:def 3 ( 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
;
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
then
f1 is
continuous
by PRE_TOPC:def 6;
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;
verum
end;
hence
oContMaps (S1,T1) = oContMaps (S2,T2)
by YELLOW_0:57; verum