dom (proj (f,x)) = product f by Def16;
hence proj (f,x) is product f -defined by RELAT_1:def 18; :: thesis: verum