let G1 be non empty multMagma ; :: thesis: for x1, x2 being Element of G1 holds <*x1*> * <*x2*> = <*(x1 * x2)*>
let x1, x2 be Element of G1; :: thesis: <*x1*> * <*x2*> = <*(x1 * x2)*>
set G = <*G1*>;
reconsider l = <*x1*>, p = <*x2*>, lpl = <*x1*> * <*x2*>, lpp = <*(x1 * x2)*> as Element of product (Carrier <*G1*>) by Def2;
A1: 1 in {1} by TARSKI:def 1;
A2: ( l . 1 = x1 & p . 1 = x2 & <*G1*> . 1 = G1 ) by FINSEQ_1:def 8;
dom lpl = dom (Carrier <*G1*>) by CARD_3:18
.= Seg 1 by FINSEQ_1:4, PARTFUN1:def 4 ;
then A3: len lpl = 1 by FINSEQ_1:def 3;
A4: len lpp = 1 by FINSEQ_1:56;
A5: lpp . 1 = x1 * x2 by FINSEQ_1:def 8;
for k being Nat st 1 <= k & k <= 1 holds
lpl . k = lpp . k

proof

let k be Nat; :: thesis: ( 1 <= k & k <= 1 implies lpl . k = lpp . k )
A6: k in NAT by ORDINAL1:def 13;
assume ( 1 <= k & k <= 1 ) ; :: thesis: lpl . k = lpp . k
then k in Seg 1 by A6;
then k = 1 by FINSEQ_1:4, TARSKI:def 1;
hence lpl . k = lpp . k by A1, A2, A5, Th4; :: thesis: verum

end;

hence <*x1*> * <*x2*> = <*(x1 * x2)*> by A3, A4, FINSEQ_1:18; :: thesis: verum