let n be Element of NAT ; :: thesis: for h, x being Real
for f being Function of REAL ,REAL holds ((fdif f,h) . (2 * n)) . x = ((cdif f,h) . (2 * n)) . (x + (n * h))
let h, x be Real; :: thesis: for f being Function of REAL ,REAL holds ((fdif f,h) . (2 * n)) . x = ((cdif f,h) . (2 * n)) . (x + (n * h))
let f be Function of REAL ,REAL ; :: thesis: ((fdif f,h) . (2 * n)) . x = ((cdif f,h) . (2 * n)) . (x + (n * h))
defpred S₁[ Element of NAT ] means for x being Real holds ((fdif f,h) . (2 * $1)) . x = ((cdif f,h) . (2 * $1)) . (x + ($1 * h));
A1: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A2: for x being Real holds ((fdif f,h) . (2 * k)) . x = ((cdif f,h) . (2 * k)) . (x + (k * h)) ; :: thesis: S₁[k + 1]
let x be Real; :: thesis: ((fdif f,h) . (2 * (k + 1))) . x = ((cdif f,h) . (2 * (k + 1))) . (x + ((k + 1) * h))
A3: ((fdif f,h) . (2 * k)) . ((x + h) + h) = ((cdif f,h) . (2 * k)) . (((x + h) + h) + (k * h)) by A2
.= ((cdif f,h) . (2 * k)) . (x + ((k + 2) * h)) ;
A4: ((fdif f,h) . (2 * k)) . (x + h) = ((cdif f,h) . (2 * k)) . ((x + h) + (k * h)) by A2
.= ((cdif f,h) . (2 * k)) . (x + ((k + 1) * h)) ;
set r3 = ((cdif f,h) . (2 * k)) . (x + (k * h));
set r2 = ((cdif f,h) . (2 * k)) . (x + ((k + 1) * h));
set r1 = ((cdif f,h) . (2 * k)) . (x + ((k + 2) * h));
A5: (fdif f,h) . ((2 * k) + 1) is Function of REAL ,REAL by Th2;
A6: (cdif f,h) . (2 * k) 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) is Function of REAL ,REAL by Th2;
A9: ((cdif f,h) . ((2 * k) + 1)) . ((x + ((k + 1) * h)) - (h / 2)) = (cD ((cdif f,h) . (2 * k)),h) . ((x + ((k + 1) * h)) - (h / 2)) by Def8
.= (((cdif f,h) . (2 * k)) . (((x + ((k + 1) * h)) - (h / 2)) + (h / 2))) - (((cdif f,h) . (2 * k)) . (((x + ((k + 1) * h)) - (h / 2)) - (h / 2))) by A6, Th5
.= (((cdif f,h) . (2 * k)) . (x + ((k + 1) * h))) - (((cdif f,h) . (2 * k)) . (x + (k * h))) ;
A10: ((cdif f,h) . ((2 * k) + 1)) . ((x + ((k + 1) * h)) + (h / 2)) = (cD ((cdif f,h) . (2 * k)),h) . ((x + ((k + 1) * h)) + (h / 2)) by Def8
.= (((cdif f,h) . (2 * k)) . (((x + ((k + 1) * h)) + (h / 2)) + (h / 2))) - (((cdif f,h) . (2 * k)) . (((x + ((k + 1) * h)) + (h / 2)) - (h / 2))) by A6, Th5
.= (((cdif f,h) . (2 * k)) . (x + ((k + 2) * h))) - (((cdif f,h) . (2 * k)) . (x + ((k + 1) * h))) ;
A11: ((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)) . (x + ((k + 2) * h))) - (((cdif f,h) . (2 * k)) . (x + ((k + 1) * h)))) - ((((cdif f,h) . (2 * k)) . (x + ((k + 1) * h))) - (((cdif f,h) . (2 * k)) . (x + (k * h)))) by A7, A10, A9, Th5 ;
((fdif f,h) . (2 * (k + 1))) . x = ((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 A5, Th3
.= ((fD ((fdif f,h) . (2 * k)),h) . (x + h)) - (((fdif f,h) . ((2 * k) + 1)) . x) by Def6
.= ((fD ((fdif f,h) . (2 * k)),h) . (x + h)) - ((fD ((fdif f,h) . (2 * k)),h) . x) by Def6
.= ((((fdif f,h) . (2 * k)) . ((x + h) + h)) - (((fdif f,h) . (2 * k)) . (x + h))) - ((fD ((fdif f,h) . (2 * k)),h) . x) by A8, Th3
.= ((((fdif f,h) . (2 * k)) . ((x + h) + h)) - (((fdif f,h) . (2 * k)) . (x + h))) - ((((fdif f,h) . (2 * k)) . (x + h)) - (((fdif f,h) . (2 * k)) . x)) by A8, Th3
.= ((((cdif f,h) . (2 * k)) . (x + ((k + 2) * h))) - (((cdif f,h) . (2 * k)) . (x + ((k + 1) * h)))) - ((((cdif f,h) . (2 * k)) . (x + ((k + 1) * h))) - (((cdif f,h) . (2 * k)) . (x + (k * h)))) by A2, A3, A4 ;
hence ((fdif f,h) . (2 * (k + 1))) . x = ((cdif f,h) . (2 * (k + 1))) . (x + ((k + 1) * h)) by A11; :: thesis: verum

end;

A12: S₁[ 0 ]

proof

let x be Real; :: thesis: ((fdif f,h) . (2 * 0 )) . x = ((cdif f,h) . (2 * 0 )) . (x + (0 * h))
((fdif f,h) . (2 * 0 )) . x = f . x by Def6
.= ((cdif f,h) . (2 * 0 )) . (x + (0 * h)) by Def8 ;
hence ((fdif f,h) . (2 * 0 )) . x = ((cdif f,h) . (2 * 0 )) . (x + (0 * h)) ; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A12, A1);
hence ((fdif f,h) . (2 * n)) . x = ((cdif f,h) . (2 * n)) . (x + (n * h)) ; :: thesis: verum