theorem Th36: :: UPROOTS:39

for L being non degenerated comRing
for x being Element of L
for i being Nat holds len (<%x,(1. L)%> `^ i) = i + 1