let X be non empty TopSpace; :: thesis: for Y, Z being monotone-convergence T_0-TopSpace

for f being continuous Function of Y,Z holds oContMaps (X,f) is directed-sups-preserving

let Y, Z be monotone-convergence T_0-TopSpace; :: thesis: for f being continuous Function of Y,Z holds oContMaps (X,f) is directed-sups-preserving

let f be continuous Function of Y,Z; :: thesis: oContMaps (X,f) is directed-sups-preserving

let A be Subset of (oContMaps (X,Y)); :: according to WAYBEL_0:def 37 :: thesis: ( A is empty or not A is directed or oContMaps (X,f) preserves_sup_of A )

reconsider sA = sup A as continuous Function of X,Y by Th2;

set Xf = oContMaps (X,f);

reconsider sfA = sup ((oContMaps (X,f)) .: A), XfsA = (oContMaps (X,f)) . (sup A) as Function of X,(Omega Z) by Th1;

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;

assume ( not A is empty & A is directed ) ; :: thesis: oContMaps (X,f) preserves_sup_of A

then reconsider A9 = A as non empty directed Subset of (oContMaps (X,Y)) ;

reconsider fA9 = (oContMaps (X,f)) .: A9 as non empty directed Subset of (oContMaps (X,Z)) by Th8, YELLOW_2:15;

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 = A9 as non empty directed Subset of XY ;

reconsider B9 = B as non empty directed Subset of ((Omega Y) |^ the carrier of X) by YELLOW_2:7;

reconsider fB = fA9 as non empty directed Subset of XZ ;

reconsider fB9 = fB as non empty directed Subset of ((Omega Z) |^ the carrier of X) by YELLOW_2:7;

assume ex_sup_of A, oContMaps (X,Y) ; :: according to WAYBEL_0:def 31 :: thesis: ( ex_sup_of (oContMaps (X,f)) .: A, oContMaps (X,Z) & "\/" (((oContMaps (X,f)) .: A),(oContMaps (X,Z))) = (oContMaps (X,f)) . ("\/" (A,(oContMaps (X,Y)))) )

set I = the carrier of X;

set J1 = the carrier of X --> (Omega Y);

set J2 = the carrier of X --> (Omega Z);

