let S, T be RealNormSpace; :: thesis: for f being PartFunc of S,T
for Z being Subset of S
for n being Nat st f is_differentiable_on n,Z holds
for m being Nat st m <= n holds
f is_differentiable_on m,Z
let f be PartFunc of S,T; :: thesis: for Z being Subset of S
for n being Nat st f is_differentiable_on n,Z holds
for m being Nat st m <= n holds
f is_differentiable_on m,Z
let Z be Subset of S; :: thesis: for n being Nat st f is_differentiable_on n,Z holds
for m being Nat st m <= n holds
f is_differentiable_on m,Z
let n be Nat; :: thesis: ( f is_differentiable_on n,Z implies for m being Nat st m <= n holds
f is_differentiable_on m,Z )
assume A1: f is_differentiable_on n,Z ; :: thesis: for m being Nat st m <= n holds
f is_differentiable_on m,Z
let m be Nat; :: thesis: ( m <= n implies f is_differentiable_on m,Z )
assume m <= n ; :: thesis: f is_differentiable_on m,Z
then A2: m - 1 <= n - 1 by XREAL_1:13;
thus Z c= dom f by A1; :: according to NDIFF_6:def 7 :: thesis: for i being Nat st i <= m - 1 holds
modetrans (((diff (f,Z)) . i),S,(diff_SP (i,S,T))) is_differentiable_on Z
thus for i being Nat st i <= m - 1 holds
modetrans (((diff (f,Z)) . i),S,(diff_SP (i,S,T))) is_differentiable_on Z by A1, A2, XXREAL_0:2; :: thesis: verum