deffunc H₁( Nat) -> set = ((((diff (f,Z)) . $1) . a) * ((b - a) |^ $1)) / ($1 !);
consider seq being Real_Sequence such that
A1: for n being Nat holds seq . n = H₁(n) from SEQ_1:sch 1();
take seq ; :: thesis: for n being Nat holds seq . n = ((((diff (f,Z)) . n) . a) * ((b - a) |^ n)) / (n !)
let n be Nat; :: thesis: seq . n = ((((diff (f,Z)) . n) . a) * ((b - a) |^ n)) / (n !)
thus seq . n = ((((diff (f,Z)) . n) . a) * ((b - a) |^ n)) / (n !) by A1; :: thesis: verum