set F = { (- f) where f is Element of X : f in X } ;
{ (- f) where f is Element of X : f in X } is complex-functions-membered
proof
let x be object ; :: according to VALUED_2:def 2 :: thesis: ( not x in { (- f) where f is Element of X : f in X } or x is set )
assume x in { (- f) where f is Element of X : f in X } ; :: thesis: x is set
then ex f being Element of X st
( x = - f & f in X ) ;
hence x is set ; :: thesis: verum
end;
then reconsider F = { (- f) where f is Element of X : f in X } as complex-functions-membered set ;
take F ; :: thesis: for f being complex-valued Function holds
( - f in F iff f in X )
let f be complex-valued Function; :: thesis: ( - f in F iff f in X )
hereby :: thesis: ( f in X implies - f in F )
assume - f in F ; :: thesis: f in X
then ex g being Element of X st
( - f = - g & g in X ) ;
hence f in X by RVSUM_1:24; :: thesis: verum
end;
thus ( f in X implies - f in F ) ; :: thesis: verum