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