let C be non empty set ; :: thesis: for V being RealNormSpace
for f being PartFunc of C,V holds
( f is total iff - f is total )
let V be RealNormSpace; :: thesis: for f being PartFunc of C,V holds
( f is total iff - f is total )
let f be PartFunc of C,V; :: thesis: ( f is total iff - f is total )
thus ( f is total implies - f is total ) ; :: thesis: ( - f is total implies f is total )
assume A1: - f is total ; :: thesis: f is total
- f = (- 1) (#) f by Th23;
hence f is total by A1, Def4; :: thesis: verum