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 4;
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
object ;
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;
then
x is
continuous Function of
X,
Z
by FUNCT_2:2, PRE_TOPC:26;
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
object ;
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))
reconsider x =
x,
y =
y as
Element of
(oContMaps (X,Y)) by A4, ZFMISC_1:87;
reconsider a =
x,
b =
y as
Element of
(oContMaps (X,Z)) by A3;
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 5;
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 5;
verum
end;
then reconsider XY = oContMaps (X,Y) as non empty SubRelStr of oContMaps (X,Z) ;
A5:
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 A5, 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
object ;
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 A6:
[x,y] in the
InternalRel of
(oContMaps (X,Z)) |_2 the
carrier of
XY
;
[x,y] in the InternalRel of XY
then A7:
[x,y] in [: the carrier of XY, the carrier of XY:]
by A5, XBOOLE_0:def 4;
reconsider x =
x,
y =
y as
Element of
XY by A7, ZFMISC_1:87;
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)) ;
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 A5, A6, XBOOLE_0:def 4;
then
a <= b
by ORDERS_2:def 5;
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 5;
verum
end;
hence
oContMaps (X,Y) is full SubRelStr of oContMaps (X,Z)
by YELLOW_0:def 14; verum