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