let X, Y be non empty multMagma ; :: thesis: the carrier of (product <*X,Y*>) = product <* the carrier of X, the carrier of Y*>

set CarrX = the carrier of X;

set CarrY = the carrier of Y;

A1: the carrier of (product <*X,Y*>) = product (Carrier <*X,Y*>) by GROUP_7:def 2;

len <* the carrier of X, the carrier of Y*> = 2 by FINSEQ_1:44;

then A2: dom <* the carrier of X, the carrier of Y*> = {1,2} by FINSEQ_1:2, FINSEQ_1:def 3;

A3: ( <*X,Y*> . 1 = X & <*X,Y*> . 2 = Y ) by FINSEQ_1:44;

for a being object st a in dom (Carrier <*X,Y*>) holds

(Carrier <*X,Y*>) . a = <* the carrier of X, the carrier of Y*> . a

set CarrX = the carrier of X;

set CarrY = the carrier of Y;

A1: the carrier of (product <*X,Y*>) = product (Carrier <*X,Y*>) by GROUP_7:def 2;

len <* the carrier of X, the carrier of Y*> = 2 by FINSEQ_1:44;

then A2: dom <* the carrier of X, the carrier of Y*> = {1,2} by FINSEQ_1:2, FINSEQ_1:def 3;

A3: ( <*X,Y*> . 1 = X & <*X,Y*> . 2 = Y ) by FINSEQ_1:44;

for a being object st a in dom (Carrier <*X,Y*>) holds

(Carrier <*X,Y*>) . a = <* the carrier of X, the carrier of Y*> . a

proof

hence
the carrier of (product <*X,Y*>) = product <* the carrier of X, the carrier of Y*>
by PARTFUN1:def 2, A2, FUNCT_1:2, A1; :: thesis: verum
let a be object ; :: thesis: ( a in dom (Carrier <*X,Y*>) implies (Carrier <*X,Y*>) . a = <* the carrier of X, the carrier of Y*> . a )

assume A4: a in dom (Carrier <*X,Y*>) ; :: thesis: (Carrier <*X,Y*>) . a = <* the carrier of X, the carrier of Y*> . a

end;assume A4: a in dom (Carrier <*X,Y*>) ; :: thesis: (Carrier <*X,Y*>) . a = <* the carrier of X, the carrier of Y*> . a

per cases
( a = 1 or a = 2 )
by A4, TARSKI:def 2;

end;

suppose A5:
a = 1
; :: thesis: (Carrier <*X,Y*>) . a = <* the carrier of X, the carrier of Y*> . a

then
ex R being 1-sorted st

( R = <*X,Y*> . 1 & (Carrier <*X,Y*>) . 1 = the carrier of R ) by A4, PRALG_1:def 15;

hence (Carrier <*X,Y*>) . a = <* the carrier of X, the carrier of Y*> . a by FINSEQ_1:44, A3, A5; :: thesis: verum

end;( R = <*X,Y*> . 1 & (Carrier <*X,Y*>) . 1 = the carrier of R ) by A4, PRALG_1:def 15;

hence (Carrier <*X,Y*>) . a = <* the carrier of X, the carrier of Y*> . a by FINSEQ_1:44, A3, A5; :: thesis: verum

suppose A6:
a = 2
; :: thesis: (Carrier <*X,Y*>) . a = <* the carrier of X, the carrier of Y*> . a

then
ex R being 1-sorted st

( R = <*X,Y*> . 2 & (Carrier <*X,Y*>) . 2 = the carrier of R ) by A4, PRALG_1:def 15;

hence (Carrier <*X,Y*>) . a = <* the carrier of X, the carrier of Y*> . a by FINSEQ_1:44, A3, A6; :: thesis: verum

end;( R = <*X,Y*> . 2 & (Carrier <*X,Y*>) . 2 = the carrier of R ) by A4, PRALG_1:def 15;

hence (Carrier <*X,Y*>) . a = <* the carrier of X, the carrier of Y*> . a by FINSEQ_1:44, A3, A6; :: thesis: verum