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

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