let n be Nat; :: thesis: for a, b, c being Element of (TOP-REAL n) st a - c = b - c holds
a = b
let a, b, c be Element of (TOP-REAL n); :: thesis: ( a - c = b - c implies a = b )
assume a - c = b - c ; :: thesis: a = b
then a + ((- c) + c) = (b - c) + c by RLVECT_1:def 3;
then a + (0. (TOP-REAL n)) = (b - c) + c by RLVECT_1:5;
then a = b + ((- c) + c) by RLVECT_1:def 3;
then a = b + (0. (TOP-REAL n)) by RLVECT_1:5;
hence a = b ; :: thesis: verum