dom (proj f,x) = product f by Def17;
hence proj f,x is total by PARTFUN1:def 4; :: thesis: verum