( rng O c= J & dom O = I & dom F = J ) by Def3, FUNCT_2:def 1, RELSET_1:12;
hence dom (F * O) = I by RELAT_1:46; :: according to PBOOLE:def 3 :: thesis: verum