dom J = I by PARTFUN1:def 2;
then ( J is trivial & i in dom J ) ;
hence proj (J,i) is one-to-one by Th19; :: thesis: verum