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 A1, RELAT_1:27;
dom (X (/\) Y) = I by PARTFUN1:def 2;
then A3: dom ((X (/\) Y) * i) = dom i by A1, RELAT_1:27;
dom Y = I by PARTFUN1:def 2;
then A4: dom (Y * i) = dom i by A1, RELAT_1:27;
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 A4, A3, A7, FUNCT_1:12;
i . y in rng i by A4, A7, FUNCT_1:def 3;
then g . y in (X . (i . y)) /\ (Y . (i . y)) by A1, A8, PBOOLE:def 5;
then g . y in Y . (i . y) by XBOOLE_0:def 4;
hence g . y in (Y * i) . y by A7, FUNCT_1:12; :: thesis: verum

end;

then A9: x in product (Y * i) by A4, A3, A5, CARD_3:def 5;
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 A2, A3, A10, FUNCT_1:12;
i . y in rng i by A2, A10, FUNCT_1:def 3;
then g . y in (X . (i . y)) /\ (Y . (i . y)) by A1, A11, PBOOLE:def 5;
then g . y in X . (i . y) by XBOOLE_0:def 4;
hence g . y in (X * i) . y by A10, FUNCT_1:12; :: thesis: verum

end;

then x in product (X * i) by A2, A3, A5, CARD_3:def 5;
hence x in (product (X * i)) /\ (product (Y * i)) by A9, XBOOLE_0:def 4; :: 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 A12, XBOOLE_0:def 4;
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 A3, FUNCT_1:def 3;
g . y in (X * i) . y by A2, A3, A15, A17;
then A19: g . y in X . (i . y) by A2, A3, A17, FUNCT_1:12;
g . y in (Y * i) . y by A4, A3, A13, A16, A17;
then g . y in Y . (i . y) by A4, A3, A17, FUNCT_1:12;
then g . y in (X . (i . y)) /\ (Y . (i . y)) by A19, XBOOLE_0:def 4;
then g . y in (X (/\) Y) . (i . y) by A1, A18, PBOOLE:def 5;
hence g . y in ((X (/\) Y) * i) . y by A17, FUNCT_1:12; :: thesis: verum

end;

hence x in product ((X (/\) Y) * i) by A2, A3, A13, A14, CARD_3:def 5; :: thesis: verum