let I be set ; :: thesis: for f, g being ManySortedSet of I holds (product f) /\ (product g) = product (f (/\) g)
let f, g be ManySortedSet of I; :: thesis: (product f) /\ (product g) = product (f (/\) g)
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 ) ) )

proof

let x be object ; :: thesis: ( 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 ) ) )

hereby :: thesis: ( 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 ) ) implies x in (product f) /\ (product g) )

assume x in (product f) /\ (product g) ; :: thesis: 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 ) )
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: ( h = x & dom h = dom (f (/\) g) & ( for y being object st y in dom (f (/\) g) holds
h . y in (f (/\) g) . y ) )
thus h = x by A2; :: thesis: ( dom h = dom (f (/\) g) & ( for y being object st y in dom (f (/\) g) holds
h . y in (f (/\) g) . y ) )
thus dom h = I by A2, PARTFUN1:def 2
.= dom (f (/\) g) by PARTFUN1:def 2 ; :: thesis: for y being object st y in dom (f (/\) g) holds
h . y in (f (/\) g) . y
let y be object ; :: thesis: ( y in dom (f (/\) g) implies h . y in (f (/\) g) . y )
assume a4: y in dom (f (/\) g) ; :: thesis: h . y in (f (/\) g) . y
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: verum

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: x in (product f) /\ (product g)
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: for y being object st ( y in dom f or y in dom g ) holds
( h . y in f . y & h . y in g . y )

let y be object ; :: thesis: ( ( y in dom f or y in dom g ) implies ( h . y in f . y & h . y in g . y ) )
assume A11: ( y in dom f or y in dom g ) ; :: thesis: ( h . y in f . y & h . y in g . y )
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: verum

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: verum

end;

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