let g be Element of (product F); :: thesis: ( g is I -defined & g is Relation-like & g is Function-like )
dom g = I by GROUP_19:3;
hence ( g is I -defined & g is Relation-like & g is Function-like ) by RELAT_1:def 18; :: thesis: verum