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 12;
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:18; :: thesis: verum