( dom (I --> i) = I & rng (I --> i) c= {i} ) by Th13;
hence I --> i is Function of I,{i} by FUNCT_2:def 1, RELSET_1:4; :: thesis: verum