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