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