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 )
A1: - f = (- 1r) (#) f by COMPLEX1:def 4;
thus ( f is total implies - f is total ) :: thesis: ( - f is total implies f is total )

proof

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

end;

assume - f is total ; :: thesis: f is total
hence f is total by A1, Th71; :: thesis: verum