let I be set ; :: thesis:
let f, g be ManySortedSet of I; :: thesis:
for x being object holds
( x in (product f) /\ (product g) iff ex h being Function st
( h = x & dom h = dom (f (/\) g) & ( for y being object st y in dom (f (/\) g) holds
h . y in (f (/\) g) . y ) ) )

let x be object ; :: thesis:

hereby :: thesis:

assume x in (product f) /\ (product g) ; :: thesis:
then A1: ( x in product f & x in product g ) by XBOOLE_0:def 4;
then consider h being Function such that
A2: ( h = x & dom h = dom f ) and
A3: for y being object st y in dom f holds
h . y in f . y by CARD_3:def 5;
take h = h; :: thesis:
thus h = x by A2; :: thesis:
thus dom h = I by A2, PARTFUN1:def 2
.= dom (f (/\) g) by PARTFUN1:def 2 ; :: thesis:
let y be object ; :: thesis:
assume a4: y in dom (f (/\) g) ; :: thesis:
then A4: y in I ;
A5: ( y in dom f & y in dom g ) by A4, PARTFUN1:def 2;
then A6: h . y in f . y by A3;
h . y in g . y by A1, A2, A5, CARD_3:9;
then h . y in (f . y) /\ (g . y) by A6, XBOOLE_0:def 4;
hence h . y in (f (/\) g) . y by a4, PBOOLE:def 5; :: thesis:

end;

given h being Function such that A7: ( h = x & dom h = dom (f (/\) g) ) and
A8: for y being object st y in dom (f (/\) g) holds
h . y in (f (/\) g) . y ; :: thesis:
a9: dom h = I by A7, PARTFUN1:def 2;
then A9: ( dom h = dom f & dom h = dom g ) by PARTFUN1:def 2;

A10: now :: thesis:

let y be object ; :: thesis:
assume A11: ( y in dom f or y in dom g ) ; :: thesis:
h . y in (f (/\) g) . y by A7, A8, a9, A11;
then h . y in (f . y) /\ (g . y) by A11, PBOOLE:def 5;
hence ( h . y in f . y & h . y in g . y ) by XBOOLE_0:def 4; :: thesis:

end;

for y being object st y in dom f holds
h . y in f . y by A10;
then A13: h in product f by A9, CARD_3:9;
for y being object st y in dom g holds
h . y in g . y by A10;
then h in product g by A9, CARD_3:9;
hence x in (product f) /\ (product g) by A7, A13, XBOOLE_0:def 4; :: thesis:

end;

hence (product f) /\ (product g) = product (f (/\) g) by CARD_3:def 5; :: thesis: