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 S₁[ Nat] means s1 . $1 = (a GeoSeq) . $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 A1, Def1
.= (a |^ m) * a by NEWTON:6
.= (s1 . m) * a by A1, Def1 ; :: 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 S₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A5: s1 . m = (a GeoSeq) . m ; :: thesis: S₁[m + 1]
thus s1 . (m + 1) = (s1 . m) * a by A3
.= (a |^ m) * a by A5, Def1
.= a |^ (m + 1) by NEWTON:6
.= (a GeoSeq) . (m + 1) by Def1 ; :: thesis: verum

end;

s1 . 0 = a |^ 0 by A2, NEWTON:4
.= (a GeoSeq) . 0 by Def1 ;
then A6: S₁[ 0 ] ;
for m being Nat holds S₁[m] from NAT_1:sch 2(A6, A4);
then for m being Element of NAT holds S₁[m] ;
hence s1 = a GeoSeq by FUNCT_2:63; :: thesis: verum