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