theorem :: SEQ_1:57

for a being Real
for k being Nat holds (seq_const a) . k = a by ORDINAL1:def 12, FUNCOP_1:7;