let n be Nat; :: thesis: for f being real-valued n -long FinSequence holds f in REAL n
let f be real-valued n -long 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 FINSEQ_1:def 18;
hence f in REAL n by A1; :: thesis: verum