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
proof
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;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B or x in 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