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