let H be Subgroup of G; H is add-associative
let x, y, z be Element of H; RLVECT_1:def 3 (x + y) + z = x + (y + z)
( y + z in the carrier of H & the carrier of H c= the carrier of G )
by DefA5;
then reconsider a = x, b = y, c = z, ab = x + y, bc = y + z as Element of G ;
thus (x + y) + z =
ab + c
by Th43
.=
(a + b) + c
by Th43
.=
a + (b + c)
by RLVECT_1:def 3
.=
a + bc
by Th43
.=
x + (y + z)
by Th43
; verum