let f be PartFunc of REAL,REAL; :: thesis: for Z being Subset of REAL
for n being Nat st f is_differentiable_on n,Z holds
for a, b being Real st a < b & ].a,b.[ c= Z holds
((diff (f,Z)) . n) | ].a,b.[ = (diff (f,].a,b.[)) . n
let Z be Subset of REAL; :: thesis: for n being Nat st f is_differentiable_on n,Z holds
for a, b being Real st a < b & ].a,b.[ c= Z holds
((diff (f,Z)) . n) | ].a,b.[ = (diff (f,].a,b.[)) . n
defpred S₁[ Nat] means ( f is_differentiable_on $1,Z implies for a, b being Real st a < b & ].a,b.[ c= Z holds
((diff (f,Z)) . $1) | ].a,b.[ = (diff (f,].a,b.[)) . $1 );
A1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A2: S₁[k] ; :: thesis: S₁[k + 1]
assume A3: f is_differentiable_on k + 1,Z ; :: thesis: for a, b being Real st a < b & ].a,b.[ c= Z holds
((diff (f,Z)) . (k + 1)) | ].a,b.[ = (diff (f,].a,b.[)) . (k + 1)
let a, b be Real; :: thesis: ( a < b & ].a,b.[ c= Z implies ((diff (f,Z)) . (k + 1)) | ].a,b.[ = (diff (f,].a,b.[)) . (k + 1) )
assume that
A4: a < b and
A5: ].a,b.[ c= Z ; :: thesis: ((diff (f,Z)) . (k + 1)) | ].a,b.[ = (diff (f,].a,b.[)) . (k + 1)
A6: (diff (f,Z)) . k is_differentiable_on Z by A3;
then A7: (diff (f,Z)) . k is_differentiable_on ].a,b.[ by A5, FDIFF_1:26;
then A8: dom (((diff (f,Z)) . k) `| ].a,b.[) = ].a,b.[ by FDIFF_1:def 7;
A9: dom ((((diff (f,Z)) . k) `| Z) | ].a,b.[) = (dom (((diff (f,Z)) . k) `| Z)) /\ ].a,b.[ by RELAT_1:61
.= Z /\ ].a,b.[ by A6, FDIFF_1:def 7
.= ].a,b.[ by A5, XBOOLE_1:28 ;

A10: now :: thesis: for x being Element of REAL st x in dom ((((diff (f,Z)) . k) `| Z) | ].a,b.[) holds
((((diff (f,Z)) . k) `| Z) | ].a,b.[) . x = (((diff (f,Z)) . k) `| ].a,b.[) . x

let x be Element of REAL ; :: thesis: ( x in dom ((((diff (f,Z)) . k) `| Z) | ].a,b.[) implies ((((diff (f,Z)) . k) `| Z) | ].a,b.[) . x = (((diff (f,Z)) . k) `| ].a,b.[) . x )
assume A11: x in dom ((((diff (f,Z)) . k) `| Z) | ].a,b.[) ; :: thesis: ((((diff (f,Z)) . k) `| Z) | ].a,b.[) . x = (((diff (f,Z)) . k) `| ].a,b.[) . x
thus ((((diff (f,Z)) . k) `| Z) | ].a,b.[) . x = (((diff (f,Z)) . k) `| Z) . x by A9, A11, FUNCT_1:49
.= diff (((diff (f,Z)) . k),x) by A5, A6, A9, A11, FDIFF_1:def 7
.= (((diff (f,Z)) . k) `| ].a,b.[) . x by A7, A9, A11, FDIFF_1:def 7 ; :: thesis: verum

end;

thus ((diff (f,Z)) . (k + 1)) | ].a,b.[ = (((diff (f,Z)) . k) `| Z) | ].a,b.[ by Def5
.= ((diff (f,Z)) . k) `| ].a,b.[ by A9, A8, A10, PARTFUN1:5
.= (((diff (f,Z)) . k) | ].a,b.[) `| ].a,b.[ by A7, FDIFF_2:16
.= ((diff (f,].a,b.[)) . k) `| ].a,b.[ by A2, A3, A4, A5, Th23, NAT_1:11
.= (diff (f,].a,b.[)) . (k + 1) by Def5 ; :: thesis: verum

end;

A12: S₁[ 0 ]

proof

assume f is_differentiable_on 0 ,Z ; :: thesis: for a, b being Real st a < b & ].a,b.[ c= Z holds
((diff (f,Z)) . 0) | ].a,b.[ = (diff (f,].a,b.[)) . 0
let a, b be Real; :: thesis: ( a < b & ].a,b.[ c= Z implies ((diff (f,Z)) . 0) | ].a,b.[ = (diff (f,].a,b.[)) . 0 )
assume that
a < b and
A13: ].a,b.[ c= Z ; :: thesis: ((diff (f,Z)) . 0) | ].a,b.[ = (diff (f,].a,b.[)) . 0
thus ((diff (f,Z)) . 0) | ].a,b.[ = (f | Z) | ].a,b.[ by Def5
.= f | ].a,b.[ by A13, FUNCT_1:51
.= (diff (f,].a,b.[)) . 0 by Def5 ; :: thesis: verum

end;

thus for k being Nat holds S₁[k] from NAT_1:sch 2(A12, A1); :: thesis: verum