let i, j be Element of NAT ; :: thesis: for t being Element of i -tuples_on REAL st j in Seg i holds
t . j is Real
let t be Element of i -tuples_on REAL ; :: thesis: ( j in Seg i implies t . j is Real )
len t = i by FINSEQ_1:def 18;
then A1: Seg i = dom t by FINSEQ_1:def 3;
assume j in Seg i ; :: thesis: t . j is Real
hence t . j is Real by A1, FINSEQ_2:13; :: thesis: verum