let n be Element of NAT ; :: thesis: for f being FinSequence of REAL st dom f = Seg n holds
f is Element of REAL n
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 FINSEQ_1:def 3;
then f is Element of n -tuples_on REAL by FINSEQ_2:110;
hence f is Element of REAL n by EUCLID:def 1; :: thesis: verum