( rng O c= J & dom O = I & dom F = J ) by PARTFUN1:def 4, FUNCT_2:def 1, RELAT_1:def 19;
then dom (F * O) = I by RELAT_1:46;
hence for b₁ being I -defined Function st b₁ = F * O holds
b₁ is total by PARTFUN1:def 4; :: thesis: verum