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: product J is with_suprema

set IT = product J;

for x, y being Element of (product J) ex z being Element of (product J) st

( x <= z & y <= z & ( for z9 being Element of (product J) st x <= z9 & y <= z9 holds

z <= z9 ) )

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: product J is with_suprema

set IT = product J;

for x, y being Element of (product J) ex z being Element of (product J) st

( x <= z & y <= z & ( for z9 being Element of (product J) st x <= z9 & y <= z9 holds

z <= z9 ) )

proof

hence
product J is with_suprema
; :: thesis: verum
let x, y be Element of (product J); :: thesis: ex z being Element of (product J) st

( x <= z & y <= z & ( for z9 being Element of (product J) st x <= z9 & y <= z9 holds

z <= z9 ) )

deffunc H_{1}( 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 = H_{1}(i)
from PBOOLE:sch 5();

A3: for i being Element of I holds z . i is Element of (J . i)

then reconsider z = z as Element of (product J) by A3, WAYBEL_3:27;

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of (product J) st x <= z9 & y <= z9 holds

z <= z9 ) )

for i being Element of I holds

( x . i <= z . i & y . i <= z . i )

z <= z9

let z9 be Element of (product J); :: 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

end;( x <= z & y <= z & ( for z9 being Element of (product J) st x <= z9 & y <= z9 holds

z <= z9 ) )

deffunc H

consider z being ManySortedSet of I such that

A2: for i being Element of I holds z . i = H

A3: for i being Element of I holds z . i is Element of (J . i)

proof

dom z = I
by PARTFUN1:def 2;
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;z . i = (x . i) "\/" (y . i) by A2;

hence z . i is Element of (J . i) ; :: thesis: verum

then reconsider z = z as Element of (product J) by A3, WAYBEL_3:27;

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of (product J) st x <= z9 & y <= z9 holds

z <= z9 ) )

for i being Element of I holds

( x . i <= z . i & y . i <= z . i )

proof

hence
( x <= z & y <= z )
by WAYBEL_3:28; :: thesis: for z9 being Element of (product J) st x <= z9 & y <= z9 holds
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;( 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

z <= z9

let z9 be Element of (product J); :: 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

hence
z <= z9
by WAYBEL_3:28; :: thesis: verum
let i be Element of I; :: thesis: z . i <= z9 . i

A6: ( z9 . i >= y . i & z . i = (x . i) "\/" (y . i) ) by A2, A5, WAYBEL_3:28;

( J . i is antisymmetric with_suprema RelStr & z9 . i >= x . i ) by A1, A4, WAYBEL_3:28;

hence z . i <= z9 . i by A6, YELLOW_0:22; :: thesis: verum

end;A6: ( z9 . i >= y . i & z . i = (x . i) "\/" (y . i) ) by A2, A5, WAYBEL_3:28;

( J . i is antisymmetric with_suprema RelStr & z9 . i >= x . i ) by A1, A4, WAYBEL_3:28;

hence z . i <= z9 . i by A6, YELLOW_0:22; :: thesis: verum