let X be non empty TopSpace; :: thesis:
let Y, Z be monotone-convergence T_0-TopSpace; :: thesis:
A1: oContMaps X,Z is up-complete by Th8;
let f be continuous Function of Y,Z; :: thesis:
( TopStruct(# the carrier of Y,the topology of Y #) = TopStruct(# the carrier of (Omega Y),the topology of (Omega Y) #) & TopStruct(# the carrier of Z,the topology of Z #) = TopStruct(# the carrier of (Omega Z),the topology of (Omega Z) #) ) by WAYBEL25:def 2;
then reconsider f' = f as continuous Function of (Omega Y),(Omega Z) by YELLOW12:36;
let A be Subset of (oContMaps X,Y); :: according to WAYBEL_0:def 37 :: thesis:
assume ( not A is empty & A is directed ) ; :: thesis:
then reconsider A' = A as non empty directed Subset of (oContMaps X,Y) ;
reconsider XY = oContMaps X,Y as non empty full directed-sups-inheriting SubRelStr of (Omega Y) |^ the carrier of X by WAYBEL24:def 3, WAYBEL25:43;
reconsider B = A' as non empty directed Subset of XY ;
reconsider B' = B as non empty directed Subset of ((Omega Y) |^ the carrier of X) by YELLOW_2:7;
A2: ex_sup_of B',(Omega Y) |^ the carrier of X by WAYBEL_0:75;
then A3: sup B' = sup A by WAYBEL_0:7;
set Xf = oContMaps X,f;
reconsider fA' = (oContMaps X,f) .: A' as non empty directed Subset of (oContMaps X,Z) by Th9, YELLOW_2:17;
reconsider XZ = oContMaps X,Z as non empty full directed-sups-inheriting SubRelStr of (Omega Z) |^ the carrier of X by WAYBEL24:def 3, WAYBEL25:43;
reconsider fB = fA' as non empty directed Subset of XZ ;
reconsider fB' = fB as non empty directed Subset of ((Omega Z) |^ the carrier of X) by YELLOW_2:7;
ex_sup_of fB',(Omega Z) |^ the carrier of X by WAYBEL_0:75;
then A4: sup fB' = sup ((oContMaps X,f) .: A) by WAYBEL_0:7;
assume ex_sup_of A, oContMaps X,Y ; :: according to WAYBEL_0:def 31 :: thesis:
fA' is directed ;
hence ex_sup_of (oContMaps X,f) .: A, oContMaps X,Z by A1, WAYBEL_0:75; :: thesis:
reconsider sfA = sup ((oContMaps X,f) .: A), XfsA = (oContMaps X,f) . (sup A) as Function of X,(Omega Z) by Th1;
set I = the carrier of X;
set J1 = the carrier of X --> (Omega Y);
set J2 = the carrier of X --> (Omega Z);
A5: (Omega Z) |^ the carrier of X = the carrier of X -POS_prod (the carrier of X --> (Omega Z)) by YELLOW_1:def 5;
then reconsider fB'' = fB' as non empty directed Subset of (the carrier of X -POS_prod (the carrier of X --> (Omega Z))) ;
A6: (Omega Y) |^ the carrier of X = the carrier of X -POS_prod (the carrier of X --> (Omega Y)) by YELLOW_1:def 5;
then reconsider B'' = B' as non empty directed Subset of (the carrier of X -POS_prod (the carrier of X --> (Omega Y))) ;
reconsider sA = sup A as continuous Function of X,Y by Th2;

now

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

end;

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

now

let x be Element of X; :: thesis:
A8: (sup B'') . x = sup (pi B'',x) by A2, A6, YELLOW16:35;
A9: ( (the carrier of X --> (Omega Y)) . x = Omega Y & (the carrier of X --> (Omega Z)) . x = Omega Z ) by FUNCOP_1:13;
then reconsider Bx = pi B'',x as non empty directed Subset of (Omega Y) by YELLOW16:37;
A10: ( ex_sup_of Bx, Omega Y & f' preserves_sup_of Bx ) by WAYBEL_0:75, WAYBEL_0:def 37;
A11: pi fB'',x = f' .: Bx by Th13;
thus sfA . x = sup (pi fB'',x) by A4, A5, A7, YELLOW16:35
.= f . (sup Bx) by A9, A10, A11, WAYBEL_0:def 31
.= (f * sA) . x by A3, A6, A8, A9, FUNCT_2:21
.= XfsA . x by Def2 ; :: thesis:

end;

hence sup ((oContMaps X,f) .: A) = (oContMaps X,f) . (sup A) by FUNCT_2:113; :: thesis: