let c1, c2 be complex number ; :: thesis: for g being complex-valued Function st g <> {} & g - c1 = g - c2 holds
c1 = c2
let g be complex-valued Function; :: thesis: ( g <> {} & g - c1 = g - c2 implies c1 = c2 )
assume that
A2: g <> {} and
A0: g - c1 = g - c2 ; :: thesis: c1 = c2
consider x being set such that
A1: x in dom g by A2, XBOOLE_0:def 1;
( dom g = dom (g - c1) & dom g = dom (g - c2) ) by VALUED_1:def 2;
then ( (g - c1) . x = (g . x) - c1 & (g - c2) . x = (g . x) - c2 ) by A1, VALUED_1:def 2;
hence c1 = c2 by A0; :: thesis: verum