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 sup-Semilattice ) holds
product J is with_suprema

let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I; :: thesis: ( ( for i being Element of I holds J . i is sup-Semilattice ) implies product J is with_suprema )
assume A1: for i being Element of I holds J . i is sup-Semilattice ; :: thesis:
set IT = product J;
for x, y being Element of () ex z being Element of () st
( x <= z & y <= z & ( for z9 being Element of () st x <= z9 & y <= z9 holds
z <= z9 ) )
proof
let x, y be Element of (); :: thesis: ex z being Element of () st
( x <= z & y <= z & ( for z9 being Element of () st x <= z9 & y <= z9 holds
z <= z9 ) )

deffunc H1( Element of I) -> Element of the carrier of (J . \$1) = (x . \$1) "\/" (y . \$1);
consider z being ManySortedSet of I such that
A2: for i being Element of I holds z . i = H1(i) from PBOOLE:sch 5();
A3: for i being Element of I holds z . i is Element of (J . i)
proof
let i be Element of I; :: thesis: z . i is Element of (J . i)
z . i = (x . i) "\/" (y . i) by A2;
hence z . i is Element of (J . i) ; :: thesis: verum
end;
dom z = I by PARTFUN1:def 2;
then reconsider z = z as Element of () by ;
take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of () st x <= z9 & y <= z9 holds
z <= z9 ) )

for i being Element of I holds
( x . i <= z . i & y . i <= z . i )
proof
let i be Element of I; :: thesis: ( x . i <= z . i & y . i <= z . i )
( J . i is antisymmetric with_suprema RelStr & z . i = (x . i) "\/" (y . i) ) by A1, A2;
hence ( x . i <= z . i & y . i <= z . i ) by YELLOW_0:22; :: thesis: verum
end;
hence ( x <= z & y <= z ) by WAYBEL_3:28; :: thesis: for z9 being Element of () st x <= z9 & y <= z9 holds
z <= z9

let z9 be Element of (); :: thesis: ( x <= z9 & y <= z9 implies z <= z9 )
assume that
A4: x <= z9 and
A5: y <= z9 ; :: thesis: z <= z9
for i being Element of I holds z . i <= z9 . i
proof
let i be Element of I; :: thesis: z . i <= z9 . i
A6: ( z9 . i >= y . i & z . i = (x . i) "\/" (y . i) ) by ;
( J . i is antisymmetric with_suprema RelStr & z9 . i >= x . i ) by ;
hence z . i <= z9 . i by ; :: thesis: verum
end;
hence z <= z9 by WAYBEL_3:28; :: thesis: verum
end;
hence product J is with_suprema ; :: thesis: verum