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