let p be prime odd Nat; :: thesis: for m being positive Nat holds len (~ (Product (x. (m,p)))) = (m * p) + 1
let m be positive Nat; :: thesis: len (~ (Product (x. (m,p)))) = (m * p) + 1
set PR = Polynom-Ring INT.Ring;
defpred S₁[ non zero Nat] means len (~ (Product (x. ($1,p)))) = ($1 * p) + 1;
A1: S₁[1]

proof

A2: len (x. (1,p)) = 1 by Def2;
A3: x. (1,p) = <*((x. (1,p)) . 1)*> by Def2, FINSEQ_1:40;
dom (x. (1,p)) = Seg 1 by A2, FINSEQ_1:def 3;
then 1 in dom (x. (1,p)) ;
then (x. (1,p)) . 1 = (tau 1) |^ p by Def2;
then len (~ (Product (x. (1,p)))) = len (~ ((tau 1) |^ p)) by A3, FINSOP_1:11
.= p + 1 by Th8 ;
hence S₁[1] ; :: thesis: verum

end;

A5: for k being non zero Nat st S₁[k] holds
S₁[k + 1]

proof

let k be non zero Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A6: S₁[k] ; :: thesis: S₁[k + 1]
set pp0 = Product (x. (k,p));
set t0 = (tau (k + 1)) |^ p;
A7: len (~ ((tau (k + 1)) |^ p)) = p + 1 by Th8;
then A8: (len (~ (Product (x. (k,p))))) * (len (~ ((tau (k + 1)) |^ p))) <> 0 by A6;
len (~ (Product (x. ((k + 1),p)))) = len (~ ((Product (x. (k,p))) * ((tau (k + 1)) |^ p))) by Th10
.= ((len (~ (Product (x. (k,p))))) + (len (~ ((tau (k + 1)) |^ p)))) - 1 by A8, Th9
.= ((k + 1) * p) + 1 by A6, A7 ;
hence S₁[k + 1] ; :: thesis: verum

end;

for k being non zero Nat holds S₁[k] from NAT_1:sch 10(A1, A5);
hence len (~ (Product (x. (m,p)))) = (m * p) + 1 ; :: thesis: verum