let I be non empty set ; :: thesis: for J being non-Empty Poset-yielding ManySortedSet of I
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 I; :: 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 )

set f = sup X;
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

A2: now :: thesis: for x being Element of (J . i) st pi (X,i) is_<=_than x holds
(sup X) . i <= x

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) by FUNCT_7:30;
dom (sup X) = I by WAYBEL_3:27;
then A5: ((sup X) +* (i,x)) . i = x by FUNCT_7:31;

now :: thesis: for j being Element of I holds ((sup X) +* (i,x)) . j is Element of (J . j)

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:32;
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 A7: h in X ; :: thesis: h <= g
then A8: h . i in pi (X,i) by CARD_3:def 6;
A9: h <= sup X by A6, A7;

now :: thesis: for j being Element of I holds h . j <= g . j

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:32;
hence h . j <= g . j by A3, A9, A8, 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;

sup X is_>=_than X by A1, YELLOW_0:30;
then (sup X) . i is_>=_than pi (X,i) by Th28;
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 ex f being Element of (product J) st
( ( for i being Element of I holds f . i = sup (pi (X,i)) ) & f is_>=_than X & ( for g being Element of (product J) st X is_<=_than g holds
f <= g ) ) by Lm1;
hence ex_sup_of X, product J by YELLOW_0:30; :: thesis: verum