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

( - 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