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

now

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