let X, Y be non empty set ; :: thesis: for A, B being Subset of X
for f being Function of X,Y st f .: A misses f .: B holds
A misses B
let A, B be Subset of X; :: thesis: for f being Function of X,Y st f .: A misses f .: B holds
A misses B
let f be Function of X,Y; :: thesis: ( f .: A misses f .: B implies A misses B )
assume A1: (f .: A) /\ (f .: B) = {} ; :: according to XBOOLE_0:def 7 :: thesis: A misses B
assume A /\ B <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
then consider x being Element of X such that
A2: x in A /\ B by SUBSET_1:10;
( x in A & x in B ) by A2, XBOOLE_0:def 4;
then ( f . x in f .: A & f . x in f .: B ) by FUNCT_2:43;
hence contradiction by A1, XBOOLE_0:def 4; :: thesis: verum