let L be non empty multMagma ; :: thesis: for a, b being Element of L holds <*b*> * a = <*(b * a)*>
let a, b be Element of L; :: thesis: <*b*> * a = <*(b * a)*>
A1: for i being object st i in dom <*b*> holds
<*(b * a)*> /. i = (<*b*> /. i) * a

proof

let i be object ; :: thesis: ( i in dom <*b*> implies <*(b * a)*> /. i = (<*b*> /. i) * a )
assume i in dom <*b*> ; :: thesis: <*(b * a)*> /. i = (<*b*> /. i) * a
then i in {1} by FINSEQ_1:2, FINSEQ_1:38;
then A2: i = 1 by TARSKI:def 1;
hence <*(b * a)*> /. i = b * a by FINSEQ_4:16
.= (<*b*> /. i) * a by A2, FINSEQ_4:16 ;
:: thesis: verum

end;

dom <*(b * a)*> = Seg 1 by FINSEQ_1:38
.= dom <*b*> by FINSEQ_1:38 ;
hence <*b*> * a = <*(b * a)*> by A1, Def2; :: thesis: verum