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
let f be continuous Function of Y,Z; :: thesis:
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 )
reconsider sA = sup A as continuous Function of Z,X by Th2;
set fX = oContMaps (f,X);
reconsider sfA = sup ((oContMaps (f,X)) .: A), XfsA = (oContMaps (f,X)) . (sup A) as Function of Y,() by Th1;
reconsider YX = oContMaps (Y,X) as non empty full directed-sups-inheriting SubRelStr of () |^ the carrier of Y by ;
assume ( not A is empty & A is directed ) ; :: thesis:
then reconsider A9 = A as non empty directed Subset of (oContMaps (Z,X)) ;
reconsider fA9 = (oContMaps (f,X)) .: A9 as non empty directed Subset of (oContMaps (Y,X)) by ;
reconsider ZX = oContMaps (Z,X) as non empty full directed-sups-inheriting SubRelStr of () |^ the carrier of Z by ;
reconsider B = A9 as non empty directed Subset of ZX ;
reconsider B9 = B as non empty directed Subset of (() |^ the carrier of Z) by YELLOW_2:7;
reconsider fB = fA9 as non empty directed Subset of YX ;
reconsider fB9 = fB as non empty directed Subset of (() |^ the carrier of Y) by YELLOW_2: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)))) )
set I1 = the carrier of Z;
set I2 = the carrier of Y;
set J1 = the carrier of Z --> ();
set J2 = the carrier of Y --> ();
ex_sup_of fB9,() |^ the carrier of Y by WAYBEL_0:75;
then A1: sup fB9 = sup ((oContMaps (f,X)) .: A) by WAYBEL_0:7;
( oContMaps (Y,X) is up-complete & fA9 is directed ) by Th7;
hence ex_sup_of (oContMaps (f,X)) .: A, oContMaps (Y,X) by WAYBEL_0:75; :: thesis: "\/" (((oContMaps (f,X)) .: A),(oContMaps (Y,X))) = (oContMaps (f,X)) . ("\/" (A,(oContMaps (Z,X))))
A2: (Omega X) |^ the carrier of Y = the carrier of Y -POS_prod ( the carrier of Y --> ()) by YELLOW_1:def 5;
then reconsider fB99 = fB9 as non empty directed Subset of ( the carrier of Y -POS_prod ( the carrier of Y --> ())) ;
now :: thesis: for x being Element of Y holds ex_sup_of pi (fB99,x),( the carrier of Y --> ()) . x
let x be Element of Y; :: thesis: ex_sup_of pi (fB99,x),( the carrier of Y --> ()) . x
( ( the carrier of Y --> ()) . x = Omega X & pi (fB99,x) is directed ) by ;
hence ex_sup_of pi (fB99,x),( the carrier of Y --> ()) . x by WAYBEL_0:75; :: thesis: verum
end;
then A3: ex_sup_of fB99, the carrier of Y -POS_prod ( the carrier of Y --> ()) by YELLOW16:31;
A4: (Omega X) |^ the carrier of Z = the carrier of Z -POS_prod ( the carrier of Z --> ()) by YELLOW_1:def 5;
then reconsider B99 = B9 as non empty directed Subset of ( the carrier of Z -POS_prod ( the carrier of Z --> ())) ;
A5: ex_sup_of B9,() |^ the carrier of Z by WAYBEL_0:75;
then A6: sup B9 = sup A by WAYBEL_0:7;
now :: thesis: for x being Element of Y holds sfA . x = XfsA . x
let x be Element of Y; :: thesis: sfA . x = XfsA . x
A7: ( ( the carrier of Z --> ()) . (f . x) = Omega X & ( the carrier of Y --> ()) . x = Omega X ) by FUNCOP_1:7;
A8: pi (fB99,x) = pi (B99,(f . x)) by Th14;
thus sfA . x = sup (pi (fB99,x)) by
.= (sup B99) . (f . x) by
.= (sA * f) . x by
.= 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:63; :: thesis: verum