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