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