let r, A be complex-functions-membered set ; :: thesis: ( ( for f being complex-valued Function holds

( - f in r iff f in A ) ) implies for f being complex-valued Function holds

( - f in A iff f in r ) )

assume A7: for f being complex-valued Function holds

( - f in r iff f in A ) ; :: thesis: for f being complex-valued Function holds

( - f in A iff f in r )

let f be complex-valued Function; :: thesis: ( - f in A iff f in r )

assume f in r ; :: thesis: - f in A

then - (- f) in r ;

hence - f in A by A7; :: thesis: verum

( - f in r iff f in A ) ) implies for f being complex-valued Function holds

( - f in A iff f in r ) )

assume A7: for f being complex-valued Function holds

( - f in r iff f in A ) ; :: thesis: for f being complex-valued Function holds

( - f in A iff f in r )

let f be complex-valued Function; :: thesis: ( - f in A iff f in r )

assume f in r ; :: thesis: - f in A

then - (- f) in r ;

hence - f in A by A7; :: thesis: verum