let V be right_complementable add-associative right_zeroed addLoopStr ; :: thesis: V is right_add-cancelable
let v be Element of V; :: according to ALGSTR_0:def 7 :: thesis: v is right_add-cancelable
consider v1 being Element of V such that
A1: v + v1 = 0. V by ALGSTR_0:def 11;
let u, w be Element of V; :: according to ALGSTR_0:def 4 :: thesis: ( not u + v = w + v or u = w )
assume A2: u + v = w + v ; :: thesis: u = w
thus u = u + (0. V) by Def4
.= (u + v) + v1 by A1, Def3
.= w + (0. V) by A1, A2, Def3
.= w by Def4 ; :: thesis: verum