let I be non empty set ; :: thesis: for X, Y being ManySortedSet of I
for i being Element of I * holds product ((X (/\) Y) * i) = (product (X * i)) /\ (product (Y * i))

let X, Y be ManySortedSet of I; :: thesis: for i being Element of I * holds product ((X (/\) Y) * i) = (product (X * i)) /\ (product (Y * i))
let i be Element of I * ; :: thesis: product ((X (/\) Y) * i) = (product (X * i)) /\ (product (Y * i))
A1: rng i c= I by FINSEQ_1:def 4;
dom X = I by PARTFUN1:def 2;
then A2: dom (X * i) = dom i by ;
dom (X (/\) Y) = I by PARTFUN1:def 2;
then A3: dom ((X (/\) Y) * i) = dom i by ;
dom Y = I by PARTFUN1:def 2;
then A4: dom (Y * i) = dom i by ;
thus product ((X (/\) Y) * i) c= (product (X * i)) /\ (product (Y * i)) :: according to XBOOLE_0:def 10 :: thesis: (product (X * i)) /\ (product (Y * i)) c= product ((X (/\) Y) * i)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in product ((X (/\) Y) * i) or x in (product (X * i)) /\ (product (Y * i)) )
assume x in product ((X (/\) Y) * i) ; :: thesis: x in (product (X * i)) /\ (product (Y * i))
then consider g being Function such that
A5: ( x = g & dom g = dom ((X (/\) Y) * i) ) and
A6: for y being object st y in dom ((X (/\) Y) * i) holds
g . y in ((X (/\) Y) * i) . y by CARD_3:def 5;
for y being object st y in dom (Y * i) holds
g . y in (Y * i) . y
proof
let y be object ; :: thesis: ( y in dom (Y * i) implies g . y in (Y * i) . y )
assume A7: y in dom (Y * i) ; :: thesis: g . y in (Y * i) . y
then g . y in ((X (/\) Y) * i) . y by A4, A3, A6;
then A8: g . y in (X (/\) Y) . (i . y) by ;
i . y in rng i by ;
then g . y in (X . (i . y)) /\ (Y . (i . y)) by ;
then g . y in Y . (i . y) by XBOOLE_0:def 4;
hence g . y in (Y * i) . y by ; :: thesis: verum
end;
then A9: x in product (Y * i) by ;
for y being object st y in dom (X * i) holds
g . y in (X * i) . y
proof
let y be object ; :: thesis: ( y in dom (X * i) implies g . y in (X * i) . y )
assume A10: y in dom (X * i) ; :: thesis: g . y in (X * i) . y
then g . y in ((X (/\) Y) * i) . y by A2, A3, A6;
then A11: g . y in (X (/\) Y) . (i . y) by ;
i . y in rng i by ;
then g . y in (X . (i . y)) /\ (Y . (i . y)) by ;
then g . y in X . (i . y) by XBOOLE_0:def 4;
hence g . y in (X * i) . y by ; :: thesis: verum
end;
then x in product (X * i) by ;
hence x in (product (X * i)) /\ (product (Y * i)) by ; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (product (X * i)) /\ (product (Y * i)) or x in product ((X (/\) Y) * i) )
assume A12: x in (product (X * i)) /\ (product (Y * i)) ; :: thesis: x in product ((X (/\) Y) * i)
then x in product (X * i) by XBOOLE_0:def 4;
then consider g being Function such that
A13: x = g and
A14: dom g = dom (X * i) and
A15: for y being object st y in dom (X * i) holds
g . y in (X * i) . y by CARD_3:def 5;
x in product (Y * i) by ;
then A16: ex h being Function st
( x = h & dom h = dom (Y * i) & ( for y being object st y in dom (Y * i) holds
h . y in (Y * i) . y ) ) by CARD_3:def 5;
for y being object st y in dom ((X (/\) Y) * i) holds
g . y in ((X (/\) Y) * i) . y
proof
let y be object ; :: thesis: ( y in dom ((X (/\) Y) * i) implies g . y in ((X (/\) Y) * i) . y )
assume A17: y in dom ((X (/\) Y) * i) ; :: thesis: g . y in ((X (/\) Y) * i) . y
then A18: i . y in rng i by ;
g . y in (X * i) . y by A2, A3, A15, A17;
then A19: g . y in X . (i . y) by ;
g . y in (Y * i) . y by A4, A3, A13, A16, A17;
then g . y in Y . (i . y) by ;
then g . y in (X . (i . y)) /\ (Y . (i . y)) by ;
then g . y in (X (/\) Y) . (i . y) by ;
hence g . y in ((X (/\) Y) * i) . y by ; :: thesis: verum
end;
hence x in product ((X (/\) Y) * i) by ; :: thesis: verum