( 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 f9 = f as continuous Function of (Omega Y),(Omega Z) by YELLOW12:36;

ex_sup_of fB9,(Omega Z) |^ the carrier of X by WAYBEL_0:75;

then A1: sup fB9 = sup ((oContMaps (X,f)) .: A) by WAYBEL_0:7;

( oContMaps (X,Z) is up-complete & fA9 is directed ) by Th7;

hence ex_sup_of (oContMaps (X,f)) .: A, oContMaps (X,Z) by WAYBEL_0:75; :: thesis: "\/" (((oContMaps (X,f)) .: A),(oContMaps (X,Z))) = (oContMaps (X,f)) . ("\/" (A,(oContMaps (X,Y))))

A2: (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 fB99 = fB9 as non empty directed Subset of ( the carrier of X -POS_prod ( the carrier of X --> (Omega Z))) ;

A4: (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 B99 = B9 as non empty directed Subset of ( the carrier of X -POS_prod ( the carrier of X --> (Omega Y))) ;

A5: ex_sup_of B9,(Omega Y) |^ the carrier of X by WAYBEL_0:75;

then A6: sup B9 = sup A by WAYBEL_0:7;

for f being continuous Function of Y,Z holds oContMaps (X,f) is directed-sups-preserving

let Y, Z be monotone-convergence T_0-TopSpace; :: thesis: for f being continuous Function of Y,Z holds oContMaps (X,f) is directed-sups-preserving

let f be continuous Function of Y,Z; :: thesis: oContMaps (X,f) is directed-sups-preserving

let A be Subset of (oContMaps (X,Y)); :: according to WAYBEL_0:def 37 :: thesis: ( A is empty or not A is directed or oContMaps (X,f) preserves_sup_of A )

reconsider sA = sup A as continuous Function of X,Y by Th2;

set Xf = oContMaps (X,f);

reconsider sfA = sup ((oContMaps (X,f)) .: A), XfsA = (oContMaps (X,f)) . (sup A) as Function of X,(Omega Z) by Th1;

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;

assume ( not A is empty & A is directed ) ; :: thesis: oContMaps (X,f) preserves_sup_of A

then reconsider A9 = A as non empty directed Subset of (oContMaps (X,Y)) ;

reconsider fA9 = (oContMaps (X,f)) .: A9 as non empty directed Subset of (oContMaps (X,Z)) by Th8, YELLOW_2:15;

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 = A9 as non empty directed Subset of XY ;

reconsider B9 = B as non empty directed Subset of ((Omega Y) |^ the carrier of X) by YELLOW_2:7;

reconsider fB = fA9 as non empty directed Subset of XZ ;

reconsider fB9 = fB as non empty directed Subset of ((Omega Z) |^ the carrier of X) by YELLOW_2:7;

assume ex_sup_of A, oContMaps (X,Y) ; :: according to WAYBEL_0:def 31 :: thesis: ( ex_sup_of (oContMaps (X,f)) .: A, oContMaps (X,Z) & "\/" (((oContMaps (X,f)) .: A),(oContMaps (X,Z))) = (oContMaps (X,f)) . ("\/" (A,(oContMaps (X,Y)))) )

set I = the carrier of X;

set J1 = the carrier of X --> (Omega Y);

set J2 = the carrier of X --> (Omega Z);

( 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 f9 = f as continuous Function of (Omega Y),(Omega Z) by YELLOW12:36;

ex_sup_of fB9,(Omega Z) |^ the carrier of X by WAYBEL_0:75;

then A1: sup fB9 = sup ((oContMaps (X,f)) .: A) by WAYBEL_0:7;

( oContMaps (X,Z) is up-complete & fA9 is directed ) by Th7;

hence ex_sup_of (oContMaps (X,f)) .: A, oContMaps (X,Z) by WAYBEL_0:75; :: thesis: "\/" (((oContMaps (X,f)) .: A),(oContMaps (X,Z))) = (oContMaps (X,f)) . ("\/" (A,(oContMaps (X,Y))))

A2: (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 fB99 = fB9 as non empty directed Subset of ( the carrier of X -POS_prod ( the carrier of X --> (Omega Z))) ;

now :: thesis: for x being Element of X holds ex_sup_of pi (fB99,x),( the carrier of X --> (Omega Z)) . x

then A3:
ex_sup_of fB99, the carrier of X -POS_prod ( the carrier of X --> (Omega Z))
by YELLOW16:31;let x be Element of X; :: thesis: ex_sup_of pi (fB99,x),( the carrier of X --> (Omega Z)) . x

( ( the carrier of X --> (Omega Z)) . x = Omega Z & pi (fB99,x) is directed ) by FUNCOP_1:7, YELLOW16:35;

hence ex_sup_of pi (fB99,x),( the carrier of X --> (Omega Z)) . x by WAYBEL_0:75; :: thesis: verum

end;( ( the carrier of X --> (Omega Z)) . x = Omega Z & pi (fB99,x) is directed ) by FUNCOP_1:7, YELLOW16:35;

hence ex_sup_of pi (fB99,x),( the carrier of X --> (Omega Z)) . x by WAYBEL_0:75; :: thesis: verum

A4: (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 B99 = B9 as non empty directed Subset of ( the carrier of X -POS_prod ( the carrier of X --> (Omega Y))) ;

A5: ex_sup_of B9,(Omega Y) |^ the carrier of X by WAYBEL_0:75;

then A6: sup B9 = sup A by WAYBEL_0:7;

now :: thesis: for x being Element of X holds sfA . x = XfsA . x

hence
"\/" (((oContMaps (X,f)) .: A),(oContMaps (X,Z))) = (oContMaps (X,f)) . ("\/" (A,(oContMaps (X,Y))))
by FUNCT_2:63; :: thesis: verumlet x be Element of X; :: thesis: sfA . x = XfsA . x

A7: ( the carrier of X --> (Omega Y)) . x = Omega Y by FUNCOP_1:7;

then reconsider Bx = pi (B99,x) as non empty directed Subset of (Omega Y) by YELLOW16:35;

A8: ( ( the carrier of X --> (Omega Z)) . x = Omega Z & ex_sup_of Bx, Omega Y ) by FUNCOP_1:7, WAYBEL_0:75;

A9: (sup B99) . x = sup (pi (B99,x)) by A5, A4, YELLOW16:33;

A10: ( f9 preserves_sup_of Bx & pi (fB99,x) = f9 .: Bx ) by Th12, WAYBEL_0:def 37;

thus sfA . x = sup (pi (fB99,x)) by A1, A2, A3, YELLOW16:33

.= f . (sup Bx) by A8, A10

.= (f * sA) . x by A6, A4, A9, A7, FUNCT_2:15

.= XfsA . x by Def2 ; :: thesis: verum

end;A7: ( the carrier of X --> (Omega Y)) . x = Omega Y by FUNCOP_1:7;

then reconsider Bx = pi (B99,x) as non empty directed Subset of (Omega Y) by YELLOW16:35;

A8: ( ( the carrier of X --> (Omega Z)) . x = Omega Z & ex_sup_of Bx, Omega Y ) by FUNCOP_1:7, WAYBEL_0:75;

A9: (sup B99) . x = sup (pi (B99,x)) by A5, A4, YELLOW16:33;

A10: ( f9 preserves_sup_of Bx & pi (fB99,x) = f9 .: Bx ) by Th12, WAYBEL_0:def 37;

thus sfA . x = sup (pi (fB99,x)) by A1, A2, A3, YELLOW16:33

.= f . (sup Bx) by A8, A10

.= (f * sA) . x by A6, A4, A9, A7, FUNCT_2:15

.= XfsA . x by Def2 ; :: thesis: verum