let a, m, n be Nat; :: thesis: ( n + 1,m + 1 are_coprime implies (Partial_Sums (a GeoSeq)) . n,(Partial_Sums (a GeoSeq)) . m are_coprime )
assume A1: n + 1,m + 1 are_coprime ; :: thesis: (Partial_Sums (a GeoSeq)) . n,(Partial_Sums (a GeoSeq)) . m are_coprime
A2: (Partial_Sums (a GeoSeq)) . 0 = (a GeoSeq) . 0 by SERIES_1:def 1
.= 1 by PREPOWER:3 ;
( n + 1 <> m + 1 or ( n + 1 = m + 1 & m + 1 = 1 ) ) by A1, Th14;

per cases then ( n < m or m < n or ( n = m & m = 0 ) ) by XXREAL_0:1;

suppose ( n < m or m < n ) ; :: thesis: (Partial_Sums (a GeoSeq)) . n,(Partial_Sums (a GeoSeq)) . m are_coprime

hence (Partial_Sums (a GeoSeq)) . n,(Partial_Sums (a GeoSeq)) . m are_coprime by A1, Lm31; :: thesis: verum

end;

suppose ( n = m & m = 0 ) ; :: thesis: (Partial_Sums (a GeoSeq)) . n,(Partial_Sums (a GeoSeq)) . m are_coprime

hence (Partial_Sums (a GeoSeq)) . n,(Partial_Sums (a GeoSeq)) . m are_coprime by A2, NAT_D:32; :: thesis: verum

end;

end;