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 :: thesis: contradiction

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

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