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 (sup X) . i = sup (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 (sup X) . i = sup (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 (sup X) . i = sup (pi X,i)
then reconsider L = product J as complete LATTICE by Th31;
A2: L is complete ;
let X be Subset of (product J); :: thesis: for i being Element of I holds (sup X) . i = sup (pi X,i)
let i be Element of I; :: thesis: (sup X) . i = sup (pi X,i)
A3: sup X is_>=_than X by A2, YELLOW_0:32;
A4: (sup X) . i is_>=_than pi X,i

proof

let a be Element of (J . i); :: according to LATTICE3:def 9 :: thesis: ( not a in pi X,i or a <= (sup X) . i )
assume a in pi X,i ; :: thesis: a <= (sup X) . i
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;
sup X >= f by A3, A5, LATTICE3:def 9;
hence a <= (sup X) . i by A5, Th28; :: 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 (sup X) . i <= a )
assume A7: a is_>=_than pi X,i ; :: thesis: (sup X) . i <= a
set f = (sup X) +* i,a;
A8: ( dom ((sup X) +* i,a) = dom (sup X) & dom (sup X) = I ) by Th27, FUNCT_7:32;

now

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

end;

then reconsider f = (sup X) +* i,a as Element of (product J) by A8, Th27;
f is_>=_than X

proof

let g be Element of (product J); :: according to LATTICE3:def 9 :: thesis: ( not g in X or g <= f )
assume g in X ; :: thesis: g <= f
then A9: ( g <= sup 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 = (sup X) . j or ( f . j = a & j = i ) ) by A8, FUNCT_7:33, FUNCT_7:34;
hence f . j >= g . j by A7, A9, Th28, LATTICE3:def 9; :: thesis: verum

end;

hence g <= f by Th28; :: thesis: verum

end;

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

end;

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