let I be non empty set ; :: thesis: for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I 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 I; :: 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 and
A6: a = f . i by CARD_3:def 6;
reconsider f = f as Element of (product J) by A5;
sup X >= f by A3, A5;
hence a <= (sup X) . i by A6, Th28; :: thesis: verum

end;

A7: J . i is complete LATTICE by A1;

now :: thesis: for a being Element of (J . i) st a is_>=_than pi (X,i) holds
(sup X) . i <= a

let a be Element of (J . i); :: thesis: ( a is_>=_than pi (X,i) implies (sup X) . i <= a )
assume A8: a is_>=_than pi (X,i) ; :: thesis: (sup X) . i <= a
set f = (sup X) +* (i,a);
A9: dom ((sup X) +* (i,a)) = dom (sup X) by FUNCT_7:30;
A10: dom (sup X) = I by Th27;

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

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 A10, FUNCT_7:31, FUNCT_7:32;
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 A9, 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 A11: g in X ; :: thesis: g <= f
then A12: g <= sup X by A2, YELLOW_2:22;
A13: g . i in pi (X,i) by A11, CARD_3:def 6;

now :: thesis: for j being Element of I holds f . j >= g . j

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 A10, FUNCT_7:31, FUNCT_7:32;
hence f . j >= g . j by A8, A12, A13, Th28; :: thesis: verum

end;

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

end;

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

end;

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