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

proof

assume f is_differentiable_on 0 ,X ; :: thesis: ( f is_differentiable_on 0 ,Z & diff (f,0,Z) = (diff (f,0,X)) | Z )
hence f is_differentiable_on 0 ,Z by A1, XBOOLE_1:1; :: thesis: diff (f,0,Z) = (diff (f,0,X)) | Z
A3: f | X = diff (f,0,X) by NDIFF_6:11;
thus diff (f,0,Z) = f | Z by NDIFF_6:11
.= (diff (f,0,X)) | Z by A1, A3, RELAT_1:74 ; :: 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: f is_differentiable_on i + 1,X ; :: thesis: ( f is_differentiable_on i + 1,Z & diff (f,(i + 1),Z) = (diff (f,(i + 1),X)) | Z )
A7: 0 + i <= i + 1 by XREAL_1:7;
for k being Nat st k <= (i + 1) - 1 holds
diff (f,k,Z) is_differentiable_on Z

proof

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

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

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

diff (f,i,X) is_differentiable_on X by A6, NDIFF_6:14;
then diff (f,i,X) is_differentiable_on Z by A1, NDIFF_1:46;
hence diff (f,k,Z) is_differentiable_on Z by A5, A6, A7, A9, Th3, NDIFF_6:17; :: thesis: verum

end;

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

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

end;

end;

end;

hence f is_differentiable_on i + 1,Z by A1, A6, NDIFF_6:14, XBOOLE_1:1; :: thesis: diff (f,(i + 1),Z) = (diff (f,(i + 1),X)) | Z
A10: diff (f,i,X) is_differentiable_on X by A6, NDIFF_6:14;
diff (f,(i + 1),Z) = ((diff (f,i,X)) | Z) `| Z by A5, A6, A7, NDIFF_6:13, NDIFF_6:17
.= (diff (f,i,X)) `| Z by A1, A10, Th4, NDIFF_1:46
.= ((diff (f,i,X)) `| X) | Z by A1, A10, Th5
.= (diff (f,(i + 1),X)) | Z by NDIFF_6:13 ;
hence diff (f,(i + 1),Z) = (diff (f,(i + 1),X)) | Z ; :: thesis: verum

end;

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