theorem Th3: :: PREPOWER:3

for a being Real
for s1 being Real_Sequence holds
( s1 = a GeoSeq iff ( s1 . 0 = 1 & ( for m being Nat holds s1 . (m + 1) = (s1 . m) * a ) ) )