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

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

now

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:34;
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, LATTICE3:def 8;

now

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:34;
hence h . j >= g . j by A6, A9, A8, LATTICE3:def 8, 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, Th32;
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