let a, i, k be Nat; :: thesis: ((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))
set P = Partial_Sums (a GeoSeq);
reconsider N = ((Partial_Sums (a GeoSeq)) . (k + i)) - ((Partial_Sums (a GeoSeq)) . k) as Element of NAT by INT_1:5, SEQM_3:5;
(Partial_Sums (a GeoSeq)) . (k + i) = ((Partial_Sums (a GeoSeq)) . k) + N ;
hence ((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)) by FIB_NUM:1; :: thesis: verum