theorem Th10: :: HILB10_2:10

for n being Nat
for L being non empty ZeroStr
for p being Series of n,L holds {(0. L)} \/ (rng p) = rng (p extended_by_0)