let h, g, f be Element of G; :: according to BINOP_1:def 3 :: 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 Def3
.= the multF of G . (( the multF of G . (h,g)),f) ; :: thesis: verum