let n be Nat; :: thesis: ( n <> 0 implies for p, m being Integer st p divides m holds
p divides (m GeoSeq) . n )
assume A1: n <> 0 ; :: thesis: for p, m being Integer st p divides m holds
p divides (m GeoSeq) . n
let p, m be Integer; :: thesis: ( p divides m implies p divides (m GeoSeq) . n )
assume A2: p divides m ; :: thesis: p divides (m GeoSeq) . n
set G = m GeoSeq ;
defpred S₁[ Nat] means ( $1 <> 0 implies p divides (m GeoSeq) . $1 );
A3: (m GeoSeq) . 0 = 1 by PREPOWER:3;
(m GeoSeq) . (0 + 1) = ((m GeoSeq) . 0) * m by PREPOWER:3;
then A4: S₁[1] by A2, A3;
A5: for k being non zero Nat st S₁[k] holds
S₁[k + 1]

proof

let k be non zero Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
(m GeoSeq) . (k + 1) = ((m GeoSeq) . k) * m by PREPOWER:3;
hence ( S₁[k] implies S₁[k + 1] ) by INT_2:2; :: thesis: verum

end;

for k being non zero Nat holds S₁[k] from NAT_1:sch 10(A4, A5);
hence p divides (m GeoSeq) . n by A1; :: thesis: verum