let f be PartFunc of REAL , REAL ; :: thesis: for Z being Subset of REAL
for Z1 being open Subset of REAL st Z1 c= Z holds
for n being Element of NAT st f is_differentiable_on n,Z holds
((diff f,Z) . n) | Z1 = (diff f,Z1) . n
let Z be Subset of REAL ; :: thesis: for Z1 being open Subset of REAL st Z1 c= Z holds
for n being Element of NAT st f is_differentiable_on n,Z holds
((diff f,Z) . n) | Z1 = (diff f,Z1) . n
let Z1 be open Subset of REAL ; :: thesis: ( Z1 c= Z implies for n being Element of NAT st f is_differentiable_on n,Z holds
((diff f,Z) . n) | Z1 = (diff f,Z1) . n )
assume A1: Z1 c= Z ; :: thesis: for n being Element of NAT st f is_differentiable_on n,Z holds
((diff f,Z) . n) | Z1 = (diff f,Z1) . n
defpred S₁[ Element of NAT ] means ( f is_differentiable_on $1,Z implies ((diff f,Z) . $1) | Z1 = (diff f,Z1) . $1 );
A2: S₁[ 0 ]

proof

assume f is_differentiable_on 0 ,Z ; :: thesis: ((diff f,Z) . 0 ) | Z1 = (diff f,Z1) . 0
thus ((diff f,Z) . 0 ) | Z1 = (f | Z) | Z1 by Def5
.= f | Z1 by A1, FUNCT_1:82
.= (diff f,Z1) . 0 by Def5 ; :: thesis: verum

end;

A3: 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 A4: S₁[k] ; :: thesis: S₁[k + 1]
assume A5: f is_differentiable_on k + 1,Z ; :: thesis: ((diff f,Z) . (k + 1)) | Z1 = (diff f,Z1) . (k + 1)
A6: k <= k + 1 by NAT_1:11;
k <= (k + 1) - 1 ;
then A7: (diff f,Z) . k is_differentiable_on Z by A5, Def6;
then A8: (diff f,Z) . k is_differentiable_on Z1 by A1, FDIFF_1:34;
A9: dom ((((diff f,Z) . k) `| Z) | Z1) = (dom (((diff f,Z) . k) `| Z)) /\ Z1 by FUNCT_1:68
.= Z /\ Z1 by A7, FDIFF_1:def 8
.= Z1 by A1, XBOOLE_1:28 ;
A10: dom (((diff f,Z) . k) `| Z1) = Z1 by A8, FDIFF_1:def 8;

A11: now

let x be Real; :: thesis: ( x in dom ((((diff f,Z) . k) `| Z) | Z1) implies ((((diff f,Z) . k) `| Z) | Z1) . x = (((diff f,Z) . k) `| Z1) . x )
assume A12: x in dom ((((diff f,Z) . k) `| Z) | Z1) ; :: thesis: ((((diff f,Z) . k) `| Z) | Z1) . x = (((diff f,Z) . k) `| Z1) . x
thus ((((diff f,Z) . k) `| Z) | Z1) . x = (((diff f,Z) . k) `| Z) . x by A9, A12, FUNCT_1:72
.= diff ((diff f,Z) . k),x by A1, A7, A9, A12, FDIFF_1:def 8
.= (((diff f,Z) . k) `| Z1) . x by A8, A9, A12, FDIFF_1:def 8 ; :: thesis: verum

end;

thus ((diff f,Z) . (k + 1)) | Z1 = (((diff f,Z) . k) `| Z) | Z1 by Def5
.= ((diff f,Z) . k) `| Z1 by A9, A10, A11, PARTFUN1:34
.= ((diff f,Z1) . k) `| Z1 by A4, A5, A6, A8, Th23, FDIFF_2:16
.= (diff f,Z1) . (k + 1) by Def5 ; :: thesis: verum

end;

thus for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A2, A3); :: thesis: verum