let n, m be Nat; :: thesis: ( n in Seg m implies PROJ m,n is continuous )
assume A1: n in Seg m ; :: thesis: PROJ m,n is continuous
A2: m in NAT by ORDINAL1:def 13;
for p being Element of (TOP-REAL m) holds (PROJ m,n) . p = p /. n by Def6;
hence PROJ m,n is continuous by A2, A1, JORDAN2B:22; :: thesis: verum