rng (seq_const b) = {b} by FUNCOP_1:8;
hence not 0 in rng (seq_const b) by TARSKI:def 1; :: according to ORDINAL1:def 15 :: thesis: verum