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