let V be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for v, w being Element of V st ( v + w = v or w + v = v ) holds
w = 0. V
let v, w be Element of V; :: thesis: ( ( v + w = v or w + v = v ) implies w = 0. V )
assume ( v + w = v or w + v = v ) ; :: thesis: w = 0. V
then ( v + w = v + (0. V) or w + v = (0. V) + v ) ;
hence w = 0. V by Th8; :: thesis: verum