let X be complex-functions-membered set ; :: thesis: for f being complex-valued Function holds
( - f in X iff f in (-) X )
let f be complex-valued Function; :: thesis: ( - f in X iff f in (-) X )
( - (- f) = f & (-) ((-) X) = X ) ;
hence ( - f in X iff f in (-) X ) by Def3; :: thesis: verum