deffunc H1( Nat) -> set = ((((diff (f,Z)) . $1) . a) * ((b - a) |^ $1)) / ($1 !);
let s1, s2 be Real_Sequence; ( ( for n being Nat holds s1 . n = ((((diff (f,Z)) . n) . a) * ((b - a) |^ n)) / (n !) ) & ( for n being Nat holds s2 . n = ((((diff (f,Z)) . n) . a) * ((b - a) |^ n)) / (n !) ) implies s1 = s2 )
assume that
A2:
for n being Nat holds s1 . n = H1(n)
and
A3:
for n being Nat holds s2 . n = H1(n)
; s1 = s2
hence
s1 = s2
; verum