let p be prime odd Nat; :: thesis: for m being positive Nat holds len (~ (f_0 (m,p))) = (m * p) + p
let m be positive Nat; :: thesis: len (~ (f_0 (m,p))) = (m * p) + p
set xp0 = x. (m,p);
set pp0 = Product (x. (m,p));
set t0 = (tau 0) |^ (p -' 1);
A1: len (~ (Product (x. (m,p)))) = (m * p) + 1 by Th11;
A2: p -' 1 = p - 1 by XREAL_1:233, NAT_1:14;
len (~ ((tau 0) |^ (p -' 1))) = (p -' 1) + 1 by Th8;
then A4: (len (~ (Product (x. (m,p))))) * (len (~ ((tau 0) |^ (p -' 1)))) <> 0 by A1;
A5: len (~ (Product (x. (m,p)))) = (m * p) + 1 by Th11;
len (~ ((tau 0) |^ (p -' 1))) = (p -' 1) + 1 by Th8;
then len (~ ((Product (x. (m,p))) * ((tau 0) |^ (p -' 1)))) = (((m * p) + 1) + p) - 1 by A2, A5, A4, Th9;
hence len (~ (f_0 (m,p))) = (m * p) + p by GROUP_4:6; :: thesis: verum