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_inf_of X, product J iff for i being Element of I holds ex_inf_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_inf_of X, product J iff for i being Element of I holds ex_inf_of pi (X,i),J . i )
let X be Subset of (product J); :: thesis: ( ex_inf_of X, product J iff for i being Element of I holds ex_inf_of pi (X,i),J . i )

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

set f = inf X;
assume A1: ex_inf_of X, product J ; :: thesis: for i being Element of I holds ex_inf_of pi (X,i),J . i
let i be Element of I; :: thesis: ex_inf_of pi (X,i),J . i
A2: inf X is_<=_than X by A1, YELLOW_0:31;

A3: now :: thesis: for x being Element of (J . i) st pi (X,i) is_>=_than x holds
(inf X) . i >= x

let x be Element of (J . i); :: thesis: ( pi (X,i) is_>=_than x implies (inf X) . i >= x )
set g = (inf X) +* (i,x);
A4: dom ((inf X) +* (i,x)) = dom (inf X) by FUNCT_7:30;
dom (inf X) = I by WAYBEL_3:27;
then A5: ((inf X) +* (i,x)) . i = x by FUNCT_7:31;

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

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

end;

then reconsider g = (inf X) +* (i,x) as Element of (product J) by A4, WAYBEL_3:27;
assume A6: pi (X,i) is_>=_than x ; :: thesis: (inf X) . i >= x
X is_>=_than g

proof

let h be Element of (product J); :: according to LATTICE3:def 8 :: thesis: ( not h in X or g <= h )
assume A7: h in X ; :: thesis: g <= h
then A8: h . i in pi (X,i) by CARD_3:def 6;
A9: h >= inf X by A2, 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 = (inf X) . j or ( g . j = x & j = i ) ) by A5, FUNCT_7:32;
hence h . j >= g . j by A6, A9, A8, WAYBEL_3:28; :: thesis: verum

end;

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

end;

then inf X >= g by A1, YELLOW_0:31;
hence (inf X) . i >= x by A5, WAYBEL_3:28; :: thesis: verum

end;

(inf X) . i is_<=_than pi (X,i) by A2, Th29;
hence ex_inf_of pi (X,i),J . i by A3, YELLOW_0:31; :: thesis: verum

end;

assume for i being Element of I holds ex_inf_of pi (X,i),J . i ; :: thesis: ex_inf_of X, product J
then ex f being Element of (product J) st
( ( for i being Element of I holds f . i = inf (pi (X,i)) ) & f is_<=_than X & ( for g being Element of (product J) st X is_>=_than g holds
f >= g ) ) by Lm2;
hence ex_inf_of X, product J by YELLOW_0:31; :: thesis: verum