let p be Point of (TOP-REAL n); :: thesis: p is n -long
A1: p is Function of (Seg n),REAL by Th26;
Seg (len p) = dom p by FINSEQ_1:def 3
.= Seg n by A1, FUNCT_2:def 1 ;
hence len p = n by FINSEQ_1:8; :: according to FINSEQ_1:def 18 :: thesis: verum