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 ;
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
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 ;
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 ;
hence (Carrier <*X,Y*>) . a = <* the carrier of X, the carrier of Y*> . a by ; :: 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 ;
hence (Carrier <*X,Y*>) . a = <* the carrier of X, the carrier of Y*> . a by ; :: thesis: verum
end;
end;
end;
hence the carrier of (product <*X,Y*>) = product <* the carrier of X, the carrier of Y*> by ; :: thesis: verum