let K be non empty commutative multMagma ; :: thesis: the multF of K is commutative

now :: thesis: for a, b being Element of K holds the multF of K . (a,b) = the multF of K . (b,a)

let a, b be Element of K; :: thesis: the multF of K . (a,b) = the multF of K . (b,a)
thus the multF of K . (a,b) = a * b
.= b * a
.= the multF of K . (b,a) ; :: thesis: verum

end;

hence the multF of K is commutative by BINOP_1:def 2; :: thesis: verum