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 )
hereby :: thesis: ( f in r implies - f in A )
assume - f in A ; :: thesis: f in r
then - (- f) in r by A7;
hence f in r ; :: thesis: verum
end;
assume f in r ; :: thesis: - f in A
then - (- f) in r ;
hence - f in A by A7; :: thesis: verum