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