let n be Nat; :: thesis: for f being complex-valued Function st f <> 0* n holds
- f <> 0* n
let f be complex-valued Function; :: thesis: ( f <> 0* n implies - f <> 0* n )
assume A1: f <> 0* n ; :: thesis: - f <> 0* n
assume - f = 0* n ; :: thesis: contradiction
then - (- f) = - (0* n) ;
hence contradiction by A1, Th13; :: thesis: verum