let C be non empty set ; :: thesis: for c being Element of C
for f being PartFunc of C,COMPLEX st f is total holds
( (- f) /. c = - (f /. c) & |.f.| . c = |.(f /. c).| )
let c be Element of C; :: thesis: for f being PartFunc of C,COMPLEX st f is total holds
( (- f) /. c = - (f /. c) & |.f.| . c = |.(f /. c).| )
let f be PartFunc of C,COMPLEX; :: thesis: ( f is total implies ( (- f) /. c = - (f /. c) & |.f.| . c = |.(f /. c).| ) )
assume A1: f is total ; :: thesis: ( (- f) /. c = - (f /. c) & |.f.| . c = |.(f /. c).| )
then |.f.| is total by Th60;
then A2: ( dom |.f.| = dom f & dom |.f.| = C ) by VALUED_1:def 11;
- f is total by A1, Th59;
then dom (- f) = C ;
hence (- f) /. c = - (f /. c) by Th5; :: thesis: |.f.| . c = |.(f /. c).|
thus |.f.| . c = |.(f . c).| by VALUED_1:18
.= |.(f /. c).| by A2, PARTFUN1:def 6 ; :: thesis: verum