let a, b be Nat; :: thesis: for r being Real holds (r GeoSeq) . (a + b) = ((r GeoSeq) . a) * (r |^ b)
let r be Real; :: thesis: (r GeoSeq) . (a + b) = ((r GeoSeq) . a) * (r |^ b)
set S = r GeoSeq ;
defpred S₁[ Nat] means (r GeoSeq) . (a + $1) = ((r GeoSeq) . a) * (r |^ $1);
A1: S₁[ 0 ]

proof

r |^ 0 = 1 by NEWTON:4;
hence S₁[ 0 ] ; :: thesis: verum

end;

A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
a + (k + 1) = (a + k) + 1 ;
hence (r GeoSeq) . (a + (k + 1)) = ((r GeoSeq) . (a + k)) * (r |^ 1) by PREPOWER:3
.= ((r GeoSeq) . a) * ((r |^ k) * r) by A3
.= ((r GeoSeq) . a) * (r |^ (k + 1)) by NEWTON:6 ;
:: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A2);
hence (r GeoSeq) . (a + b) = ((r GeoSeq) . a) * (r |^ b) ; :: thesis: verum