rng (proj (J,i)) = the carrier of (J . i) by Th52;
hence ( proj (J,i) is continuous & proj (J,i) is onto ) by WAYBEL18:5, FUNCT_2:def 3; :: thesis: verum