let a be Real; :: thesis: for s being Real_Sequence st ( for n being Nat st n >= 1 holds

( s . n = a & s . 0 = 1 ) ) holds

for n being Nat st n >= 1 holds

(Partial_Product s) . n = a |^ n

let s be Real_Sequence; :: thesis: ( ( for n being Nat st n >= 1 holds

( s . n = a & s . 0 = 1 ) ) implies for n being Nat st n >= 1 holds

(Partial_Product s) . n = a |^ n )

defpred S_{1}[ Nat] means (Partial_Product s) . $1 = a |^ $1;

assume A1: for n being Nat st n >= 1 holds

( s . n = a & s . 0 = 1 ) ; :: thesis: for n being Nat st n >= 1 holds

(Partial_Product s) . n = a |^ n

A2: for n being Nat st n >= 1 & S_{1}[n] holds

S_{1}[n + 1]

.= (s . 0) * (s . (1 + 0)) by SERIES_3:def 1

.= 1 * (s . 1) by A1

.= 1 * a by A1

.= a |^ 1 ;

then A5: S_{1}[1]
;

for n being Nat st n >= 1 holds

S_{1}[n]
from NAT_1:sch 8(A5, A2);

hence for n being Nat st n >= 1 holds

(Partial_Product s) . n = a |^ n ; :: thesis: verum

( s . n = a & s . 0 = 1 ) ) holds

for n being Nat st n >= 1 holds

(Partial_Product s) . n = a |^ n

let s be Real_Sequence; :: thesis: ( ( for n being Nat st n >= 1 holds

( s . n = a & s . 0 = 1 ) ) implies for n being Nat st n >= 1 holds

(Partial_Product s) . n = a |^ n )

defpred S

assume A1: for n being Nat st n >= 1 holds

( s . n = a & s . 0 = 1 ) ; :: thesis: for n being Nat st n >= 1 holds

(Partial_Product s) . n = a |^ n

A2: for n being Nat st n >= 1 & S

S

proof

(Partial_Product s) . (1 + 0) =
((Partial_Product s) . 0) * (s . (1 + 0))
by SERIES_3:def 1
let n be Nat; :: thesis: ( n >= 1 & S_{1}[n] implies S_{1}[n + 1] )

assume that

n >= 1 and

A3: (Partial_Product s) . n = a |^ n ; :: thesis: S_{1}[n + 1]

A4: n + 1 >= 1 by NAT_1:11;

(Partial_Product s) . (n + 1) = ((Partial_Product s) . n) * (s . (n + 1)) by SERIES_3:def 1

.= (a |^ n) * a by A1, A3, A4

.= a |^ (n + 1) by NEWTON:6 ;

hence S_{1}[n + 1]
; :: thesis: verum

end;assume that

n >= 1 and

A3: (Partial_Product s) . n = a |^ n ; :: thesis: S

A4: n + 1 >= 1 by NAT_1:11;

(Partial_Product s) . (n + 1) = ((Partial_Product s) . n) * (s . (n + 1)) by SERIES_3:def 1

.= (a |^ n) * a by A1, A3, A4

.= a |^ (n + 1) by NEWTON:6 ;

hence S

.= (s . 0) * (s . (1 + 0)) by SERIES_3:def 1

.= 1 * (s . 1) by A1

.= 1 * a by A1

.= a |^ 1 ;

then A5: S

for n being Nat st n >= 1 holds

S

hence for n being Nat st n >= 1 holds

(Partial_Product s) . n = a |^ n ; :: thesis: verum