( rng f = X & rng g = X ) by Def3;
then rng (f * g) = X by Th52;
hence for b₁ being PartFunc of X,X st b₁ = f * g holds
b₁ is onto ; :: thesis: verum