let x0 be Real; :: thesis: for n being non zero Element of NAT
for f1, f2 being PartFunc of REAL,(REAL n) st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds
( f1 - f2 is_differentiable_in x0 & diff ((f1 - f2),x0) = (diff (f1,x0)) - (diff (f2,x0)) )
let n be non zero Element of NAT ; :: thesis: for f1, f2 being PartFunc of REAL,(REAL n) st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds
( f1 - f2 is_differentiable_in x0 & diff ((f1 - f2),x0) = (diff (f1,x0)) - (diff (f2,x0)) )
let f1, f2 be PartFunc of REAL,(REAL n); :: thesis: ( f1 is_differentiable_in x0 & f2 is_differentiable_in x0 implies ( f1 - f2 is_differentiable_in x0 & diff ((f1 - f2),x0) = (diff (f1,x0)) - (diff (f2,x0)) ) )
A1: f1 - f2 = f1 + (- f2) by Th1;
assume A2: f1 is_differentiable_in x0 ; :: thesis: ( not f2 is_differentiable_in x0 or ( f1 - f2 is_differentiable_in x0 & diff ((f1 - f2),x0) = (diff (f1,x0)) - (diff (f2,x0)) ) )
assume f2 is_differentiable_in x0 ; :: thesis: ( f1 - f2 is_differentiable_in x0 & diff ((f1 - f2),x0) = (diff (f1,x0)) - (diff (f2,x0)) )
then ( - f2 is_differentiable_in x0 & diff ((- f2),x0) = - (diff (f2,x0)) ) by Th10;
hence ( f1 - f2 is_differentiable_in x0 & diff ((f1 - f2),x0) = (diff (f1,x0)) - (diff (f2,x0)) ) by A1, A2, Th11; :: thesis: verum