let p be prime odd Nat; :: thesis: for m being positive Nat
for i being Nat st i in Seg m holds
( (ff_0 (m,p)) /. i = (tau i) |^ p & (ff_0 (m,p)) . i = (tau i) |^ p & i in dom (ff_0 (m,p)) )
let m be positive Nat; :: thesis: for i being Nat st i in Seg m holds
( (ff_0 (m,p)) /. i = (tau i) |^ p & (ff_0 (m,p)) . i = (tau i) |^ p & i in dom (ff_0 (m,p)) )
let i be Nat; :: thesis: ( i in Seg m implies ( (ff_0 (m,p)) /. i = (tau i) |^ p & (ff_0 (m,p)) . i = (tau i) |^ p & i in dom (ff_0 (m,p)) ) )
assume A1: i in Seg m ; :: thesis: ( (ff_0 (m,p)) /. i = (tau i) |^ p & (ff_0 (m,p)) . i = (tau i) |^ p & i in dom (ff_0 (m,p)) )
then i in Seg (len (x. (m,p))) by Def2;
then A2: i in dom (x. (m,p)) by FINSEQ_1:def 3;
then A3: (ff_0 (m,p)) . i = (x. (m,p)) . i by FINSEQ_1:def 7
.= (tau i) |^ p by A2, Def2 ;
len (ff_0 (m,p)) = m + 1 by Th16;
then A4: dom (ff_0 (m,p)) = Seg (m + 1) by FINSEQ_1:def 3;
m + 0 <= m + 1 by XREAL_1:7;
then i in dom (ff_0 (m,p)) by A4, A1, FINSEQ_1:5, TARSKI:def 3;
hence ( (ff_0 (m,p)) /. i = (tau i) |^ p & (ff_0 (m,p)) . i = (tau i) |^ p & i in dom (ff_0 (m,p)) ) by A3, PARTFUN1:def 6; :: thesis: verum