let Y, Z be non empty TopSpace; :: thesis: for X being monotone-convergence T_0-TopSpace
for f being continuous Function of Y,Z holds oContMaps f,X is directed-sups-preserving
let X be monotone-convergence T_0-TopSpace; :: thesis: for f being continuous Function of Y,Z holds oContMaps f,X is directed-sups-preserving
A1: oContMaps Y,X is up-complete by Th8;
let f be continuous Function of Y,Z; :: thesis: oContMaps f,X is directed-sups-preserving
let A be Subset of (oContMaps Z,X); :: according to WAYBEL_0:def 37 :: thesis: ( A is empty or not A is directed or oContMaps f,X preserves_sup_of A )
assume ( not A is empty & A is directed ) ; :: thesis: oContMaps f,X preserves_sup_of A
then reconsider A' = A as non empty directed Subset of (oContMaps Z,X) ;
reconsider ZX = oContMaps Z,X as non empty full directed-sups-inheriting SubRelStr of (Omega X) |^ the carrier of Z by WAYBEL24:def 3, WAYBEL25:43;
reconsider B = A' as non empty directed Subset of ZX ;
reconsider B' = B as non empty directed Subset of ((Omega X) |^ the carrier of Z) by YELLOW_2:7;
A2: ex_sup_of B',(Omega X) |^ the carrier of Z by WAYBEL_0:75;
then A3: sup B' = sup A by WAYBEL_0:7;
set fX = oContMaps f,X;
reconsider fA' = (oContMaps f,X) .: A' as non empty directed Subset of (oContMaps Y,X) by Th11, YELLOW_2:17;
reconsider YX = oContMaps Y,X as non empty full directed-sups-inheriting SubRelStr of (Omega X) |^ the carrier of Y by WAYBEL24:def 3, WAYBEL25:43;
reconsider fB = fA' as non empty directed Subset of YX ;
reconsider fB' = fB as non empty directed Subset of ((Omega X) |^ the carrier of Y) by YELLOW_2:7;
ex_sup_of fB',(Omega X) |^ the carrier of Y by WAYBEL_0:75;
then A4: sup fB' = sup ((oContMaps f,X) .: A) by WAYBEL_0:7;
assume ex_sup_of A, oContMaps Z,X ; :: according to WAYBEL_0:def 31 :: thesis: ( ex_sup_of (oContMaps f,X) .: A, oContMaps Y,X & "\/" ((oContMaps f,X) .: A),(oContMaps Y,X) = (oContMaps f,X) . ("\/" A,(oContMaps Z,X)) )
fA' is directed ;
hence ex_sup_of (oContMaps f,X) .: A, oContMaps Y,X by A1, WAYBEL_0:75; :: thesis: "\/" ((oContMaps f,X) .: A),(oContMaps Y,X) = (oContMaps f,X) . ("\/" A,(oContMaps Z,X))
reconsider sfA = sup ((oContMaps f,X) .: A), XfsA = (oContMaps f,X) . (sup A) as Function of Y,(Omega X) by Th1;
set I1 = the carrier of Z;
set I2 = the carrier of Y;
set J1 = the carrier of Z --> (Omega X);
set J2 = the carrier of Y --> (Omega X);
A5: (Omega X) |^ the carrier of Y = the carrier of Y -POS_prod (the carrier of Y --> (Omega X)) by YELLOW_1:def 5;
then reconsider fB'' = fB' as non empty directed Subset of (the carrier of Y -POS_prod (the carrier of Y --> (Omega X))) ;
A6: (Omega X) |^ the carrier of Z = the carrier of Z -POS_prod (the carrier of Z --> (Omega X)) by YELLOW_1:def 5;
then reconsider B'' = B' as non empty directed Subset of (the carrier of Z -POS_prod (the carrier of Z --> (Omega X))) ;
reconsider sA = sup A as continuous Function of Z,X by Th2;

now

let x be Element of Y; :: thesis: ex_sup_of pi fB'',x,(the carrier of Y --> (Omega X)) . x
( (the carrier of Y --> (Omega X)) . x = Omega X & pi fB'',x is directed ) by FUNCOP_1:13, YELLOW16:37;
hence ex_sup_of pi fB'',x,(the carrier of Y --> (Omega X)) . x by WAYBEL_0:75; :: thesis: verum

end;

then A7: ex_sup_of fB'',the carrier of Y -POS_prod (the carrier of Y --> (Omega X)) by YELLOW16:33;

now

let x be Element of Y; :: thesis: sfA . x = XfsA . x
A8: ( (the carrier of Z --> (Omega X)) . (f . x) = Omega X & (the carrier of Y --> (Omega X)) . x = Omega X ) by FUNCOP_1:13;
A9: pi fB'',x = pi B'',(f . x) by Th15;
thus sfA . x = sup (pi fB'',x) by A4, A5, A7, YELLOW16:35
.= (sup B'') . (f . x) by A2, A6, A8, A9, YELLOW16:35
.= (sA * f) . x by A3, A6, FUNCT_2:21
.= XfsA . x by Def3 ; :: thesis: verum

end;

hence "\/" ((oContMaps f,X) .: A),(oContMaps Y,X) = (oContMaps f,X) . ("\/" A,(oContMaps Z,X)) by FUNCT_2:113; :: thesis: verum