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

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:32;
dom (sup X) = I by 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 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, 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, A9, A8, 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;

sup X is_>=_than X by A1, YELLOW_0:30;
then (sup X) . i is_>=_than pi X,i by Th31;
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