let n be Element of NAT ; :: thesis: for f being FinSequence of REAL st len f = n holds
f in the carrier of (TOP-REAL n)
let f be FinSequence of REAL ; :: thesis: ( len f = n implies f in the carrier of (TOP-REAL n) )
assume len f = n ; :: thesis: f in the carrier of (TOP-REAL n)
then f in the carrier of (Euclid n) by Th17;
hence f in the carrier of (TOP-REAL n) by TOPREAL3:8; :: thesis: verum