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 ()
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 ()
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 ()
for i being Element of I holds (f "/\" g) . i = (f . i) "/\" (g . i)

let f, g be Element of (); :: 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 ;
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
deffunc H1( 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 = H1(i) from PBOOLE:sch 5();
A7: 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;
dom z = I by PARTFUN1:def 2;
then reconsider z = z as Element of () by ;
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 )
( 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;
then ( z <= f & z <= g ) by WAYBEL_3:28;
then A8: f "/\" g >= z by ;
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 by A6;
hence (f "/\" g) . i >= (f . i) "/\" (g . i) by ; :: thesis: verum
end;
hence (f "/\" g) . i >= (f . i) "/\" (g . i) ; :: thesis: verum
end;
f >= f "/\" g by ;
then f . i >= (f "/\" g) . i by WAYBEL_3:28;
then (f "/\" g) . i <= (f . i) "/\" (g . i) by ;
hence (f "/\" g) . i = (f . i) "/\" (g . i) by ; :: thesis: verum