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

proof

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

end;

hence a * <*b*> = <*(a * b)*> by A1, Def2; :: thesis: verum