let V be non empty right_complementable add-associative right_zeroed addLoopStr ; for v, u being Element of V holds
( Sum <*(0. V),u,v*> = u + v & Sum <*u,v,(0. V)*> = u + v & Sum <*u,(0. V),v*> = u + v )
let v, u be Element of V; ( Sum <*(0. V),u,v*> = u + v & Sum <*u,v,(0. V)*> = u + v & Sum <*u,(0. V),v*> = u + v )
thus Sum <*(0. V),u,v*> =
((0. V) + u) + v
by Th46
.=
u + v
; ( Sum <*u,v,(0. V)*> = u + v & Sum <*u,(0. V),v*> = u + v )
thus Sum <*u,v,(0. V)*> =
(u + v) + (0. V)
by Th46
.=
u + v
; Sum <*u,(0. V),v*> = u + v
thus Sum <*u,(0. V),v*> =
(u + (0. V)) + v
by Th46
.=
u + v
; verum