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 Semilattice ) holds

for f, g being Element of (product J)

for i being Element of I holds (f "/\" g) . i = (f . i) "/\" (g . i)

let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I; :: thesis: ( ( for i being Element of I holds J . i is Semilattice ) implies for f, g being Element of (product J)

for i being Element of I holds (f "/\" g) . i = (f . i) "/\" (g . i) )

assume A1: for i being Element of I holds J . i is Semilattice ; :: thesis: for f, g being Element of (product J)

for i being Element of I holds (f "/\" g) . i = (f . i) "/\" (g . i)

let f, g be Element of (product J); :: thesis: for i being Element of I holds (f "/\" g) . i = (f . i) "/\" (g . i)

let i be Element of I; :: thesis: (f "/\" g) . i = (f . i) "/\" (g . i)

A2: J . i is Semilattice by A1;

for i being Element of I holds J . i is antisymmetric by A1;

then A3: ( product J is antisymmetric & product J is with_infima ) by A1, Th10, WAYBEL_3:30;

then g >= f "/\" g by YELLOW_0:23;

then A4: g . i >= (f "/\" g) . i by WAYBEL_3:28;

A5: (f "/\" g) . i >= (f . i) "/\" (g . i)

then f . i >= (f "/\" g) . i by WAYBEL_3:28;

then (f "/\" g) . i <= (f . i) "/\" (g . i) by A2, A4, YELLOW_0:23;

hence (f "/\" g) . i = (f . i) "/\" (g . i) by A2, A5, YELLOW_0:def 3; :: thesis: verum

for f, g being Element of (product J)

for i being Element of I holds (f "/\" g) . i = (f . i) "/\" (g . i)

let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I; :: thesis: ( ( for i being Element of I holds J . i is Semilattice ) implies for f, g being Element of (product J)

for i being Element of I holds (f "/\" g) . i = (f . i) "/\" (g . i) )

assume A1: for i being Element of I holds J . i is Semilattice ; :: thesis: for f, g being Element of (product J)

for i being Element of I holds (f "/\" g) . i = (f . i) "/\" (g . i)

let f, g be Element of (product J); :: thesis: for i being Element of I holds (f "/\" g) . i = (f . i) "/\" (g . i)

let i be Element of I; :: thesis: (f "/\" g) . i = (f . i) "/\" (g . i)

A2: J . i is Semilattice by A1;

for i being Element of I holds J . i is antisymmetric by A1;

then A3: ( product J is antisymmetric & product J is with_infima ) by A1, Th10, WAYBEL_3:30;

then g >= f "/\" g by YELLOW_0:23;

then A4: g . i >= (f "/\" g) . i by WAYBEL_3:28;

A5: (f "/\" g) . i >= (f . i) "/\" (g . i)

proof

f >= f "/\" g
by A3, YELLOW_0:23;
deffunc H_{1}( Element of I) -> Element of the carrier of (J . $1) = (f . $1) "/\" (g . $1);

consider z being ManySortedSet of I such that

A6: for i being Element of I holds z . i = H_{1}(i)
from PBOOLE:sch 5();

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

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

for i being Element of I holds

( z . i <= f . i & z . i <= g . i )

then A8: f "/\" g >= z by A3, YELLOW_0:23;

for i being Element of I holds (f "/\" g) . i >= (f . i) "/\" (g . i)

end;consider z being ManySortedSet of I such that

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

A7: 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 = (f . i) "/\" (g . i) by A6;

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

end;z . i = (f . i) "/\" (g . i) by A6;

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

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

for i being Element of I holds

( z . i <= f . i & z . i <= g . i )

proof

then
( z <= f & z <= g )
by WAYBEL_3:28;
let i be Element of I; :: thesis: ( z . i <= f . i & z . i <= g . i )

( J . i is antisymmetric with_infima RelStr & z . i = (f . i) "/\" (g . i) ) by A1, A6;

hence ( z . i <= f . i & z . i <= g . i ) by YELLOW_0:23; :: thesis: verum

end;( J . i is antisymmetric with_infima RelStr & z . i = (f . i) "/\" (g . i) ) by A1, A6;

hence ( z . i <= f . i & z . i <= g . i ) by YELLOW_0:23; :: thesis: verum

then A8: f "/\" g >= z by A3, YELLOW_0:23;

for i being Element of I holds (f "/\" g) . i >= (f . i) "/\" (g . i)

proof

hence
(f "/\" g) . i >= (f . i) "/\" (g . i)
; :: thesis: verum
let i be Element of I; :: thesis: (f "/\" g) . i >= (f . i) "/\" (g . i)

(f . i) "/\" (g . i) = z . i by A6;

hence (f "/\" g) . i >= (f . i) "/\" (g . i) by A8, WAYBEL_3:28; :: thesis: verum

end;(f . i) "/\" (g . i) = z . i by A6;

hence (f "/\" g) . i >= (f . i) "/\" (g . i) by A8, WAYBEL_3:28; :: thesis: verum

then f . i >= (f "/\" g) . i by WAYBEL_3:28;

then (f "/\" g) . i <= (f . i) "/\" (g . i) by A2, A4, YELLOW_0:23;

hence (f "/\" g) . i = (f . i) "/\" (g . i) by A2, A5, YELLOW_0:def 3; :: thesis: verum