let C be non empty set ; :: thesis: for c being Element of C
for f being PartFunc of C,COMPLEX st c in dom (f ^ ) holds
f /. c <> 0
let c be Element of C; :: thesis: for f being PartFunc of C,COMPLEX st c in dom (f ^ ) holds
f /. c <> 0
let f be PartFunc of C,COMPLEX ; :: 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 " {0c }) by A1, Def2;
then A4: not c in f " {0c } by XBOOLE_0:def 5;

now

per cases ( not c in dom f or not f /. c in {0c } ) by A4, PARTFUN2:44;

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

hence contradiction by A3, XBOOLE_0:def 5; :: thesis: verum

end;

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

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

end;

end;

end;

hence contradiction ; :: thesis: verum