let M be non empty set ; :: thesis: for V being ComplexNormSpace
for f being PartFunc of M,V holds
( f is total iff - f is total )
let V be ComplexNormSpace; :: thesis: for f being PartFunc of M,V holds
( f is total iff - f is total )
let f be PartFunc of M,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 )
proof
assume A1: f is total ; :: thesis: - f is total
- f = (- 1r) (#) f by Th23;
hence - f is total by A1, Th34; :: thesis: verum
end;
assume A2: - f is total ; :: thesis: f is total
- f = (- 1r) (#) f by Th23;
hence f is total by A2, Th34; :: thesis: verum