for r being Real
for n being Nat holds n |-> r is Element of REAL n