let r be Real; :: thesis: for n being Nat holds n |-> r is Element of REAL n
let n be Nat; :: thesis: n |-> r is Element of REAL n
A1: r is Element of REAL by XREAL_0:def 1;
set f = n |-> r;
reconsider f = n |-> r as Function ;
f in Funcs ((Seg n),REAL)

proof

f is Element of n -tuples_on REAL by A1, FINSEQ_2:112;
then f in n -tuples_on REAL ;
hence f in Funcs ((Seg n),REAL) by FINSEQ_2:93; :: thesis: verum

end;

hence n |-> r is Element of REAL n by FINSEQ_2:93; :: thesis: verum