let S, T be RealNormSpace; for Z being Subset of S st Z is open holds
for f1, f2 being PartFunc of S,T st Z c= dom (f1 - f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds
( f1 - f2 is_differentiable_on Z & ( for x being Point of S st x in Z holds
((f1 - f2) `| Z) /. x = (diff (f1,x)) - (diff (f2,x)) ) )
let Z be Subset of S; ( Z is open implies for f1, f2 being PartFunc of S,T st Z c= dom (f1 - f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds
( f1 - f2 is_differentiable_on Z & ( for x being Point of S st x in Z holds
((f1 - f2) `| Z) /. x = (diff (f1,x)) - (diff (f2,x)) ) ) )
assume A1:
Z is open
; for f1, f2 being PartFunc of S,T st Z c= dom (f1 - f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds
( f1 - f2 is_differentiable_on Z & ( for x being Point of S st x in Z holds
((f1 - f2) `| Z) /. x = (diff (f1,x)) - (diff (f2,x)) ) )
let f1, f2 be PartFunc of S,T; ( Z c= dom (f1 - f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z implies ( f1 - f2 is_differentiable_on Z & ( for x being Point of S st x in Z holds
((f1 - f2) `| Z) /. x = (diff (f1,x)) - (diff (f2,x)) ) ) )
assume that
A2:
Z c= dom (f1 - f2)
and
A3:
( f1 is_differentiable_on Z & f2 is_differentiable_on Z )
; ( f1 - f2 is_differentiable_on Z & ( for x being Point of S st x in Z holds
((f1 - f2) `| Z) /. x = (diff (f1,x)) - (diff (f2,x)) ) )
hence A4:
f1 - f2 is_differentiable_on Z
by A1, A2, Th31; for x being Point of S st x in Z holds
((f1 - f2) `| Z) /. x = (diff (f1,x)) - (diff (f2,x))
now for x being Point of S st x in Z holds
((f1 - f2) `| Z) /. x = (diff (f1,x)) - (diff (f2,x))let x be
Point of
S;
( x in Z implies ((f1 - f2) `| Z) /. x = (diff (f1,x)) - (diff (f2,x)) )assume A5:
x in Z
;
((f1 - f2) `| Z) /. x = (diff (f1,x)) - (diff (f2,x))then A6:
(
f1 is_differentiable_in x &
f2 is_differentiable_in x )
by A1, A3, Th31;
thus ((f1 - f2) `| Z) /. x =
diff (
(f1 - f2),
x)
by A4, A5, Def9
.=
(diff (f1,x)) - (diff (f2,x))
by A6, Th36
;
verum end;
hence
for x being Point of S st x in Z holds
((f1 - f2) `| Z) /. x = (diff (f1,x)) - (diff (f2,x))
; verum