let G be addGroup; :: thesis: for a, g, h being Element of G holds (a * g) * h = a * (g + h)
let a, g, h be Element of G; :: thesis: (a * g) * h = a * (g + h)
thus (a * g) * h = (((- h) + ((- g) + a)) + g) + h by RLVECT_1:def 3
.= ((((- h) + (- g)) + a) + g) + h by RLVECT_1:def 3
.= (((- (g + h)) + a) + g) + h by Th16
.= a * (g + h) by RLVECT_1:def 3 ; :: thesis: verum