deffunc H₁( Element of NAT ) -> Element of REAL = ((((diff f,Z) . $1) . a) * ((b - a) |^ $1)) / ($1 ! );
consider seq being Real_Sequence such that
A1: for n being Element of NAT holds seq . n = H₁(n) from SEQ_1:sch 1();
take seq ; :: thesis: for n being natural number holds seq . n = ((((diff f,Z) . n) . a) * ((b - a) |^ n)) / (n ! )
let n be natural number ; :: thesis: seq . n = ((((diff f,Z) . n) . a) * ((b - a) |^ n)) / (n ! )
n is Element of NAT by ORDINAL1:def 13;
hence seq . n = ((((diff f,Z) . n) . a) * ((b - a) |^ n)) / (n ! ) by A1; :: thesis: verum