let a be Real; :: thesis: for s1 being Real_Sequence holds
( s1 = a GeoSeq iff ( s1 . 0 = 1 & ( for m being Nat holds s1 . (m + 1) = (s1 . m) * a ) ) )

let s1 be Real_Sequence; :: thesis: ( s1 = a GeoSeq iff ( s1 . 0 = 1 & ( for m being Nat holds s1 . (m + 1) = (s1 . m) * a ) ) )
defpred S1[ Nat] means s1 . \$1 = () . \$1;
hereby :: thesis: ( s1 . 0 = 1 & ( for m being Nat holds s1 . (m + 1) = (s1 . m) * a ) implies s1 = a GeoSeq )
assume A1: s1 = a GeoSeq ; :: thesis: ( s1 . 0 = 1 & ( for m being Nat holds s1 . (m + 1) = (s1 . m) * a ) )
hence s1 . 0 = a |^ 0 by Def1
.= 1 by NEWTON:4 ;
:: thesis: for m being Nat holds s1 . (m + 1) = (s1 . m) * a
let m be Nat; :: thesis: s1 . (m + 1) = (s1 . m) * a
thus s1 . (m + 1) = a |^ (m + 1) by
.= (a |^ m) * a by NEWTON:6
.= (s1 . m) * a by ; :: thesis: verum
end;
assume that
A2: s1 . 0 = 1 and
A3: for m being Nat holds s1 . (m + 1) = (s1 . m) * a ; :: thesis: s1 = a GeoSeq
A4: for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be Nat; :: thesis: ( S1[m] implies S1[m + 1] )
assume A5: s1 . m = () . m ; :: thesis: S1[m + 1]
thus s1 . (m + 1) = (s1 . m) * a by A3
.= (a |^ m) * a by
.= a |^ (m + 1) by NEWTON:6
.= () . (m + 1) by Def1 ; :: thesis: verum
end;
s1 . 0 = a |^ 0 by
.= () . 0 by Def1 ;
then A6: S1[ 0 ] ;
for m being Nat holds S1[m] from NAT_1:sch 2(A6, A4);
then for m being Element of NAT holds S1[m] ;
hence s1 = a GeoSeq by FUNCT_2:63; :: thesis: verum