( dom (Frege u) = product (doms u) & doms u = a & product (rngs u) c= product a & rng (Frege u) = product (rngs u) ) by Th22, FUNCT_6:58, FUNCT_6:def 7;
hence Frege u is UnOp of (product a) by FUNCT_2:def 1, RELSET_1:11; :: thesis: verum