let S, E be RealNormSpace; :: thesis: for Z being Subset of S
for u being PartFunc of S,E
for i being Nat st u is_differentiable_on i + 1,Z holds
u `| Z is_differentiable_on i,Z
let Z be Subset of S; :: thesis: for u being PartFunc of S,E
for i being Nat st u is_differentiable_on i + 1,Z holds
u `| Z is_differentiable_on i,Z
let u be PartFunc of S,E; :: thesis: for i being Nat st u is_differentiable_on i + 1,Z holds
u `| Z is_differentiable_on i,Z
defpred S<sub>1</sub>[ Nat] means ( u is_differentiable_on $1 + 1,Z implies u `| Z is_differentiable_on $1,Z );
A1: S₁[ 0 ]

proof

assume u is_differentiable_on 0 + 1,Z ; :: thesis: u `| Z is_differentiable_on 0 ,Z
then A2: ( Z c= dom u & u | Z is_differentiable_on Z ) by NDIFF_6:15;
u is_differentiable_on Z by A2;
hence u `| Z is_differentiable_on 0 ,Z by NDIFF_1:def 9; :: thesis: verum

end;

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

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A5: S₁[i] ; :: thesis: S₁[i + 1]
assume A6: u is_differentiable_on (i + 1) + 1,Z ; :: thesis: u `| Z is_differentiable_on i + 1,Z
A7: 0 + (i + 1) <= (i + 1) + 1 by XREAL_1:7;
0 <= i by NAT_1:2;
then 0 + 2 <= i + 2 by XREAL_1:7;
then A8: u is_differentiable_on 2,Z by A6, NDIFF_6:17;
A9: ( Z c= dom u & u | Z is_differentiable_on Z ) by A8, NDIFF_6:16;
A10: u is_differentiable_on Z by A9;
then A11: dom (u `| Z) = Z by NDIFF_1:def 9;
for k being Nat st k <= (i + 1) - 1 holds
diff ((u `| Z),k,Z) is_differentiable_on Z

proof

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

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

suppose A13: k = i ; :: thesis: diff ((u `| Z),k,Z) is_differentiable_on Z

A14: diff_SP ((k + 1),S,E) = diff_SP (k,S,(R_NormSpace_of_BoundedLinearOperators (S,E))) by Th30;
(u | Z) `| Z = (u `| Z) | Z by A10, A11, Th4;
then diff ((u `| Z),k,Z) = diff (u,(i + 1),Z) by A13, Th31;
hence diff ((u `| Z),k,Z) is_differentiable_on Z by A6, A13, A14, NDIFF_6:14; :: thesis: verum

end;

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

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

end;

end;

end;

hence u `| Z is_differentiable_on i + 1,Z by A11, NDIFF_6:14; :: thesis: verum

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A1, A4);
hence for i being Nat st u is_differentiable_on i + 1,Z holds
u `| Z is_differentiable_on i,Z ; :: thesis: verum