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