let X be set ; :: thesis: for f being Function st f is one-to-one & X c= dom f holds
card (f .: X) = card X
let f be Function; :: thesis: ( f is one-to-one & X c= dom f implies card (f .: X) = card X )
assume ( f is one-to-one & X c= dom f ) ; :: thesis: card (f .: X) = card X
then ( card (f .: X) c= card X & card X c= card (f .: X) ) by Th3, CARD_1:67;
hence card (f .: X) = card X by XBOOLE_0:def 10; :: thesis: verum