let X be set ; :: thesis: for f being Function st X c= dom f & f is one-to-one holds
f " (f .: X) = X
let f be Function; :: thesis: ( X c= dom f & f is one-to-one implies f " (f .: X) = X )
assume that
A1: X c= dom f and
A2: f is one-to-one ; :: thesis: f " (f .: X) = X
thus f " (f .: X) c= X by A2, Th81; :: according to XBOOLE_0:def 10 :: thesis: X c= f " (f .: X)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in f " (f .: X) )
assume A3: x in X ; :: thesis: x in f " (f .: X)
then f . x in f .: X by A1, Def6;
hence x in f " (f .: X) by A1, A3, Def7; :: thesis: verum