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

A1: g <> {} and

A2: g is non-empty and

A3: g (#) c1 = g (#) c2 ; :: thesis: c1 = c2

consider x being object such that

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

g . x in rng g by A4, FUNCT_1:def 3;

then A5: g . x <> {} by A2, RELAT_1:def 9;

( (g (#) c1) . x = (g . x) * c1 & (g (#) c2) . x = (g . x) * c2 ) by VALUED_1:6;

hence c1 = c2 by A3, A5, XCMPLX_1:5; :: thesis: verum

c1 = c2

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

assume that

A1: g <> {} and

A2: g is non-empty and

A3: g (#) c1 = g (#) c2 ; :: thesis: c1 = c2

consider x being object such that

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

g . x in rng g by A4, FUNCT_1:def 3;

then A5: g . x <> {} by A2, RELAT_1:def 9;

( (g (#) c1) . x = (g . x) * c1 & (g (#) c2) . x = (g . x) * c2 ) by VALUED_1:6;

hence c1 = c2 by A3, A5, XCMPLX_1:5; :: thesis: verum