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*>;
A1: <*G1*> . 1 = G1 ;
reconsider l = <*x1*>, p = <*x2*>, lpl = <*x1*> * <*x2*>, lpp = <*(x1 * x2)*> as Element of product (Carrier <*G1*>) by Def2;
A2: l . 1 = x1 ;
A3: p . 1 = x2 ;
A5: 1 in {1} by TARSKI:def 1;
A6: 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 )
assume that
A7: 1 <= k and
A8: k <= 1 ; :: thesis: lpl . k = lpp . k
k in Seg 1 by A7, A8;
then k = 1 by FINSEQ_1:2, TARSKI:def 1;
hence lpl . k = lpp . k by A5, A2, A3, A1, Th1; :: thesis: verum

end;

dom lpl = dom (Carrier <*G1*>) by CARD_3:9
.= Seg 1 by FINSEQ_1:2, PARTFUN1:def 2 ;
then A9: len lpl = 1 by FINSEQ_1:def 3;
len lpp = 1 by FINSEQ_1:39;
hence <*x1*> * <*x2*> = <*(x1 * x2)*> by A9, A6; :: thesis: verum