let K be Nat; :: thesis: for n being Nat ex Z being Nat st

( Product (1 + (K * (idseq n))) = 1 + (K * Z) & ( n > 0 implies Z > 0 ) )

defpred S_{1}[ Nat] means ex Z being Nat st

( Product (1 + (K * (idseq $1))) = 1 + (K * Z) & ( $1 > 0 implies Z > 0 ) );

reconsider Z = 0 as Nat ;

Product (1 + (K * (idseq Z))) = 1 + (K * 0) by RVSUM_1:94;

then A1: S_{1}[ 0 ]
;

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

S_{1}[n + 1]
_{1}[n]
from NAT_1:sch 2(A1, A2);

hence for n being Nat ex Z being Nat st

( Product (1 + (K * (idseq n))) = 1 + (K * Z) & ( n > 0 implies Z > 0 ) ) ; :: thesis: verum

( Product (1 + (K * (idseq n))) = 1 + (K * Z) & ( n > 0 implies Z > 0 ) )

defpred S

( Product (1 + (K * (idseq $1))) = 1 + (K * Z) & ( $1 > 0 implies Z > 0 ) );

reconsider Z = 0 as Nat ;

Product (1 + (K * (idseq Z))) = 1 + (K * 0) by RVSUM_1:94;

then A1: S

A2: for n being Nat st S

S

proof

for n being Nat holds S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume S_{1}[n]
; :: thesis: S_{1}[n + 1]

then consider Z being Nat such that

A3: ( Product (1 + (K * (idseq n))) = 1 + (K * Z) & ( n > 0 implies Z > 0 ) ) ;

set n1 = n + 1;

A4: 1 + (K * <*(n + 1)*>) = 1 + <*(K * (n + 1))*> by RVSUM_1:47

.= <*(1 + (K * (n + 1)))*> by BASEL_1:2 ;

idseq (n + 1) = (idseq n) ^ <*(n + 1)*> by FINSEQ_2:51;

then K * (idseq (n + 1)) = (K * (idseq n)) ^ (K * <*(n + 1)*>) by NEWTON04:43;

then 1 + (K * (idseq (n + 1))) = (1 + (K * (idseq n))) ^ (1 + (K * <*(n + 1)*>)) by BASEL_1:3;

then Product (1 + (K * (idseq (n + 1)))) = (Product (1 + (K * (idseq n)))) * (1 + (K * (n + 1))) by A4, RVSUM_1:96;

then Product (1 + (K * (idseq (n + 1)))) = 1 + (K * ((Z + (n + 1)) + ((K * Z) * (n + 1)))) by A3;

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

end;assume S

then consider Z being Nat such that

A3: ( Product (1 + (K * (idseq n))) = 1 + (K * Z) & ( n > 0 implies Z > 0 ) ) ;

set n1 = n + 1;

A4: 1 + (K * <*(n + 1)*>) = 1 + <*(K * (n + 1))*> by RVSUM_1:47

.= <*(1 + (K * (n + 1)))*> by BASEL_1:2 ;

idseq (n + 1) = (idseq n) ^ <*(n + 1)*> by FINSEQ_2:51;

then K * (idseq (n + 1)) = (K * (idseq n)) ^ (K * <*(n + 1)*>) by NEWTON04:43;

then 1 + (K * (idseq (n + 1))) = (1 + (K * (idseq n))) ^ (1 + (K * <*(n + 1)*>)) by BASEL_1:3;

then Product (1 + (K * (idseq (n + 1)))) = (Product (1 + (K * (idseq n)))) * (1 + (K * (n + 1))) by A4, RVSUM_1:96;

then Product (1 + (K * (idseq (n + 1)))) = 1 + (K * ((Z + (n + 1)) + ((K * Z) * (n + 1)))) by A3;

hence S

hence for n being Nat ex Z being Nat st

( Product (1 + (K * (idseq n))) = 1 + (K * Z) & ( n > 0 implies Z > 0 ) ) ; :: thesis: verum