let X be non empty TopSpace; :: thesis: for Z being monotone-convergence T_0-TopSpace
for Y being non empty SubSpace of Z
for f being continuous Function of Z,Y st f is being_a_retraction holds
oContMaps X,f is_a_retraction_of oContMaps X,Z, oContMaps X,Y
let Z be monotone-convergence T_0-TopSpace; :: thesis: for Y being non empty SubSpace of Z
for f being continuous Function of Z,Y st f is being_a_retraction holds
oContMaps X,f is_a_retraction_of oContMaps X,Z, oContMaps X,Y
let Y be non empty SubSpace of Z; :: thesis: for f being continuous Function of Z,Y st f is being_a_retraction holds
oContMaps X,f is_a_retraction_of oContMaps X,Z, oContMaps X,Y
set XY = oContMaps X,Y;
set XZ = oContMaps X,Z;
reconsider uXZ = oContMaps X,Z as non empty up-complete Poset by Th8;
reconsider sXY = oContMaps X,Y as non empty full SubRelStr of uXZ by Th17;
let f be continuous Function of Z,Y; :: thesis: ( f is being_a_retraction implies oContMaps X,f is_a_retraction_of oContMaps X,Z, oContMaps X,Y )
assume A1:
f is being_a_retraction
; :: thesis: oContMaps X,f is_a_retraction_of oContMaps X,Z, oContMaps X,Y
set F = oContMaps X,f;
reconsider Y' = Y as monotone-convergence T_0-TopSpace by A1, Lm1;
oContMaps X,Y' is up-complete
by Th8;
hence
oContMaps X,f is directed-sups-preserving Function of (oContMaps X,Z),(oContMaps X,Y)
by Th14; :: according to YELLOW16:def 1 :: thesis: ( (oContMaps X,f) | the carrier of (oContMaps X,Y) = id (oContMaps X,Y) & oContMaps X,Y is SubRelStr of oContMaps X,Z )
A2:
dom (id (oContMaps X,Y)) = the carrier of (oContMaps X,Y)
by RELAT_1:71;
A3:
the carrier of sXY c= the carrier of uXZ
by YELLOW_0:def 13;
then
(oContMaps X,f) | the carrier of (oContMaps X,Y) is Function of the carrier of (oContMaps X,Y),the carrier of (oContMaps X,Y)
by FUNCT_2:38;
then A4:
dom ((oContMaps X,f) | the carrier of (oContMaps X,Y)) = the carrier of (oContMaps X,Y)
by FUNCT_2:def 1;
now let x be
set ;
:: thesis: ( x in the carrier of (oContMaps X,Y) implies (id (oContMaps X,Y)) . x = ((oContMaps X,f) | the carrier of (oContMaps X,Y)) . x )assume A5:
x in the
carrier of
(oContMaps X,Y)
;
:: thesis: (id (oContMaps X,Y)) . x = ((oContMaps X,f) | the carrier of (oContMaps X,Y)) . xthen reconsider a =
x as
Element of
(oContMaps X,Z) by A3;
reconsider a =
a as
continuous Function of
X,
Z by Th2;
A6:
(
rng f = the
carrier of
Y &
x is
Function of
X,
Y )
by A1, A5, Th2, YELLOW16:46;
then
(
f is
idempotent &
rng a c= the
carrier of
Y &
dom f = the
carrier of
Z )
by A1, FUNCT_2:def 1, RELAT_1:def 19, YELLOW16:47;
then
f * a = a
by A6, YELLOW16:4;
hence (id (oContMaps X,Y)) . x =
f * a
by A5, FUNCT_1:35
.=
(oContMaps X,f) . a
by Def2
.=
((oContMaps X,f) | the carrier of (oContMaps X,Y)) . x
by A5, FUNCT_1:72
;
:: thesis: verum end;
hence
(oContMaps X,f) | the carrier of (oContMaps X,Y) = id (oContMaps X,Y)
by A2, A4, FUNCT_1:9; :: thesis: oContMaps X,Y is SubRelStr of oContMaps X,Z
A7:
oContMaps X,Y' is non empty full directed-sups-inheriting SubRelStr of (Omega Y) |^ the carrier of X
by WAYBEL24:def 3, WAYBEL25:43;
A8:
oContMaps X,Z is non empty full directed-sups-inheriting SubRelStr of (Omega Z) |^ the carrier of X
by WAYBEL24:def 3, WAYBEL25:43;
Omega Y is full directed-sups-inheriting SubRelStr of Omega Z
by A1, Th18, WAYBEL25:17;
then
(Omega Y) |^ the carrier of X is full directed-sups-inheriting SubRelStr of (Omega Z) |^ the carrier of X
by YELLOW16:41, YELLOW16:44;
then
oContMaps X,Y is full directed-sups-inheriting SubRelStr of (Omega Z) |^ the carrier of X
by A7, YELLOW16:28, YELLOW16:29;
hence
oContMaps X,Y is SubRelStr of oContMaps X,Z
by A8, Th17, YELLOW16:30; :: thesis: verum