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

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