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