( ( x in dom f or x nin dom f ) & dom f = I ) by PARTFUN1:def 2;
then ( ( x in I & dom (f . x) = X . x & ( y in X . x or y nin X . x ) ) or ( f . x = {} & dom {} = {} ) ) by Def6, FUNCT_1:def 2;
hence ( (f . x) . y is Function-like & (f . x) . y is Relation-like ) by Def6, FUNCT_1:def 2; :: thesis: verum