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

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