let V be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for v being Element of V holds v - (0. V) = v
let v be Element of V; :: thesis: v - (0. V) = v
thus v - (0. V) = v + (0. V) by Th25
.= v by Th10 ; :: thesis: verum