let C be non empty set ; :: thesis: for f being PartFunc of C,COMPLEX holds
( |.f.| " {0 } = f " {0 } & (- f) " {0 } = f " {0 } )
let f be PartFunc of C,COMPLEX ; :: thesis: ( |.f.| " {0 } = f " {0 } & (- f) " {0 } = f " {0 } )
A1: dom |.f.| = dom f by VALUED_1:def 11;

now

let c be Element of C; :: thesis: ( ( c in |.f.| " {0 } implies c in f " {0c } ) & ( c in f " {0c } implies c in |.f.| " {0 } ) )
thus ( c in |.f.| " {0 } implies c in f " {0c } ) :: thesis: ( c in f " {0c } implies c in |.f.| " {0 } )

proof

assume c in |.f.| " {0 } ; :: thesis: c in f " {0c }
then A2: ( c in dom |.f.| & |.f.| . c in {0 } ) by FUNCT_1:def 13;
then A3: f . c = f /. c by A1, PARTFUN1:def 8;
( c in dom |.f.| & |.f.| . c = 0 ) by A2, TARSKI:def 1;
then ( c in dom |.f.| & |.(f . c).| = 0 ) by VALUED_1:18;
then ( c in dom f & f /. c = 0c ) by A3, COMPLEX1:131, VALUED_1:def 11;
then ( c in dom f & f /. c in {0c } ) by TARSKI:def 1;
hence c in f " {0c } by PARTFUN2:44; :: thesis: verum

end;

assume c in f " {0c } ; :: thesis: c in |.f.| " {0 }
then A4: ( c in dom f & f /. c in {0c } ) by PARTFUN2:44;
then A5: f . c = f /. c by PARTFUN1:def 8;
( c in dom |.f.| & |.(f /. c).| = 0 ) by A4, COMPLEX1:130, TARSKI:def 1, VALUED_1:def 11;
then ( c in dom |.f.| & |.f.| . c = 0 ) by A5, VALUED_1:18;
then ( c in dom |.f.| & |.f.| . c in {0 } ) by TARSKI:def 1;
hence c in |.f.| " {0 } by FUNCT_1:def 13; :: thesis: verum

end;

hence |.f.| " {0 } = f " {0 } by SUBSET_1:8; :: thesis: (- f) " {0 } = f " {0 }

now

let c be Element of C; :: thesis: ( ( c in (- f) " {0c } implies c in f " {0c } ) & ( c in f " {0c } implies c in (- f) " {0c } ) )
thus ( c in (- f) " {0c } implies c in f " {0c } ) :: thesis: ( c in f " {0c } implies c in (- f) " {0c } )

proof

assume c in (- f) " {0c } ; :: thesis: c in f " {0c }
then ( c in dom (- f) & (- f) /. c in {0c } ) by PARTFUN2:44;
then ( c in dom (- f) & (- f) /. c = 0c ) by TARSKI:def 1;
then ( c in dom (- f) & - (- (f /. c)) = - 0c ) by Th9;
then ( c in dom f & f /. c in {0c } ) by Th9, TARSKI:def 1;
hence c in f " {0c } by PARTFUN2:44; :: thesis: verum

end;

assume c in f " {0c } ; :: thesis: c in (- f) " {0c }
then ( c in dom f & f /. c in {0c } ) by PARTFUN2:44;
then ( c in dom (- f) & f /. c = 0c ) by Th9, TARSKI:def 1;
then ( c in dom (- f) & (- f) /. c = - 0c ) by Th9;
then ( c in dom (- f) & (- f) /. c in {0c } ) by TARSKI:def 1;
hence c in (- f) " {0c } by PARTFUN2:44; :: thesis: verum

end;

hence (- f) " {0 } = f " {0 } by SUBSET_1:8; :: thesis: verum