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, Def2;

then A4: not c in f " {0} by XBOOLE_0:def 5;

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, Def2;

then A4: not c in f " {0} by XBOOLE_0:def 5;

now :: thesis: contradiction

hence
contradiction
; :: thesis: verumend;