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
product J is complete LATTICE
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 product J is complete LATTICE )
assume A1: for i being Element of I holds J . i is complete LATTICE ; :: thesis: product J is complete LATTICE
then A2: for i being Element of I holds J . i is transitive ;
for i being Element of I holds J . i is antisymmetric by A1;
then reconsider L = product J as non empty Poset by A2, Th29, Th30;

now

let X be Subset of (product J); :: thesis: ex_sup_of X, product J
deffunc H₁( Element of I) -> Element of the carrier of (J . $1) = sup (pi X,$1);
consider f being ManySortedSet of such that
A3: for i being Element of I holds f . i = H₁(i) from PBOOLE:sch 5();
A4: dom f = I by PARTFUN1:def 4;

now

let i be Element of I; :: thesis: f . i is Element of (J . i)
f . i = sup (pi X,i) by A3;
hence f . i is Element of (J . i) ; :: thesis: verum

end;

then reconsider f = f as Element of (product J) by A4, Th27;
A5: f is_>=_than X

proof

let x be Element of (product J); :: according to LATTICE3:def 9 :: thesis: ( not x in X or x <= f )
assume A6: x in X ; :: thesis: x <= f

now

let i be Element of I; :: thesis: x . i <= f . i
( x . i in pi X,i & J . i is complete LATTICE & f . i = sup (pi X,i) ) by A1, A3, A6, CARD_3:def 6;
hence x . i <= f . i by YELLOW_2:24; :: thesis: verum

end;

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

end;

now

let g be Element of (product J); :: thesis: ( X is_<=_than g implies f <= g )
assume A7: X is_<=_than g ; :: thesis: f <= g

now

thus L = L ; :: thesis: for i being Element of I holds f . i <= g . i
let i be Element of I; :: thesis: f . i <= g . i
A8: ( f . i = sup (pi X,i) & J . i is complete LATTICE ) by A1, A3;
g . 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 <= g . i )
assume a in pi X,i ; :: thesis: a <= g . i
then consider h being Function such that
A9: ( h in X & a = h . i ) by CARD_3:def 6;
reconsider h = h as Element of (product J) by A9;
h <= g by A7, A9, LATTICE3:def 9;
hence a <= g . i by A9, Th28; :: thesis: verum

end;

hence f . i <= g . i by A8, YELLOW_0:32; :: thesis: verum

end;

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

end;

then ex_sup_of X,L by A5, YELLOW_0:15;
hence ex_sup_of X, product J ; :: thesis: verum

end;

then L is non empty complete Poset by YELLOW_0:53;
hence product J is complete LATTICE ; :: thesis: verum