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 Th7;
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 Th16;
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 Th7;
hence
oContMaps (X,f) is directed-sups-preserving Function of (oContMaps (X,Z)),(oContMaps (X,Y))
by Th13; 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 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))) . xlet x be
object ;
( 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))
;
(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:18
.=
(oContMaps (X,f)) . a
by Def2
.=
((oContMaps (X,f)) | the carrier of (oContMaps (X,Y))) . x
by A6, FUNCT_1:49
;
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; 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; verum