let n be Nat; :: thesis: for f being real-valued n -long FinSequence holds f is Element of n -tuples_on REAL
let f be real-valued n -long FinSequence; :: thesis: f is Element of n -tuples_on REAL
A1: f is FinSequence of REAL by Th19;
len f = n by FINSEQ_1:def 18;
hence f is Element of n -tuples_on REAL by A1, FINSEQ_2:110; :: thesis: verum