let S, T be RealNormSpace; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: ( 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)) ) )

now :: thesis: for x0 being Point of S st x0 in Z holds
f1 - f2 is_differentiable_in x0
end;
hence A4: f1 - f2 is_differentiable_on Z by A1, A2, Th31; :: thesis: for x being Point of S st x in Z holds
((f1 - f2) `| Z) /. x = (diff (f1,x)) - (diff (f2,x))

now :: thesis: 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; :: thesis: ( x in Z implies ((f1 - f2) `| Z) /. x = (diff (f1,x)) - (diff (f2,x)) )
assume A5: x in Z ; :: thesis: ((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 ; :: thesis: verum
end;
hence for x being Point of S st x in Z holds
((f1 - f2) `| Z) /. x = (diff (f1,x)) - (diff (f2,x)) ; :: thesis: verum