let X, Z be non empty TopSpace; for Y being non empty SubSpace of Z holds oContMaps (X,Y) is full SubRelStr of oContMaps (X,Z)
let Y be non empty SubSpace of Z; oContMaps (X,Y) is full SubRelStr of oContMaps (X,Z)
set XY = oContMaps (X,Y);
set XZ = oContMaps (X,Z);
A1:
Omega Y is full SubRelStr of Omega Z
by WAYBEL25:17;
A2:
[#] Y c= [#] Z
by PRE_TOPC:def 9;
oContMaps (X,Y) is SubRelStr of oContMaps (X,Z)
proof
thus A3:
the
carrier of
(oContMaps (X,Y)) c= the
carrier of
(oContMaps (X,Z))
YELLOW_0:def 13 the InternalRel of (oContMaps (X,Y)) c= the InternalRel of (oContMaps (X,Z))proof
let x be
set ;
TARSKI:def 3 ( not x in the carrier of (oContMaps (X,Y)) or x in the carrier of (oContMaps (X,Z)) )
assume
x in the
carrier of
(oContMaps (X,Y))
;
x in the carrier of (oContMaps (X,Z))
then reconsider f =
x as
continuous Function of
X,
Y by Th2;
(
dom f = the
carrier of
X &
rng f c= the
carrier of
Z )
by A2, FUNCT_2:def 1, XBOOLE_1:1;
then
x is
continuous Function of
X,
Z
by FUNCT_2:4, PRE_TOPC:56;
then
x is
Element of
(oContMaps (X,Z))
by Th2;
hence
x in the
carrier of
(oContMaps (X,Z))
;
verum
end;
let x,
y be
set ;
RELAT_1:def 3 ( not [x,y] in the InternalRel of (oContMaps (X,Y)) or [x,y] in the InternalRel of (oContMaps (X,Z)) )
assume A4:
[x,y] in the
InternalRel of
(oContMaps (X,Y))
;
[x,y] in the InternalRel of (oContMaps (X,Z))
then A5:
(
x in the
carrier of
(oContMaps (X,Y)) &
y in the
carrier of
(oContMaps (X,Y)) )
by ZFMISC_1:106;
reconsider x =
x,
y =
y as
Element of
(oContMaps (X,Y)) by A4, ZFMISC_1:106;
reconsider a =
x,
b =
y as
Element of
(oContMaps (X,Z)) by A3, A5;
reconsider f =
x,
g =
y as
continuous Function of
X,
(Omega Y) by Th1;
reconsider f9 =
a,
g9 =
b as
continuous Function of
X,
(Omega Z) by Th1;
x <= y
by A4, ORDERS_2:def 9;
then
f <= g
by Th3;
then
f9 <= g9
by A1, YELLOW16:2;
then
a <= b
by Th3;
hence
[x,y] in the
InternalRel of
(oContMaps (X,Z))
by ORDERS_2:def 9;
verum
end;
then reconsider XY = oContMaps (X,Y) as non empty SubRelStr of oContMaps (X,Z) ;
A6:
the InternalRel of (oContMaps (X,Z)) |_2 the carrier of XY = the InternalRel of (oContMaps (X,Z)) /\ [: the carrier of XY, the carrier of XY:]
by WELLORD1:def 6;
the InternalRel of XY = the InternalRel of (oContMaps (X,Z)) |_2 the carrier of XY
proof
the
InternalRel of
XY c= the
InternalRel of
(oContMaps (X,Z))
by YELLOW_0:def 13;
hence
the
InternalRel of
XY c= the
InternalRel of
(oContMaps (X,Z)) |_2 the
carrier of
XY
by A6, XBOOLE_1:19;
XBOOLE_0:def 10 the InternalRel of (oContMaps (X,Z)) |_2 the carrier of XY c= the InternalRel of XY
let x,
y be
set ;
RELAT_1:def 3 ( not [x,y] in the InternalRel of (oContMaps (X,Z)) |_2 the carrier of XY or [x,y] in the InternalRel of XY )
assume A7:
[x,y] in the
InternalRel of
(oContMaps (X,Z)) |_2 the
carrier of
XY
;
[x,y] in the InternalRel of XY
then A8:
[x,y] in [: the carrier of XY, the carrier of XY:]
by A6, XBOOLE_0:def 4;
then A9:
(
x in the
carrier of
XY &
y in the
carrier of
XY )
by ZFMISC_1:106;
reconsider x =
x,
y =
y as
Element of
XY by A8, ZFMISC_1:106;
the
carrier of
XY c= the
carrier of
(oContMaps (X,Z))
by YELLOW_0:def 13;
then reconsider a =
x,
b =
y as
Element of
(oContMaps (X,Z)) by A9;
reconsider f9 =
a,
g9 =
b as
continuous Function of
X,
(Omega Z) by Th1;
reconsider f =
x,
g =
y as
continuous Function of
X,
(Omega Y) by Th1;
[a,b] in the
InternalRel of
(oContMaps (X,Z))
by A6, A7, XBOOLE_0:def 4;
then
a <= b
by ORDERS_2:def 9;
then
f9 <= g9
by Th3;
then
f <= g
by A1, YELLOW16:3;
then
x <= y
by Th3;
hence
[x,y] in the
InternalRel of
XY
by ORDERS_2:def 9;
verum
end;
hence
oContMaps (X,Y) is full SubRelStr of oContMaps (X,Z)
by YELLOW_0:def 14; verum