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 :: thesis: for c being Element of C holds
( ( c in |.f.| " {0} implies c in f " {0c} ) & ( c in f " {0c} implies c in |.f.| " {0} ) )
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 A2: c in |.f.| " {0} ; :: thesis: c in f " {0c}
then c in dom |.f.| by FUNCT_1:def 7;
then A3: c in dom f by VALUED_1:def 11;
|.f.| . c in {0} by A2, FUNCT_1:def 7;
then |.f.| . c = 0 by TARSKI:def 1;
then A4: |.(f . c).| = 0 by VALUED_1:18;
c in dom |.f.| by A2, FUNCT_1:def 7;
then f . c = f /. c by A1, PARTFUN1:def 6;
then f /. c = 0c by A4, COMPLEX1:45;
then f /. c in {0c} by TARSKI:def 1;
hence c in f " {0c} by A3, PARTFUN2:26; :: thesis: verum
end;
assume A5: c in f " {0c} ; :: thesis: c in |.f.| " {0}
then f /. c in {0c} by PARTFUN2:26;
then A6: |.(f /. c).| = 0 by COMPLEX1:44, TARSKI:def 1;
A7: c in dom f by A5, PARTFUN2:26;
then f . c = f /. c by PARTFUN1:def 6;
then |.f.| . c = 0 by A6, VALUED_1:18;
then A8: |.f.| . c in {0} by TARSKI:def 1;
c in dom |.f.| by A7, VALUED_1:def 11;
hence c in |.f.| " {0} by A8, FUNCT_1:def 7; :: thesis: verum
end;
hence |.f.| " {0} = f " {0} by SUBSET_1:3; :: thesis: (- f) " {0} = f " {0}
now :: thesis: for c being Element of C holds
( ( c in (- f) " {0c} implies c in f " {0c} ) & ( c in f " {0c} implies c in (- f) " {0c} ) )
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 A9: c in (- f) " {0c} ; :: thesis: c in f " {0c}
then A10: c in dom (- f) by PARTFUN2:26;
(- f) /. c in {0c} by A9, PARTFUN2:26;
then (- f) /. c = 0c by TARSKI:def 1;
then - (- (f /. c)) = - 0c by A10, Th5;
then A11: f /. c in {0c} by TARSKI:def 1;
c in dom f by A10, Th5;
hence c in f " {0c} by A11, PARTFUN2:26; :: thesis: verum
end;
assume A12: c in f " {0c} ; :: thesis: c in (- f) " {0c}
then f /. c in {0c} by PARTFUN2:26;
then A13: f /. c = 0c by TARSKI:def 1;
A14: c in dom f by A12, PARTFUN2:26;
then c in dom (- f) by Th5;
then (- f) /. c = - 0c by A13, Th5;
then A15: (- f) /. c in {0c} by TARSKI:def 1;
c in dom (- f) by A14, Th5;
hence c in (- f) " {0c} by A15, PARTFUN2:26; :: thesis: verum
end;
hence (- f) " {0} = f " {0} by SUBSET_1:3; :: thesis: verum