theorem :: REALSET2:25

for F being Field
for a, b, c being Element of F st a + b = a + c holds
b = c by RLVECT_1:8;