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₁[ 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₁[ 0 ] ;
A2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume S₁[n] ; :: thesis: S₁[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₁[n + 1] ; :: thesis: verum

end;

for n being Nat holds S₁[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