dom (rngs F) = dom F by FUNCT_6:90
.= I by PARTFUN1:def 4 ;
hence rngs F is I -defined by RELAT_1:def 18; :: thesis: verum