let K be non empty multMagma ; :: thesis: for a, a1 being Element of K holds a * <*a1*> = <*(a * a1)*>
let a, a1 be Element of K; :: thesis: a * <*a1*> = <*(a * a1)*>
thus a * <*a1*> = <*((the multF of K [;] a,(id the carrier of K)) . a1)*> by FINSEQ_2:39
.= <*(a * a1)*> by Th60 ; :: thesis: verum