let L be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for a, b being Element of L holds (a - b) + b = a

let a, b be Element of L; :: thesis: (a - b) + b = a

thus (a - b) + b = a + ((- b) + b) by RLVECT_1:def 3

.= a + (0. L) by RLVECT_1:5

.= a by RLVECT_1:def 4 ; :: thesis: verum

let a, b be Element of L; :: thesis: (a - b) + b = a

thus (a - b) + b = a + ((- b) + b) by RLVECT_1:def 3

.= a + (0. L) by RLVECT_1:5

.= a by RLVECT_1:def 4 ; :: thesis: verum