theorem Th20: :: NUMBER03:20

for a, b being Nat
for r being Real holds (r GeoSeq) . (a + b) = ((r GeoSeq) . a) * (r |^ b)