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 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 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 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 Nat st f is_differentiable_on n,Z holds
((diff (f,Z)) . n) | Z1 = (diff (f,Z1)) . n
defpred S₁[ Nat] means ( f is_differentiable_on $1,Z implies ((diff (f,Z)) . $1) | Z1 = (diff (f,Z1)) . $1 );
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be 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)
A5: (diff (f,Z)) . k is_differentiable_on Z by A4;
then A6: (diff (f,Z)) . k is_differentiable_on Z1 by A1, FDIFF_1:26;
then A7: dom (((diff (f,Z)) . k) `| Z1) = Z1 by FDIFF_1:def 7;
A8: dom ((((diff (f,Z)) . k) `| Z) | Z1) = (dom (((diff (f,Z)) . k) `| Z)) /\ Z1 by RELAT_1:61
.= Z /\ Z1 by A5, FDIFF_1:def 7
.= Z1 by A1, XBOOLE_1:28 ;

A9: now :: thesis: for x being Element of REAL st x in dom ((((diff (f,Z)) . k) `| Z) | Z1) holds
((((diff (f,Z)) . k) `| Z) | Z1) . x = (((diff (f,Z)) . k) `| Z1) . x

let x be Element of 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:49
.= diff (((diff (f,Z)) . k),x) by A1, A5, A8, A10, FDIFF_1:def 7
.= (((diff (f,Z)) . k) `| Z1) . x by A6, A8, A10, FDIFF_1:def 7 ; :: 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:5
.= ((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:51
.= (diff (f,Z1)) . 0 by Def5 ; :: thesis: verum

end;

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