let I be set ; :: thesis: for f, g being ManySortedSet of I holds () /\ () = product (f (/\) g)
let f, g be ManySortedSet of I; :: thesis: () /\ () = product (f (/\) g)
for x being object holds
( x in () /\ () 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 () /\ () 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 () /\ () )
assume x in () /\ () ; :: 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
.= 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 ;
then A6: h . y in f . y by A3;
h . y in g . y by ;
then h . y in (f . y) /\ (g . y) by ;
hence h . y in (f (/\) g) . y by ; :: 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 () /\ ()
a9: dom h = I by ;
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 ;
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 ;
for y being object st y in dom g holds
h . y in g . y by A10;
then h in product g by ;
hence x in () /\ () by ; :: thesis: verum
end;
hence (product f) /\ () = product (f (/\) g) by CARD_3:def 5; :: thesis: verum