dom (f .. x) = (dom f) /\ (dom x) by Def17
.= I /\ (dom x) by PARTFUN1:def 2
.= I /\ I by PARTFUN1:def 2 ;
hence f .. x is I -defined by RELAT_1:def 18; :: thesis: verum