let n be Nat; :: thesis: for f being FinSequence of REAL st dom f = Seg n holds
f is Element of REAL n
A1: n in NAT by ORDINAL1:def 12;
let f be FinSequence of REAL ; :: thesis: ( dom f = Seg n implies f is Element of REAL n )
assume dom f = Seg n ; :: thesis: f is Element of REAL n
then len f = n by A1, FINSEQ_1:def 3;
then f is Element of n -tuples_on REAL by FINSEQ_2:92;
hence f is Element of REAL n by EUCLID:def 1; :: thesis: verum