let p be prime odd Nat; :: thesis: for m being positive Nat holds
( len (x. (m,p)) = m & len (ff_0 (m,p)) = m + 1 & (ff_0 (m,p)) . ((len (x. (m,p))) + 1) = (tau 0) |^ (p -' 1) )
let m be positive Nat; :: thesis: ( len (x. (m,p)) = m & len (ff_0 (m,p)) = m + 1 & (ff_0 (m,p)) . ((len (x. (m,p))) + 1) = (tau 0) |^ (p -' 1) )
A1: len <*((tau 0) |^ (p -' 1))*> = 1 by FINSEQ_1:40;
len (ff_0 (m,p)) = (len (x. (m,p))) + (len <*((tau 0) |^ (p -' 1))*>) by FINSEQ_1:22
.= m + 1 by Def2, A1 ;
hence ( len (x. (m,p)) = m & len (ff_0 (m,p)) = m + 1 & (ff_0 (m,p)) . ((len (x. (m,p))) + 1) = (tau 0) |^ (p -' 1) ) by Def2; :: thesis: verum