let p be Point of (TOP-REAL n); :: thesis: p is n -element
A1: p is Function of (Seg n),REAL by Th20;
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:6; :: according to CARD_1:def 7 :: thesis: verum