let G be AbGroup; :: thesis: for a, b, c being Element of G holds

( - (a - b) = (- a) - (- b) & (a - b) + c = (a + c) - b )

let a, b, c be Element of G; :: thesis: ( - (a - b) = (- a) - (- b) & (a - b) + c = (a + c) - b )

thus - (a - b) = (- a) + b by VECTSP_1:17

.= (- a) - (- b) by RLVECT_1:17 ; :: thesis: (a - b) + c = (a + c) - b

thus (a - b) + c = (a + c) - b by RLVECT_1:def 3; :: thesis: verum

( - (a - b) = (- a) - (- b) & (a - b) + c = (a + c) - b )

let a, b, c be Element of G; :: thesis: ( - (a - b) = (- a) - (- b) & (a - b) + c = (a + c) - b )

thus - (a - b) = (- a) + b by VECTSP_1:17

.= (- a) - (- b) by RLVECT_1:17 ; :: thesis: (a - b) + c = (a + c) - b

thus (a - b) + c = (a + c) - b by RLVECT_1:def 3; :: thesis: verum