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