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:35
.= <*(a * a1)*> by Th48 ; :: thesis: verum