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

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