let G1, G2 be non empty multMagma ; :: thesis: for x1, x2 being Element of G1

for y1, y2 being Element of G2 holds <*x1,y1*> * <*x2,y2*> = <*(x1 * x2),(y1 * y2)*>

let x1, x2 be Element of G1; :: thesis: for y1, y2 being Element of G2 holds <*x1,y1*> * <*x2,y2*> = <*(x1 * x2),(y1 * y2)*>

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

set G = <*G1,G2*>;

A1: <*G1,G2*> . 1 = G1 by FINSEQ_1:44;

A2: <*G1,G2*> . 2 = G2 by FINSEQ_1:44;

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

A3: 2 in {1,2} by TARSKI:def 2;

A4: l . 1 = x1 by FINSEQ_1:44;

A5: lpp . 1 = x1 * x2 by FINSEQ_1:44;

A6: p . 2 = y2 by FINSEQ_1:44;

A7: lpp . 2 = y1 * y2 by FINSEQ_1:44;

A8: p . 1 = x2 by FINSEQ_1:44;

A9: l . 2 = y1 by FINSEQ_1:44;

A10: 1 in {1,2} by TARSKI:def 2;

A11: for k being Nat st 1 <= k & k <= 2 holds

lpl . k = lpp . k

.= Seg 2 by FINSEQ_1:2, PARTFUN1:def 2 ;

then A15: len lpl = 2 by FINSEQ_1:def 3;

len lpp = 2 by FINSEQ_1:44;

hence <*x1,y1*> * <*x2,y2*> = <*(x1 * x2),(y1 * y2)*> by A15, A11; :: thesis: verum

for y1, y2 being Element of G2 holds <*x1,y1*> * <*x2,y2*> = <*(x1 * x2),(y1 * y2)*>

let x1, x2 be Element of G1; :: thesis: for y1, y2 being Element of G2 holds <*x1,y1*> * <*x2,y2*> = <*(x1 * x2),(y1 * y2)*>

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

set G = <*G1,G2*>;

A1: <*G1,G2*> . 1 = G1 by FINSEQ_1:44;

A2: <*G1,G2*> . 2 = G2 by FINSEQ_1:44;

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

A3: 2 in {1,2} by TARSKI:def 2;

A4: l . 1 = x1 by FINSEQ_1:44;

A5: lpp . 1 = x1 * x2 by FINSEQ_1:44;

A6: p . 2 = y2 by FINSEQ_1:44;

A7: lpp . 2 = y1 * y2 by FINSEQ_1:44;

A8: p . 1 = x2 by FINSEQ_1:44;

A9: l . 2 = y1 by FINSEQ_1:44;

A10: 1 in {1,2} by TARSKI:def 2;

A11: for k being Nat st 1 <= k & k <= 2 holds

lpl . k = lpp . k

proof

dom lpl =
dom (Carrier <*G1,G2*>)
by CARD_3:9
let k be Nat; :: thesis: ( 1 <= k & k <= 2 implies lpl . k = lpp . k )

assume that

A12: 1 <= k and

A13: k <= 2 ; :: thesis: lpl . k = lpp . k

A14: k in Seg 2 by A12, A13;

end;assume that

A12: 1 <= k and

A13: k <= 2 ; :: thesis: lpl . k = lpp . k

A14: k in Seg 2 by A12, A13;

.= Seg 2 by FINSEQ_1:2, PARTFUN1:def 2 ;

then A15: len lpl = 2 by FINSEQ_1:def 3;

len lpp = 2 by FINSEQ_1:44;

hence <*x1,y1*> * <*x2,y2*> = <*(x1 * x2),(y1 * y2)*> by A15, A11; :: thesis: verum