let V be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: Sum <*(0. V),(0. V),(0. V)*> = 0. V
thus Sum <*(0. V),(0. V),(0. V)*> = ((0. V) + (0. V)) + (0. V) by Th63
.= (0. V) + (0. V) by Th10
.= 0. V by Th10 ; :: thesis: verum