let i be natural Number ; :: thesis: for R1 being real-valued i -element FinSequence holds R1 is Element of i -tuples_on REAL
let R1 be real-valued i -element FinSequence; :: thesis: R1 is Element of i -tuples_on REAL
A1: R1 is FinSequence of REAL by Lm2;
len R1 = i by CARD_1:def 7;
hence R1 is Element of i -tuples_on REAL by A1, FINSEQ_2:92; :: thesis: verum