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

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

(Partial_Product s) . n = n ! )

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

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

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

(Partial_Product s) . n = 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 ! by A1, NEWTON:13 ;

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 = n ! ; :: thesis: verum

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

(Partial_Product s) . n = n ! )

defpred S

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

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

(Partial_Product s) . n = 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 = 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

.= (n !) * (n + 1) by A1, A3, A4

.= (n + 1) ! by NEWTON:15 ;

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

end;assume that

n >= 1 and

A3: (Partial_Product s) . n = 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

.= (n !) * (n + 1) by A1, A3, A4

.= (n + 1) ! by NEWTON:15 ;

hence S

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

.= 1 * (s . 1) by A1

.= 1 ! by A1, NEWTON:13 ;

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 = n ! ; :: thesis: verum