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

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