( dom x = I & rng x c= UN ) by PARTFUN1:def 2;
hence product x is Element of UN by YELLOW_6:1; :: thesis: verum