let Z be open Subset of REAL ; :: thesis: for n being Element of NAT holds (diff exp_R ,Z) . n = exp_R | Z
let n be Element of NAT ; :: thesis: (diff exp_R ,Z) . n = exp_R | Z
defpred S₁[ Element of NAT ] means (diff exp_R ,Z) . $1 = exp_R | Z;
A1: S₁[ 0 ] by TAYLOR_1:def 5;
A2: 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 A3: S₁[k] ; :: thesis: S₁[k + 1]
A4: exp_R is_differentiable_on Z by FDIFF_1:34, TAYLOR_1:16;
(diff exp_R ,Z) . (k + 1) = ((diff exp_R ,Z) . k) `| Z by TAYLOR_1:def 5
.= exp_R `| Z by A3, A4, FDIFF_2:16
.= exp_R | Z by Th5 ;
hence S₁[k + 1] ; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A1, A2);
hence (diff exp_R ,Z) . n = exp_R | Z ; :: thesis: verum