theorem Th23: :: NUMBER03:23

for a, i, k being Nat holds ((Partial_Sums (a GeoSeq)) . k) gcd ((Partial_Sums (a GeoSeq)) . (k + i)) = ((Partial_Sums (a GeoSeq)) . k) gcd (((Partial_Sums (a GeoSeq)) . (k + i)) - ((Partial_Sums (a GeoSeq)) . k))