let c be Complex; :: thesis: for f, g being complex-valued Function st c (#) f = c (#) g & c <> 0 holds
f = g
let f, g be complex-valued Function; :: thesis: ( c (#) f = c (#) g & c <> 0 implies f = g )
assume A1: c (#) f = c (#) g ; :: thesis: ( not c <> 0 or f = g )
assume c <> 0 ; :: thesis: f = g
then A2: (1 / c) * c = 1 by XCMPLX_1:106;
( ((1 / c) * c) (#) f = (1 / c) (#) (c (#) f) & ((1 / c) * c) (#) g = (1 / c) (#) (c (#) g) ) by CFUNCT_1:22;
then 1 (#) f = 1 (#) g by A1, A2;
hence f = g ; :: thesis: verum