let X, Y, Z be set ; ( 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 )
; WELLORD2:def 4 ( 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 )
; WELLORD2:def 4 X,Z are_equipotent
take
g * f
; WELLORD2:def 4 ( 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; verum