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:66
.= b * a by FUNCT_1:35 ; :: thesis: verum