dom g = U1 by FUNCT_2:def 1;
then (f * g) . u = f . (g . u) by FUNCT_1:13;
hence for b₁ being set st b₁ = ((f * g) . u) \+\ (f . (g . u)) holds
b₁ is empty ; :: thesis: verum