let n be Nat; :: thesis: for f being n -element real-valued FinSequence holds f in REAL n
let f be n -element real-valued FinSequence; :: thesis: f in REAL n
rng f c= REAL ;
then f is FinSequence of REAL by FINSEQ_1:def 4;
then A1: f is Element of REAL * by FINSEQ_1:def 11;
len f = n by CARD_1:def 7;
hence f in REAL n by A1; :: thesis: verum