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