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 Th7;
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) )
set F = oContMaps (X,f);
reconsider sXY = oContMaps (X,Y) as non empty full SubRelStr of uXZ by Th16;
assume A1: f is being_a_retraction ; :: thesis: 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 Th7;
hence oContMaps (X,f) is directed-sups-preserving Function of (oContMaps (X,Z)),(oContMaps (X,Y)) by Th13; :: 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: the carrier of sXY c= the carrier of uXZ by YELLOW_0:def 13;

A3: now :: thesis: for x being object st x in the carrier of (oContMaps (X,Y)) holds
(id (oContMaps (X,Y))) . x = ((oContMaps (X,f)) | the carrier of (oContMaps (X,Y))) . x

let x be object ; :: 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 )
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:44, YELLOW16:45;
assume A6: x in the carrier of (oContMaps (X,Y)) ; :: thesis: (id (oContMaps (X,Y))) . x = ((oContMaps (X,f)) | the carrier of (oContMaps (X,Y))) . x
then 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:18
.= (oContMaps (X,f)) . a by Def2
.= ((oContMaps (X,f)) | the carrier of (oContMaps (X,Y))) . x by A6, FUNCT_1:49 ;
:: thesis: 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:32;
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;
hence (oContMaps (X,f)) | the carrier of (oContMaps (X,Y)) = id (oContMaps (X,Y)) by A3, FUNCT_1:2; :: thesis: oContMaps (X,Y) is SubRelStr of oContMaps (X,Z)
Omega Y is full directed-sups-inheriting SubRelStr of Omega Z by A1, Th17, 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:39, YELLOW16:42;
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:26, YELLOW16:27;
hence oContMaps (X,Y) is SubRelStr of oContMaps (X,Z) by Th16, YELLOW16:28; :: thesis: verum