let G be non empty addMagma ; :: thesis: for A being Subset of G
for g, h being Element of G st G is add-associative holds
(g + h) + A = g + (h + A)
let A be Subset of G; :: thesis: for g, h being Element of G st G is add-associative holds
(g + h) + A = g + (h + A)
let g, h be Element of G; :: thesis: ( G is add-associative implies (g + h) + A = g + (h + A) )
assume A1: G is add-associative ; :: thesis: (g + h) + A = g + (h + A)
thus (g + h) + A = ({g} + {h}) + A by Th18
.= g + (h + A) by A1, Th10 ; :: thesis: verum