let n be Nat; :: thesis: for h, x being Real
for f being Function of REAL,REAL holds ((fdif (f,h)) . ((2 * n) + 1)) . x = ((cdif (f,h)) . ((2 * n) + 1)) . ((x + (n * h)) + (h / 2))

let h, x be Real; :: thesis: for f being Function of REAL,REAL holds ((fdif (f,h)) . ((2 * n) + 1)) . x = ((cdif (f,h)) . ((2 * n) + 1)) . ((x + (n * h)) + (h / 2))
let f be Function of REAL,REAL; :: thesis: ((fdif (f,h)) . ((2 * n) + 1)) . x = ((cdif (f,h)) . ((2 * n) + 1)) . ((x + (n * h)) + (h / 2))
defpred S1[ Nat] means for x being Real holds ((fdif (f,h)) . ((2 * \$1) + 1)) . x = ((cdif (f,h)) . ((2 * \$1) + 1)) . ((x + (\$1 * h)) + (h / 2));
A1: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A2: for x being Real holds ((fdif (f,h)) . ((2 * k) + 1)) . x = ((cdif (f,h)) . ((2 * k) + 1)) . ((x + (k * h)) + (h / 2)) ; :: thesis: S1[k + 1]
let x be Real; :: thesis: ((fdif (f,h)) . ((2 * (k + 1)) + 1)) . x = ((cdif (f,h)) . ((2 * (k + 1)) + 1)) . ((x + ((k + 1) * h)) + (h / 2))
A3: ((fdif (f,h)) . ((2 * k) + 1)) . ((x + h) + h) = ((cdif (f,h)) . ((2 * k) + 1)) . ((((x + h) + h) + (k * h)) + (h / 2)) by A2
.= ((cdif (f,h)) . ((2 * k) + 1)) . ((x + ((k + 2) * h)) + (h / 2)) ;
A4: ((fdif (f,h)) . ((2 * k) + 1)) . (x + h) = ((cdif (f,h)) . ((2 * k) + 1)) . (((x + h) + (k * h)) + (h / 2)) by A2
.= ((cdif (f,h)) . ((2 * k) + 1)) . ((x + ((k + 1) * h)) + (h / 2)) ;
set r3 = ((cdif (f,h)) . ((2 * k) + 1)) . ((x + (k * h)) + (h / 2));
set r2 = ((cdif (f,h)) . ((2 * k) + 1)) . ((x + ((k + 1) * h)) + (h / 2));
set r1 = ((cdif (f,h)) . ((2 * k) + 1)) . ((x + ((k + 2) * h)) + (h / 2));
A5: (fdif (f,h)) . (2 * (k + 1)) is Function of REAL,REAL by Th2;
A6: (cdif (f,h)) . ((2 * k) + 1) is Function of REAL,REAL by Th19;
A7: (cdif (f,h)) . (2 * (k + 1)) is Function of REAL,REAL by Th19;
A8: (fdif (f,h)) . ((2 * k) + 1) is Function of REAL,REAL by Th2;
A9: ((cdif (f,h)) . (2 * (k + 1))) . (x + ((k + 1) * h)) = ((cdif (f,h)) . (((2 * k) + 1) + 1)) . (x + ((k + 1) * h))
.= (cD (((cdif (f,h)) . ((2 * k) + 1)),h)) . (x + ((k + 1) * h)) by Def8
.= (((cdif (f,h)) . ((2 * k) + 1)) . ((x + ((k + 1) * h)) + (h / 2))) - (((cdif (f,h)) . ((2 * k) + 1)) . ((x + ((k + 1) * h)) - (h / 2))) by
.= (((cdif (f,h)) . ((2 * k) + 1)) . ((x + ((k + 1) * h)) + (h / 2))) - (((cdif (f,h)) . ((2 * k) + 1)) . ((x + (k * h)) + (h / 2))) ;
A10: ((cdif (f,h)) . (2 * (k + 1))) . (x + ((k + 2) * h)) = ((cdif (f,h)) . (((2 * k) + 1) + 1)) . (x + ((k + 2) * h))
.= (cD (((cdif (f,h)) . ((2 * k) + 1)),h)) . (x + ((k + 2) * h)) by Def8
.= (((cdif (f,h)) . ((2 * k) + 1)) . ((x + ((k + 2) * h)) + (h / 2))) - (((cdif (f,h)) . ((2 * k) + 1)) . ((x + ((k + 2) * h)) - (h / 2))) by
.= (((cdif (f,h)) . ((2 * k) + 1)) . ((x + ((k + 2) * h)) + (h / 2))) - (((cdif (f,h)) . ((2 * k) + 1)) . ((x + ((k + 1) * h)) + (h / 2))) ;
A11: ((cdif (f,h)) . ((2 * (k + 1)) + 1)) . ((x + ((k + 1) * h)) + (h / 2)) = (cD (((cdif (f,h)) . (2 * (k + 1))),h)) . ((x + ((k + 1) * h)) + (h / 2)) by Def8
.= (((cdif (f,h)) . (2 * (k + 1))) . (((x + ((k + 1) * h)) + (h / 2)) + (h / 2))) - (((cdif (f,h)) . (2 * (k + 1))) . (((x + ((k + 1) * h)) + (h / 2)) - (h / 2))) by
.= ((((cdif (f,h)) . ((2 * k) + 1)) . ((x + ((k + 2) * h)) + (h / 2))) - (((cdif (f,h)) . ((2 * k) + 1)) . ((x + ((k + 1) * h)) + (h / 2)))) - ((((cdif (f,h)) . ((2 * k) + 1)) . ((x + ((k + 1) * h)) + (h / 2))) - (((cdif (f,h)) . ((2 * k) + 1)) . ((x + (k * h)) + (h / 2)))) by ;
((fdif (f,h)) . ((2 * (k + 1)) + 1)) . x = (fD (((fdif (f,h)) . (2 * (k + 1))),h)) . x by Def6
.= (((fdif (f,h)) . (2 * (k + 1))) . (x + h)) - (((fdif (f,h)) . (2 * (k + 1))) . x) by
.= ((fD (((fdif (f,h)) . ((2 * k) + 1)),h)) . (x + h)) - (((fdif (f,h)) . (((2 * k) + 1) + 1)) . x) by Def6
.= ((fD (((fdif (f,h)) . ((2 * k) + 1)),h)) . (x + h)) - ((fD (((fdif (f,h)) . ((2 * k) + 1)),h)) . x) by Def6
.= ((((fdif (f,h)) . ((2 * k) + 1)) . ((x + h) + h)) - (((fdif (f,h)) . ((2 * k) + 1)) . (x + h))) - ((fD (((fdif (f,h)) . ((2 * k) + 1)),h)) . x) by
.= ((((fdif (f,h)) . ((2 * k) + 1)) . ((x + h) + h)) - (((fdif (f,h)) . ((2 * k) + 1)) . (x + h))) - ((((fdif (f,h)) . ((2 * k) + 1)) . (x + h)) - (((fdif (f,h)) . ((2 * k) + 1)) . x)) by
.= ((((cdif (f,h)) . ((2 * k) + 1)) . ((x + ((k + 2) * h)) + (h / 2))) - (((cdif (f,h)) . ((2 * k) + 1)) . ((x + ((k + 1) * h)) + (h / 2)))) - ((((cdif (f,h)) . ((2 * k) + 1)) . ((x + ((k + 1) * h)) + (h / 2))) - (((cdif (f,h)) . ((2 * k) + 1)) . ((x + (k * h)) + (h / 2)))) by A2, A3, A4 ;
hence ((fdif (f,h)) . ((2 * (k + 1)) + 1)) . x = ((cdif (f,h)) . ((2 * (k + 1)) + 1)) . ((x + ((k + 1) * h)) + (h / 2)) by A11; :: thesis: verum
end;
A12: S1[ 0 ]
proof
let x be Real; :: thesis: ((fdif (f,h)) . ((2 * 0) + 1)) . x = ((cdif (f,h)) . ((2 * 0) + 1)) . ((x + (0 * h)) + (h / 2))
((fdif (f,h)) . ((2 * 0) + 1)) . x = (fD (((fdif (f,h)) . 0),h)) . x by Def6
.= (fD (f,h)) . x by Def6
.= (f . (x + h)) - (f . x) by Th3
.= (f . ((x + (h / 2)) + (h / 2))) - (f . ((x + (h / 2)) - (h / 2)))
.= (cD (f,h)) . (x + (h / 2)) by Th5
.= (cD (((cdif (f,h)) . 0),h)) . (x + (h / 2)) by Def8
.= ((cdif (f,h)) . ((2 * 0) + 1)) . ((x + (0 * h)) + (h / 2)) by Def8 ;
hence ((fdif (f,h)) . ((2 * 0) + 1)) . x = ((cdif (f,h)) . ((2 * 0) + 1)) . ((x + (0 * h)) + (h / 2)) ; :: thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch 2(A12, A1);
hence ((fdif (f,h)) . ((2 * n) + 1)) . x = ((cdif (f,h)) . ((2 * n) + 1)) . ((x + (n * h)) + (h / 2)) ; :: thesis: verum