let L1, L2, T1, T2 be non empty reflexive antisymmetric RelStr ; :: thesis: for f being Function of L1,T1
for g being Function of L2,T2 st f is directed-sups-preserving & g is directed-sups-preserving holds
[:f,g:] is directed-sups-preserving
let f be Function of L1,T1; :: thesis: for g being Function of L2,T2 st f is directed-sups-preserving & g is directed-sups-preserving holds
[:f,g:] is directed-sups-preserving
let g be Function of L2,T2; :: thesis: ( f is directed-sups-preserving & g is directed-sups-preserving implies [:f,g:] is directed-sups-preserving )
assume that
A1: f is directed-sups-preserving and
A2: g is directed-sups-preserving ; :: thesis: [:f,g:] is directed-sups-preserving
let X be Subset of [:L1,L2:]; :: according to WAYBEL_0:def 37 :: thesis: ( X is empty or not X is directed or [:f,g:] preserves_sup_of X )
assume A3: ( not X is empty & X is directed ) ; :: thesis: [:f,g:] preserves_sup_of X
then ( not proj1 X is empty & proj1 X is directed ) by YELLOW_3:21, YELLOW_3:22;
then A4: f preserves_sup_of proj1 X by A1;
( not proj2 X is empty & proj2 X is directed ) by A3, YELLOW_3:21, YELLOW_3:22;
then A5: g preserves_sup_of proj2 X by A2;
set iX = [:f,g:] .: X;
A6: ( dom f = the carrier of L1 & dom g = the carrier of L2 ) by FUNCT_2:def 1;
assume A7: ex_sup_of X,[:L1,L2:] ; :: according to WAYBEL_0:def 31 :: thesis: ( ex_sup_of [:f,g:] .: X,[:T1,T2:] & "\/" (([:f,g:] .: X),[:T1,T2:]) = [:f,g:] . ("\/" (X,[:L1,L2:])) )
then A8: ex_sup_of proj1 X,L1 by YELLOW_3:41;
X c= the carrier of [:L1,L2:] ;
then A9: X c= [: the carrier of L1, the carrier of L2:] by YELLOW_3:def 2;
then A10: proj2 ([:f,g:] .: X) = g .: (proj2 X) by A6, Th4;
A11: ex_sup_of proj2 X,L2 by A7, YELLOW_3:41;
then A12: ex_sup_of proj2 ([:f,g:] .: X),T2 by A5, A10;
A13: proj1 ([:f,g:] .: X) = f .: (proj1 X) by A6, A9, Th4;
then ex_sup_of proj1 ([:f,g:] .: X),T1 by A4, A8;
hence ex_sup_of [:f,g:] .: X,[:T1,T2:] by A12, YELLOW_3:41; :: thesis: "\/" (([:f,g:] .: X),[:T1,T2:]) = [:f,g:] . ("\/" (X,[:L1,L2:]))
hence sup ([:f,g:] .: X) = [(sup (f .: (proj1 X))),(sup (g .: (proj2 X)))] by A13, A10, Th8
.= [(f . (sup (proj1 X))),(sup (g .: (proj2 X)))] by A4, A8
.= [(f . (sup (proj1 X))),(g . (sup (proj2 X)))] by A5, A11
.= [:f,g:] . ((sup (proj1 X)),(sup (proj2 X))) by A6, FUNCT_3:def 8
.= [:f,g:] . (sup X) by A7, Th8 ;
:: thesis: verum