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

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

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

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 A5; :: thesis: verum

end;

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 A6; :: thesis: verum

end;

end;

end;

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