:: deftheorem Def1 defines seq_const SEQ_1:def 1 :
for b being Real holds seq_const b = NAT --> b;