let K be non empty multMagma ; :: thesis: for a, b being Element of K holds ( the multF of K [;] (a,(id the carrier of K))) . b = a * b
let a, b be Element of K; :: thesis: ( the multF of K [;] (a,(id the carrier of K))) . b = a * b
thus ( the multF of K [;] (a,(id the carrier of K))) . b = the multF of K . (a,((id the carrier of K) . b)) by FUNCOP_1:53
.= a * b ; :: thesis: verum