let C be non empty set ; :: thesis: for c being Element of C
for f being complex-valued Function st c in dom (f ^ ) holds
f . c <> 0
let c be Element of C; :: thesis: for f being complex-valued Function st c in dom (f ^ ) holds
f . c <> 0
let f be complex-valued Function; :: thesis: ( c in dom (f ^ ) implies f . c <> 0 )
assume that
A1: c in dom (f ^ ) and
A2: f . c = 0 ; :: thesis: contradiction
A3: c in (dom f) \ (f " {0 }) by A1, Def8;
then A4: ( c in dom f & not c in f " {0 } ) by XBOOLE_0:def 5;

now

per cases ( not c in dom f or not f . c in {0 } ) by A4, FUNCT_1:def 13;

suppose not c in dom f ; :: thesis: contradiction

hence contradiction by A3; :: thesis: verum

end;

suppose not f . c in {0 } ; :: thesis: contradiction

hence contradiction by A2, TARSKI:def 1; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum