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 Th72;
then dom (- f) = C by PARTFUN1:def 4;
hence (- f) /. c = - (f /. c) by Th9; :: thesis: |.f.| . c = |.(f /. c).|
A2: dom |.f.| = dom f by VALUED_1:def 11;
|.f.| is total by A1, Th73;
then A3: dom |.f.| = C by PARTFUN1:def 4;
thus |.f.| . c = |.(f . c).| by VALUED_1:18
.= |.(f /. c).| by A2, A3, PARTFUN1:def 8 ; :: thesis: verum