let f be PartFunc of REAL,REAL; :: thesis: for Z being Subset of REAL
for n being natural number st f is_differentiable_on n,Z holds
for m being natural number st m <= n holds
f is_differentiable_on m,Z
let Z be Subset of REAL; :: thesis: for n being natural number st f is_differentiable_on n,Z holds
for m being natural number st m <= n holds
f is_differentiable_on m,Z
let n be natural number ; :: thesis: ( f is_differentiable_on n,Z implies for m being natural number st m <= n holds
f is_differentiable_on m,Z )
assume A1: f is_differentiable_on n,Z ; :: thesis: for m being natural number st m <= n holds
f is_differentiable_on m,Z
let m be natural number ; :: thesis: ( m <= n implies f is_differentiable_on m,Z )
assume A2: m <= n ; :: thesis: f is_differentiable_on m,Z

now

A3: m - 1 <= n - 1 by A2, XREAL_1:13;
let i be Element of 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, Def6; :: thesis: verum

end;

hence f is_differentiable_on m,Z by Def6; :: thesis: verum