let V be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for v, u being Element of V ex w being Element of V st v + w = u
let v, u be Element of V; :: thesis: ex w being Element of V st v + w = u
take w = (- v) + u; :: thesis: v + w = u
thus v + w = (v + (- v)) + u by Def3
.= (0. V) + u by Def10
.= u ; :: thesis: verum