let h, g, f be Element of G; :: according to BINOP_1:def 3 :: thesis: the addF of G . (h,( the addF of G . (g,f))) = the addF of G . (( the addF of G . (h,g)),f)
set o = the addF of G;
thus the addF of G . (h,( the addF of G . (g,f))) = h + (g + f)
.= (h + g) + f by RLVECT_1:def 3
.= the addF of G . (( the addF of G . (h,g)),f) ; :: thesis: verum