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

.= 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