let C be non empty set ; :: thesis: for f being PartFunc of C,COMPLEX holds
( f is total iff - f is total )
let f be PartFunc of C,COMPLEX ; :: thesis: ( f is total iff - f is total )
thus ( f is total implies - f is total ) :: thesis: ( - f is total implies f is total )

proof

assume A1: f is total ; :: thesis: - f is total
- f = (- 1r ) (#) f by COMPLEX1:def 7;
hence - f is total by A1, Th71; :: thesis: verum

end;

assume A2: - f is total ; :: thesis: f is total
- f = (- 1r ) (#) f by COMPLEX1:def 7;
hence f is total by A2, Th71; :: thesis: verum