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_{1}[ Nat] means s1 . $1 = (a GeoSeq) . $1;

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_{1}[m] holds

S_{1}[m + 1]

.= (a GeoSeq) . 0 by Def1 ;

then A6: S_{1}[ 0 ]
;

for m being Nat holds S_{1}[m]
from NAT_1:sch 2(A6, A4);

then for m being Element of NAT holds S_{1}[m]
;

hence s1 = a GeoSeq by FUNCT_2:63; :: thesis: verum

( 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

hereby :: thesis: ( s1 . 0 = 1 & ( for m being Nat holds s1 . (m + 1) = (s1 . m) * a ) implies s1 = a GeoSeq )

assume that 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;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

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

S

proof

s1 . 0 =
a |^ 0
by A2, NEWTON:4
let m be Nat; :: thesis: ( S_{1}[m] implies S_{1}[m + 1] )

assume A5: s1 . m = (a GeoSeq) . m ; :: thesis: S_{1}[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;assume A5: s1 . m = (a GeoSeq) . m ; :: thesis: S

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

.= (a GeoSeq) . 0 by Def1 ;

then A6: S

for m being Nat holds S

then for m being Element of NAT holds S

hence s1 = a GeoSeq by FUNCT_2:63; :: thesis: verum