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 that
A1: X c= dom f and
A2: 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 & proj1 g = X & proj2 g = f .: X )
thus g is one-to-one by A2, FUNCT_1:52; :: thesis: ( proj1 g = X & proj2 g = f .: X )
thus dom g = X by A1, RELAT_1:62; :: thesis: proj2 g = f .: X
thus proj2 g = f .: X by RELAT_1:115; :: thesis: verum