let G be non empty associative multMagma ; :: thesis: the multF of G is associative
let h, g, f be Element of G; :: according to BINOP_1:def 14 :: thesis: the multF of G . h,(the multF of G . g,f) = the multF of G . (the multF of G . h,g),f
set o = the multF of G;
thus the multF of G . h,(the multF of G . g,f) = h * (g * f)
.= (h * g) * f by Def4
.= the multF of G . (the multF of G . h,g),f ; :: thesis: verum