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 by FINSEQ_1:def 8;

reconsider l = <*x1*>, p = <*x2*>, lpl = <*x1*> * <*x2*>, lpp = <*(x1 * x2)*> as Element of product (Carrier <*G1*>) by Def2;

A2: l . 1 = x1 by FINSEQ_1:def 8;

A3: p . 1 = x2 by FINSEQ_1:def 8;

A4: lpp . 1 = x1 * x2 by FINSEQ_1:def 8;

A5: 1 in {1} by TARSKI:def 1;

A6: for k being Nat st 1 <= k & k <= 1 holds

lpl . k = lpp . k

.= 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

let x1, x2 be Element of G1; :: thesis: <*x1*> * <*x2*> = <*(x1 * x2)*>

set G = <*G1*>;

A1: <*G1*> . 1 = G1 by FINSEQ_1:def 8;

reconsider l = <*x1*>, p = <*x2*>, lpl = <*x1*> * <*x2*>, lpp = <*(x1 * x2)*> as Element of product (Carrier <*G1*>) by Def2;

A2: l . 1 = x1 by FINSEQ_1:def 8;

A3: p . 1 = x2 by FINSEQ_1:def 8;

A4: lpp . 1 = x1 * x2 by FINSEQ_1:def 8;

A5: 1 in {1} by TARSKI:def 1;

A6: for k being Nat st 1 <= k & k <= 1 holds

lpl . k = lpp . k

proof

dom lpl =
dom (Carrier <*G1*>)
by CARD_3:9
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, A4, Th1; :: thesis: verum

end;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, A4, Th1; :: thesis: verum

.= 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