let S, T be RealNormSpace; :: thesis: for f being PartFunc of S,T
for Z being Subset of S
for k being Nat st f is_differentiable_on k,Z holds
( f | Z is_differentiable_on k,Z & diff ((f | Z),k,Z) = diff (f,k,Z) )
let f be PartFunc of S,T; :: thesis: for Z being Subset of S
for k being Nat st f is_differentiable_on k,Z holds
( f | Z is_differentiable_on k,Z & diff ((f | Z),k,Z) = diff (f,k,Z) )
let Z be Subset of S; :: thesis: for k being Nat st f is_differentiable_on k,Z holds
( f | Z is_differentiable_on k,Z & diff ((f | Z),k,Z) = diff (f,k,Z) )
defpred S₁[ Nat] means ( f is_differentiable_on $1,Z implies ( f | Z is_differentiable_on $1,Z & diff ((f | Z),$1,Z) = diff (f,$1,Z) ) );
A1: S₁[ 0 ]

proof

assume f is_differentiable_on 0 ,Z ; :: thesis: ( f | Z is_differentiable_on 0 ,Z & diff ((f | Z),0,Z) = diff (f,0,Z) )
hence f | Z is_differentiable_on 0 ,Z by RELAT_1:62; :: thesis: diff ((f | Z),0,Z) = diff (f,0,Z)
diff ((f | Z),0,Z) = (f | Z) | Z by NDIFF_6:11
.= f | Z ;
hence diff ((f | Z),0,Z) = diff (f,0,Z) by NDIFF_6:11; :: thesis: verum

end;

A4: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A5: S₁[k] ; :: thesis: S₁[k + 1]
assume A6: f is_differentiable_on k + 1,Z ; :: thesis: ( f | Z is_differentiable_on k + 1,Z & diff ((f | Z),(k + 1),Z) = diff (f,(k + 1),Z) )
then A7: dom (f | Z) = Z by RELAT_1:62;
A8: k + 0 <= k + 1 by XREAL_1:7;
for i being Nat st i <= (k + 1) - 1 holds
diff ((f | Z),i,Z) is_differentiable_on Z

proof

let i be Nat; :: thesis: ( i <= (k + 1) - 1 implies diff ((f | Z),i,Z) is_differentiable_on Z )
assume A9: i <= (k + 1) - 1 ; :: thesis: diff ((f | Z),i,Z) is_differentiable_on Z

per cases ( i = k or i <> k ) ;

suppose i = k ; :: thesis: diff ((f | Z),i,Z) is_differentiable_on Z

hence diff ((f | Z),i,Z) is_differentiable_on Z by A5, A6, A8, NDIFF_6:14, NDIFF_6:17; :: thesis: verum

end;

suppose i <> k ; :: thesis: diff ((f | Z),i,Z) is_differentiable_on Z

then i < k by A9, XXREAL_0:1;
then i + 1 <= k by NAT_1:13;
then (i + 1) - 1 <= k - 1 by XREAL_1:13;
hence diff ((f | Z),i,Z) is_differentiable_on Z by A5, A6, A8, NDIFF_6:14, NDIFF_6:17; :: thesis: verum

end;

end;

end;

hence f | Z is_differentiable_on k + 1,Z by A7, NDIFF_6:14; :: thesis: diff ((f | Z),(k + 1),Z) = diff (f,(k + 1),Z)
thus diff ((f | Z),(k + 1),Z) = (diff (f,k,Z)) `| Z by A5, A6, A8, NDIFF_6:13, NDIFF_6:17
.= diff (f,(k + 1),Z) by NDIFF_6:13 ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A4);
hence for k being Nat st f is_differentiable_on k,Z holds
( f | Z is_differentiable_on k,Z & diff ((f | Z),k,Z) = diff (f,k,Z) ) ; :: thesis: verum