let n be Nat; :: thesis: for f being n -element real-valued FinSequence holds f is Element of n -tuples_on REAL
let f be n -element real-valued FinSequence; :: thesis: f is Element of n -tuples_on REAL
A1: f is FinSequence of REAL by RVSUM_1:145;
len f = n by CARD_1:def 7;
hence f is Element of n -tuples_on REAL by A1, FINSEQ_2:92; :: thesis: verum