let X be non empty TopSpace; 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; for f being continuous Function of Y,Z holds oContMaps X,f is directed-sups-preserving
let f be continuous Function of Y,Z; oContMaps X,f is directed-sups-preserving
let A be Subset of (oContMaps X,Y); WAYBEL_0:def 37 ( 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 )
; 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 Th9, YELLOW_2:17;
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
; WAYBEL_0:def 31 ( 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 Th8;
hence
ex_sup_of (oContMaps X,f) .: A, oContMaps X,Z
by WAYBEL_0:75; "\/" ((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))) ;
then A3:
ex_sup_of fB99,the carrier of X -POS_prod (the carrier of X --> (Omega Z))
by YELLOW16:33;
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 let x be
Element of
X;
sfA . x = XfsA . xA7:
(the carrier of X --> (Omega Y)) . x = Omega Y
by FUNCOP_1:13;
then reconsider Bx =
pi B99,
x as non
empty directed Subset of
(Omega Y) by YELLOW16:37;
A8:
(
(the carrier of X --> (Omega Z)) . x = Omega Z &
ex_sup_of Bx,
Omega Y )
by FUNCOP_1:13, WAYBEL_0:75;
A9:
(sup B99) . x = sup (pi B99,x)
by A5, A4, YELLOW16:35;
A10:
(
f9 preserves_sup_of Bx &
pi fB99,
x = f9 .: Bx )
by Th13, WAYBEL_0:def 37;
thus sfA . x =
sup (pi fB99,x)
by A1, A2, A3, YELLOW16:35
.=
f . (sup Bx)
by A8, A10, WAYBEL_0:def 31
.=
(f * sA) . x
by A6, A4, A9, A7, FUNCT_2:21
.=
XfsA . x
by Def2
;
verum end;
hence
"\/" ((oContMaps X,f) .: A),(oContMaps X,Z) = (oContMaps X,f) . ("\/" A,(oContMaps X,Y))
by FUNCT_2:113; verum