let p be prime odd Nat; :: thesis: for m being positive Nat
for k being Nat st 0 <= k & k <= p -' 2 holds
eval ((~ (((Der1 INT.Ring) |^ k) . (f_0 (m,p)))),(0. INT.Ring)) = 0. INT.Ring
let m be positive Nat; :: thesis: for k being Nat st 0 <= k & k <= p -' 2 holds
eval ((~ (((Der1 INT.Ring) |^ k) . (f_0 (m,p)))),(0. INT.Ring)) = 0. INT.Ring
let k be Nat; :: thesis: ( 0 <= k & k <= p -' 2 implies eval ((~ (((Der1 INT.Ring) |^ k) . (f_0 (m,p)))),(0. INT.Ring)) = 0. INT.Ring )
assume A1: ( 0 <= k & k <= p -' 2 ) ; :: thesis: eval ((~ (((Der1 INT.Ring) |^ k) . (f_0 (m,p)))),(0. INT.Ring)) = 0. INT.Ring
set Fk = ((Der1 INT.Ring) |^ k) . (f_0 (m,p));
eval ((~ (((Der1 INT.Ring) |^ k) . (f_0 (m,p)))),(0. INT.Ring)) = (~ (((Der1 INT.Ring) |^ k) . (f_0 (m,p)))) . 0 by POLYNOM5:31;
hence eval ((~ (((Der1 INT.Ring) |^ k) . (f_0 (m,p)))),(0. INT.Ring)) = 0. INT.Ring by Th21, A1; :: thesis: verum