let X, Y be non empty set ; :: thesis: for A being non empty Subset of X
for x being Element of X st not x in A holds
for f being Function of X,Y st f is one-to-one holds
not f . x in f .: A
let A be non empty Subset of X; :: thesis: for x being Element of X st not x in A holds
for f being Function of X,Y st f is one-to-one holds
not f . x in f .: A
let x be Element of X; :: thesis: ( not x in A implies for f being Function of X,Y st f is one-to-one holds
not f . x in f .: A )
assume A1: not x in A ; :: thesis: for f being Function of X,Y st f is one-to-one holds
not f . x in f .: A
let f be Function of X,Y; :: thesis: ( f is one-to-one implies not f . x in f .: A )
assume A2: f is one-to-one ; :: thesis: not f . x in f .: A
A3: dom f = X by FUNCT_2:def 1;
( f . x in f .: A iff ex a being object st
( a in dom f & a in A & f . x = f . a ) ) by FUNCT_1:def 6;
hence not f . x in f .: A by A2, A3, A1, FUNCT_1:def 4; :: thesis: verum