let f be PartFunc of REAL,REAL; for Z being Subset of REAL
for Z1 being open Subset of REAL st Z1 c= Z holds
for n being Nat st f is_differentiable_on n,Z holds
((diff (f,Z)) . n) | Z1 = (diff (f,Z1)) . n
let Z be Subset of REAL; for Z1 being open Subset of REAL st Z1 c= Z holds
for n being Nat st f is_differentiable_on n,Z holds
((diff (f,Z)) . n) | Z1 = (diff (f,Z1)) . n
let Z1 be open Subset of REAL; ( Z1 c= Z implies for n being Nat st f is_differentiable_on n,Z holds
((diff (f,Z)) . n) | Z1 = (diff (f,Z1)) . n )
assume A1:
Z1 c= Z
; for n being Nat st f is_differentiable_on n,Z holds
((diff (f,Z)) . n) | Z1 = (diff (f,Z1)) . n
defpred S1[ Nat] means ( f is_differentiable_on $1,Z implies ((diff (f,Z)) . $1) | Z1 = (diff (f,Z1)) . $1 );
A2:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A3:
S1[
k]
;
S1[k + 1]
assume A4:
f is_differentiable_on k + 1,
Z
;
((diff (f,Z)) . (k + 1)) | Z1 = (diff (f,Z1)) . (k + 1)
A5:
(diff (f,Z)) . k is_differentiable_on Z
by A4;
then A6:
(diff (f,Z)) . k is_differentiable_on Z1
by A1, FDIFF_1:26;
then A7:
dom (((diff (f,Z)) . k) `| Z1) = Z1
by FDIFF_1:def 7;
A8:
dom ((((diff (f,Z)) . k) `| Z) | Z1) =
(dom (((diff (f,Z)) . k) `| Z)) /\ Z1
by RELAT_1:61
.=
Z /\ Z1
by A5, FDIFF_1:def 7
.=
Z1
by A1, XBOOLE_1:28
;
A9:
now for x being Element of REAL st x in dom ((((diff (f,Z)) . k) `| Z) | Z1) holds
((((diff (f,Z)) . k) `| Z) | Z1) . x = (((diff (f,Z)) . k) `| Z1) . xlet x be
Element of
REAL ;
( x in dom ((((diff (f,Z)) . k) `| Z) | Z1) implies ((((diff (f,Z)) . k) `| Z) | Z1) . x = (((diff (f,Z)) . k) `| Z1) . x )assume A10:
x in dom ((((diff (f,Z)) . k) `| Z) | Z1)
;
((((diff (f,Z)) . k) `| Z) | Z1) . x = (((diff (f,Z)) . k) `| Z1) . xthus ((((diff (f,Z)) . k) `| Z) | Z1) . x =
(((diff (f,Z)) . k) `| Z) . x
by A8, A10, FUNCT_1:49
.=
diff (
((diff (f,Z)) . k),
x)
by A1, A5, A8, A10, FDIFF_1:def 7
.=
(((diff (f,Z)) . k) `| Z1) . x
by A6, A8, A10, FDIFF_1:def 7
;
verum end;
thus ((diff (f,Z)) . (k + 1)) | Z1 =
(((diff (f,Z)) . k) `| Z) | Z1
by Def5
.=
((diff (f,Z)) . k) `| Z1
by A8, A7, A9, PARTFUN1:5
.=
((diff (f,Z1)) . k) `| Z1
by A3, A4, A6, Th23, FDIFF_2:16, NAT_1:11
.=
(diff (f,Z1)) . (k + 1)
by Def5
;
verum
end;
A11:
S1[ 0 ]
thus
for k being Nat holds S1[k]
from NAT_1:sch 2(A11, A2); verum