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

( - f in A iff f in X ) ) & ( for f being complex-valued Function holds

( - f in B iff f in X ) ) implies A = B )

assume that

A1: for f being complex-valued Function holds

( - f in A iff f in X ) and

A2: for f being complex-valued Function holds

( - f in B iff f in X ) ; :: thesis: A = B

thus A c= B :: according to XBOOLE_0:def 10 :: thesis: B c= A

assume A5: x in B ; :: thesis: x in A

then reconsider x = x as Element of B ;

A6: - (- x) = x ;

then - x in X by A2, A5;

hence x in A by A1, A6; :: thesis: verum

( - f in A iff f in X ) ) & ( for f being complex-valued Function holds

( - f in B iff f in X ) ) implies A = B )

assume that

A1: for f being complex-valued Function holds

( - f in A iff f in X ) and

A2: for f being complex-valued Function holds

( - f in B iff f in X ) ; :: thesis: A = B

thus A c= B :: according to XBOOLE_0:def 10 :: thesis: B c= A

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B or x in A )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in B )

assume A3: x in A ; :: thesis: x in B

then reconsider x = x as Element of A ;

A4: - (- x) = x ;

then - x in X by A1, A3;

hence x in B by A2, A4; :: thesis: verum

end;assume A3: x in A ; :: thesis: x in B

then reconsider x = x as Element of A ;

A4: - (- x) = x ;

then - x in X by A1, A3;

hence x in B by A2, A4; :: thesis: verum

assume A5: x in B ; :: thesis: x in A

then reconsider x = x as Element of B ;

A6: - (- x) = x ;

then - x in X by A2, A5;

hence x in A by A1, A6; :: thesis: verum