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: 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]
assume A4: f is_differentiable_on k + 1,Z ; :: thesis: ((diff f,Z) . (k + 1)) | Z1 = (diff f,Z1) . (k + 1)
k <= (k + 1) - 1 ;
then A5: (diff f,Z) . k is_differentiable_on Z by A4, Def6;
then A6: (diff f,Z) . k is_differentiable_on Z1 by A1, FDIFF_1:34;
then A7: dom (((diff f,Z) . k) `| Z1) = Z1 by FDIFF_1:def 8;
A8: dom ((((diff f,Z) . k) `| Z) | Z1) = (dom (((diff f,Z) . k) `| Z)) /\ Z1 by RELAT_1:90
.= Z /\ Z1 by A5, FDIFF_1:def 8
.= Z1 by A1, XBOOLE_1:28 ;

A9: 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 A10: 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 A8, A10, FUNCT_1:72
.= diff ((diff f,Z) . k),x by A1, A5, A8, A10, FDIFF_1:def 8
.= (((diff f,Z) . k) `| Z1) . x by A6, A8, A10, 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 A8, A7, A9, PARTFUN1:34
.= ((diff f,Z1) . k) `| Z1 by A3, A4, A6, Th23, FDIFF_2:16, NAT_1:11
.= (diff f,Z1) . (k + 1) by Def5 ; :: thesis: verum

end;

A11: 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;

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