let X, Y, Z be set ; :: thesis: ( X,Y are_equipotent & Y,Z are_equipotent implies X,Z are_equipotent )
given f being Function such that A1: ( f is one-to-one & dom f = X & rng f = Y ) ; :: according to WELLORD2:def 4 :: thesis: ( not Y,Z are_equipotent or X,Z are_equipotent )
given g being Function such that A2: ( g is one-to-one & dom g = Y & rng g = Z ) ; :: according to WELLORD2:def 4 :: thesis: X,Z are_equipotent
take g * f ; :: according to WELLORD2:def 4 :: thesis: ( g * f is one-to-one & dom (g * f) = X & rng (g * f) = Z )
thus ( g * f is one-to-one & dom (g * f) = X & rng (g * f) = Z ) by A1, A2, RELAT_1:27, RELAT_1:28; :: thesis: verum