let n be Nat; :: thesis: for f being real-valued n -element FinSequence holds f in REAL n
let f be real-valued n -element 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