let I be non empty set ; :: thesis: for J being non-Empty Poset-yielding ManySortedSet of I
for X being Subset of (product J) st ex_sup_of X, product J holds
for i being Element of I holds (sup X) . i = sup (pi X,i)
let J be non-Empty Poset-yielding ManySortedSet of I; :: thesis: for X being Subset of (product J) st ex_sup_of X, product J holds
for i being Element of I holds (sup X) . i = sup (pi X,i)
let X be Subset of (product J); :: thesis: ( ex_sup_of X, product J implies for i being Element of I holds (sup X) . i = sup (pi X,i) )
assume ex_sup_of X, product J ; :: thesis: for i being Element of I holds (sup X) . i = sup (pi X,i)
then for i being Element of I holds ex_sup_of pi X,i,J . i by Th33;
then consider f being Element of (product J) such that
A1: for i being Element of I holds f . i = sup (pi X,i) and
A2: f is_>=_than X and
A3: for g being Element of (product J) st X is_<=_than g holds
f <= g by Lm1;
sup X = f by A2, A3, YELLOW_0:30;
hence for i being Element of I holds (sup X) . i = sup (pi X,i) by A1; :: thesis: verum