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: for i being object st i in dom <*b*> holds
<*(a * b)*> /. i = a * (<*b*> /. i)

proof

let i be object ; :: 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:2, FINSEQ_1:38;
then A2: i = 1 by TARSKI:def 1;
hence <*(a * b)*> /. i = a * b by FINSEQ_4:16
.= a * (<*b*> /. i) by A2, FINSEQ_4:16 ;
:: thesis: verum

end;

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