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)

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

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 * i)) /\ (product (Y * i)) or x in product ((X (/\) Y) * i) )
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

for y being object st y in dom (X * i) holds

g . y in (X * i) . y

hence x in (product (X * i)) /\ (product (Y * i)) by A9, XBOOLE_0:def 4; :: thesis: verum

end;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

then A9:
x in product (Y * i)
by A4, A3, A5, CARD_3:def 5;
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;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

for y being object st y in dom (X * i) holds

g . y in (X * i) . y

proof

then
x in product (X * i)
by A2, A3, A5, CARD_3:def 5;
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;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

hence x in (product (X * i)) /\ (product (Y * i)) by A9, XBOOLE_0:def 4; :: thesis: verum

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

hence
x in product ((X (/\) Y) * i)
by A2, A3, A13, A14, CARD_3:def 5; :: thesis: verum
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;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