let I be non empty set ; :: thesis: for J being non-Empty Poset-yielding ManySortedSet of
for X being Subset of (product J) holds
( ex_sup_of X, product J iff for i being Element of I holds ex_sup_of pi X,i,J . i )
let J be non-Empty Poset-yielding ManySortedSet of ; :: thesis: for X being Subset of (product J) holds
( ex_sup_of X, product J iff for i being Element of I holds ex_sup_of pi X,i,J . i )
let X be Subset of (product J); :: thesis: ( ex_sup_of X, product J iff for i being Element of I holds ex_sup_of pi X,i,J . i )

hereby :: thesis: ( ( for i being Element of I holds ex_sup_of pi X,i,J . i ) implies ex_sup_of X, product J )

assume A1: ex_sup_of X, product J ; :: thesis: for i being Element of I holds ex_sup_of pi X,i,J . i
let i be Element of I; :: thesis: ex_sup_of pi X,i,J . i
set f = sup X;
sup X is_>=_than X by A1, YELLOW_0:30;
then A2: (sup X) . i is_>=_than pi X,i by Th31;

now

let x be Element of (J . i); :: thesis: ( pi X,i is_<=_than x implies (sup X) . i <= x )
assume A3: pi X,i is_<=_than x ; :: thesis: (sup X) . i <= x
set g = (sup X) +* i,x;
A4: ( dom ((sup X) +* i,x) = dom (sup X) & dom (sup X) = I ) by FUNCT_7:32, WAYBEL_3:27;
then A5: ((sup X) +* i,x) . i = x by FUNCT_7:33;

now

let j be Element of I; :: thesis: ((sup X) +* i,x) . j is Element of (J . j)
( ((sup X) +* i,x) . j = (sup X) . j or ( ((sup X) +* i,x) . j = x & j = i ) ) by A5, FUNCT_7:34;
hence ((sup X) +* i,x) . j is Element of (J . j) ; :: thesis: verum

end;

then reconsider g = (sup X) +* i,x as Element of (product J) by A4, WAYBEL_3:27;
A6: X is_<=_than sup X by A1, YELLOW_0:30;
X is_<=_than g

proof

let h be Element of (product J); :: according to LATTICE3:def 9 :: thesis: ( not h in X or h <= g )
assume h in X ; :: thesis: h <= g
then A7: ( h <= sup X & h . i in pi X,i ) by A6, CARD_3:def 6, LATTICE3:def 9;

now

let j be Element of I; :: thesis: h . j <= g . j
( g . j = (sup X) . j or ( g . j = x & j = i ) ) by A5, FUNCT_7:34;
hence h . j <= g . j by A3, A7, LATTICE3:def 9, WAYBEL_3:28; :: thesis: verum

end;

hence h <= g by WAYBEL_3:28; :: thesis: verum

end;

then sup X <= g by A1, YELLOW_0:30;
hence (sup X) . i <= x by A5, WAYBEL_3:28; :: thesis: verum

end;

hence ex_sup_of pi X,i,J . i by A2, YELLOW_0:30; :: thesis: verum

end;

assume for i being Element of I holds ex_sup_of pi X,i,J . i ; :: thesis: ex_sup_of X, product J
then consider f being Element of (product J) such that
for i being Element of I holds f . i = sup (pi X,i) and
A8: f is_>=_than X and
A9: for g being Element of (product J) st X is_<=_than g holds
f <= g by Lm1;
thus ex_sup_of X, product J by A8, A9, YELLOW_0:30; :: thesis: verum