let Y, Z be non empty TopSpace; 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; for f being continuous Function of Y,Z holds oContMaps (f,X) is directed-sups-preserving
let f be continuous Function of Y,Z; oContMaps (f,X) is directed-sups-preserving
let A be Subset of (oContMaps (Z,X)); WAYBEL_0:def 37 ( 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,(Omega X) by Th1;
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;
assume
( not A is empty & A is directed )
; oContMaps (f,X) preserves_sup_of A
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 Th10, YELLOW_2:15;
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 = A9 as non empty directed Subset of ZX ;
reconsider B9 = B as non empty directed Subset of ((Omega X) |^ 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 ((Omega X) |^ the carrier of Y) by YELLOW_2:7;
assume
ex_sup_of A, oContMaps (Z,X)
; WAYBEL_0:def 31 ( 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 --> (Omega X);
set J2 = the carrier of Y --> (Omega X);
ex_sup_of fB9,(Omega X) |^ 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; "\/" (((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 --> (Omega X))
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 --> (Omega X))) ;
then A3:
ex_sup_of fB99, the carrier of Y -POS_prod ( the carrier of Y --> (Omega X))
by YELLOW16:31;
A4:
(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 B99 = B9 as non empty directed Subset of ( the carrier of Z -POS_prod ( the carrier of Z --> (Omega X))) ;
A5:
ex_sup_of B9,(Omega X) |^ the carrier of Z
by WAYBEL_0:75;
then A6:
sup B9 = sup A
by WAYBEL_0:7;
now for x being Element of Y holds sfA . x = XfsA . xlet x be
Element of
Y;
sfA . x = XfsA . xA7:
(
( the carrier of Z --> (Omega X)) . (f . x) = Omega X &
( the carrier of Y --> (Omega X)) . 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 A1, A2, A3, YELLOW16:33
.=
(sup B99) . (f . x)
by A5, A4, A7, A8, YELLOW16:33
.=
(sA * f) . x
by A6, A4, FUNCT_2:15
.=
XfsA . x
by Def3
;
verum end;
hence
"\/" (((oContMaps (f,X)) .: A),(oContMaps (Y,X))) = (oContMaps (f,X)) . ("\/" (A,(oContMaps (Z,X))))
by FUNCT_2:63; verum