let E be RealNormSpace; :: thesis: for a, b being Point of E holds (a + b) - b = a

let a, b be Point of E; :: thesis: (a + b) - b = a

thus (a + b) - b = a + (b - b) by RLVECT_1:28

.= a + (0. E) by RLVECT_1:15

.= a ; :: thesis: verum

let a, b be Point of E; :: thesis: (a + b) - b = a

thus (a + b) - b = a + (b - b) by RLVECT_1:28

.= a + (0. E) by RLVECT_1:15

.= a ; :: thesis: verum