let n be 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 Th45;
hence f in the carrier of (TOP-REAL n) by Th8; :: thesis: verum