let c1, c2 be Complex; :: 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

A1: g <> {} and

A2: g - c1 = g - c2 ; :: thesis: c1 = c2

consider x being object such that

A3: x in dom g by A1, XBOOLE_0:def 1;

dom g = dom (g - c2) by VALUED_1:def 2;

then A4: (g - c2) . x = (g . x) - c2 by A3, VALUED_1:def 2;

dom g = dom (g - c1) by VALUED_1:def 2;

then (g - c1) . x = (g . x) - c1 by A3, VALUED_1:def 2;

hence c1 = c2 by A2, A4; :: thesis: verum

c1 = c2

let g be complex-valued Function; :: thesis: ( g <> {} & g - c1 = g - c2 implies c1 = c2 )

assume that

A1: g <> {} and

A2: g - c1 = g - c2 ; :: thesis: c1 = c2

consider x being object such that

A3: x in dom g by A1, XBOOLE_0:def 1;

dom g = dom (g - c2) by VALUED_1:def 2;

then A4: (g - c2) . x = (g . x) - c2 by A3, VALUED_1:def 2;

dom g = dom (g - c1) by VALUED_1:def 2;

then (g - c1) . x = (g . x) - c1 by A3, VALUED_1:def 2;

hence c1 = c2 by A2, A4; :: thesis: verum