let c1, c2 be complex number ; :: thesis: for g being complex-valued Function st g <> {} & g is non-empty & g (/) c1 = g (/) c2 holds
c1 = c2
let g be complex-valued Function; :: thesis: ( g <> {} & g is non-empty & g (/) c1 = g (/) c2 implies c1 = c2 )
assume that
A2: g <> {} and
A4: g is non-empty 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;
g . x in rng g by A1, FUNCT_1:def 5;
then A3: g . x <> {} by A4, RELAT_1:def 9;
( (g (/) c1) . x = (g . x) / c1 & (g (/) c2) . x = (g . x) / c2 ) by VALUED_1:6;
then c1 " = c2 " by A0, A3, XCMPLX_1:5;
hence c1 = c2 by XCMPLX_1:202; :: thesis: verum