(seq_const a) . 1 = a by SEQ_1:57;
hence lim (seq_const a) = a by SEQ_4:25; :: thesis: verum