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

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 )

{ (- f) where f is Element of X : f in X } is complex-functions-membered

proof

then reconsider F = { (- f) where f is Element of X : f in X } as complex-functions-membered set ;
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;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

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 )

thus
( f in X implies - f in F )
; :: thesis: verumassume
- 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;then ex g being Element of X st

( - f = - g & g in X ) ;

hence f in X by RVSUM_1:24; :: thesis: verum