let f be PartFunc of REAL,REAL; :: thesis: for Z being Subset of REAL
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 REAL; :: 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 A2: m <= n ; :: thesis: f is_differentiable_on m,Z
now :: thesis: for i being Nat st i <= m - 1 holds
(diff (f,Z)) . i is_differentiable_on Z
A3: m - 1 <= n - 1 by A2, XREAL_1:13;
let i be Nat; :: thesis: ( i <= m - 1 implies (diff (f,Z)) . i is_differentiable_on Z )
assume i <= m - 1 ; :: thesis: (diff (f,Z)) . i is_differentiable_on Z
then i <= n - 1 by A3, XXREAL_0:2;
hence (diff (f,Z)) . i is_differentiable_on Z by A1; :: thesis: verum
end;
hence f is_differentiable_on m,Z ; :: thesis: verum