let X be set ; :: thesis: for f being Function st X c= dom f & f is one-to-one holds
X,f .: X are_equipotent
let f be Function; :: thesis: ( X c= dom f & f is one-to-one implies X,f .: X are_equipotent )
assume A1: ( X c= dom f & f is one-to-one ) ; :: thesis: X,f .: X are_equipotent
take g = f | X; :: according to WELLORD2:def 4 :: thesis: ( g is one-to-one & dom g = X & rng g = f .: X )
thus g is one-to-one by A1, FUNCT_1:84; :: thesis: ( dom g = X & rng g = f .: X )
thus dom g = X by A1, RELAT_1:91; :: thesis: rng g = f .: X
thus rng g = f .: X by RELAT_1:148; :: thesis: verum