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