let I be non empty set ; :: thesis: for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of st ( for i being Element of I holds J . i is complete LATTICE ) holds
for X being Subset of (product J)
for i being Element of I holds (inf X) . i = inf (pi X,i)
let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of ; :: thesis: ( ( for i being Element of I holds J . i is complete LATTICE ) implies for X being Subset of (product J)
for i being Element of I holds (inf X) . i = inf (pi X,i) )
assume A1: for i being Element of I holds J . i is complete LATTICE ; :: thesis: for X being Subset of (product J)
for i being Element of I holds (inf X) . i = inf (pi X,i)
then reconsider L = product J as complete LATTICE by WAYBEL_3:31;
A2: L is complete ;
let X be Subset of (product J); :: thesis: for i being Element of I holds (inf X) . i = inf (pi X,i)
let i be Element of I; :: thesis: (inf X) . i = inf (pi X,i)
A3: inf X is_<=_than X by A2, YELLOW_0:33;
A4: (inf X) . i is_<=_than pi X,i

proof

let a be Element of (J . i); :: according to LATTICE3:def 8 :: thesis: ( not a in pi X,i or (inf X) . i <= a )
assume a in pi X,i ; :: thesis: (inf X) . i <= a
then consider f being Function such that
A5: ( f in X & a = f . i ) by CARD_3:def 6;
reconsider f = f as Element of (product J) by A5;
inf X <= f by A3, A5, LATTICE3:def 8;
hence (inf X) . i <= a by A5, WAYBEL_3:28; :: thesis: verum

end;

A6: J . i is complete LATTICE by A1;

now

let a be Element of (J . i); :: thesis: ( a is_<=_than pi X,i implies (inf X) . i >= a )
assume A7: a is_<=_than pi X,i ; :: thesis: (inf X) . i >= a
set f = (inf X) +* i,a;
A8: ( dom ((inf X) +* i,a) = dom (inf X) & dom (inf X) = I ) by FUNCT_7:32, WAYBEL_3:27;

now

let j be Element of I; :: thesis: ((inf X) +* i,a) . j is Element of (J . j)
( j = i or j <> i ) ;
then ( ((inf X) +* i,a) . j = (inf X) . j or ( ((inf X) +* i,a) . j = a & j = i ) ) by A8, FUNCT_7:33, FUNCT_7:34;
hence ((inf X) +* i,a) . j is Element of (J . j) ; :: thesis: verum

end;

then reconsider f = (inf X) +* i,a as Element of (product J) by A8, WAYBEL_3:27;
f is_<=_than X

proof

let g be Element of (product J); :: according to LATTICE3:def 8 :: thesis: ( not g in X or f <= g )
assume g in X ; :: thesis: f <= g
then A9: ( g >= inf X & g . i in pi X,i ) by A2, CARD_3:def 6, YELLOW_2:24;

now

let j be Element of I; :: thesis: f . j <= g . j
( j = i or j <> i ) ;
then ( f . j = (inf X) . j or ( f . j = a & j = i ) ) by A8, FUNCT_7:33, FUNCT_7:34;
hence f . j <= g . j by A7, A9, LATTICE3:def 8, WAYBEL_3:28; :: thesis: verum

end;

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

end;

then ( f <= inf X & f . i = a ) by A2, A8, FUNCT_7:33, YELLOW_0:33;
hence (inf X) . i >= a by WAYBEL_3:28; :: thesis: verum

end;

hence (inf X) . i = inf (pi X,i) by A4, A6, YELLOW_0:33; :: thesis: verum