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 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 ; :: 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: for i being Element of I holds J . i is antisymmetric by A1;
A3: J . i is Semilattice by A1;
A4: ( product J is antisymmetric & product J is with_infima ) by A1, A2, Th10, WAYBEL_3:30;
A5: (f "/\" g) . i <= (f . i) "/\" (g . i)

proof

( f >= f "/\" g & g >= f "/\" g ) by A4, YELLOW_0:23;
then ( f . i >= (f "/\" g) . i & g . i >= (f "/\" g) . i ) by WAYBEL_3:28;
hence (f "/\" g) . i <= (f . i) "/\" (g . i) by A3, YELLOW_0:23; :: thesis: verum

end;

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

proof

deffunc H₁( Element of I) -> Element of the carrier of (J . $1) = (f . $1) "/\" (g . $1);
consider z being ManySortedSet of such that
A6: for i being Element of I holds z . i = H₁(i) from PBOOLE:sch 5();
A7: dom z = I by PARTFUN1:def 4;
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 = (f . i) "/\" (g . i) by A6;
hence z . i is Element of (J . i) ; :: thesis: verum

end;

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

let i be Element of I; :: thesis: ( z . i <= f . i & z . i <= g . i )
A8: J . i is antisymmetric with_infima RelStr by A1;
z . i = (f . i) "/\" (g . i) by A6;
hence ( z . i <= f . i & z . i <= g . i ) by A8, YELLOW_0:23; :: thesis: verum

end;

then ( z <= f & z <= g ) by WAYBEL_3:28;
then A9: f "/\" g >= z by A4, YELLOW_0:23;
for i being Element of I holds (f "/\" g) . i >= (f . i) "/\" (g . i)

proof

let i be Element of I; :: thesis: (f "/\" g) . i >= (f . i) "/\" (g . i)
( (f . i) "/\" (g . i) = z . i & (f "/\" g) . i >= z . i ) by A6, A9, WAYBEL_3:28;
hence (f "/\" g) . i >= (f . i) "/\" (g . i) ; :: thesis: verum

end;

hence (f "/\" g) . i >= (f . i) "/\" (g . i) ; :: thesis: verum

end;

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