let I be non empty set ; 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; for i being Element of I * holds product ((X (/\) Y) * i) = (product (X * i)) /\ (product (Y * i))
let i be Element of I * ; 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))
XBOOLE_0:def 10 (product (X * i)) /\ (product (Y * i)) c= product ((X (/\) Y) * i)proof
let x be
object ;
TARSKI:def 3 ( not x in product ((X (/\) Y) * i) or x in (product (X * i)) /\ (product (Y * i)) )
assume
x in product ((X (/\) Y) * i)
;
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 ;
( y in dom (Y * i) implies g . y in (Y * i) . y )
assume A7:
y in dom (Y * i)
;
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;
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 ;
( y in dom (X * i) implies g . y in (X * i) . y )
assume A10:
y in dom (X * i)
;
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;
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;
verum
end;
let x be object ; TARSKI:def 3 ( 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))
; 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 ;
( y in dom ((X (/\) Y) * i) implies g . y in ((X (/\) Y) * i) . y )
assume A17:
y in dom ((X (/\) Y) * i)
;
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;
verum
end;
hence
x in product ((X (/\) Y) * i)
by A2, A3, A13, A14, CARD_3:def 5; verum