let n be non zero Nat; :: thesis: for i being Nat
for g1, g2 being PartFunc of (REAL n),REAL
for y being Element of REAL n st g1 is_partial_differentiable_in y,i & g2 is_partial_differentiable_in y,i holds
( g1 - g2 is_partial_differentiable_in y,i & partdiff ((g1 - g2),y,i) = (partdiff (g1,y,i)) - (partdiff (g2,y,i)) )
let i be Nat; :: thesis: for g1, g2 being PartFunc of (REAL n),REAL
for y being Element of REAL n st g1 is_partial_differentiable_in y,i & g2 is_partial_differentiable_in y,i holds
( g1 - g2 is_partial_differentiable_in y,i & partdiff ((g1 - g2),y,i) = (partdiff (g1,y,i)) - (partdiff (g2,y,i)) )
let g1, g2 be PartFunc of (REAL n),REAL; :: thesis: for y being Element of REAL n st g1 is_partial_differentiable_in y,i & g2 is_partial_differentiable_in y,i holds
( g1 - g2 is_partial_differentiable_in y,i & partdiff ((g1 - g2),y,i) = (partdiff (g1,y,i)) - (partdiff (g2,y,i)) )
let y be Element of REAL n; :: thesis: ( g1 is_partial_differentiable_in y,i & g2 is_partial_differentiable_in y,i implies ( g1 - g2 is_partial_differentiable_in y,i & partdiff ((g1 - g2),y,i) = (partdiff (g1,y,i)) - (partdiff (g2,y,i)) ) )
assume that
A1: g1 is_partial_differentiable_in y,i and
A2: g2 is_partial_differentiable_in y,i ; :: thesis: ( g1 - g2 is_partial_differentiable_in y,i & partdiff ((g1 - g2),y,i) = (partdiff (g1,y,i)) - (partdiff (g2,y,i)) )
reconsider x = y as Point of (REAL-NS n) by REAL_NS1:def 4;
A3: the carrier of (REAL-NS 1) = REAL 1 by REAL_NS1:def 4;
then reconsider f1 = <>* g1, f2 = <>* g2 as PartFunc of (REAL-NS n),(REAL-NS 1) by REAL_NS1:def 4;
reconsider One = <*jj*> as VECTOR of (REAL-NS 1) by A3, FINSEQ_2:98;
A4: f1 is_partial_differentiable_in x,i by A1, Th14;
then A5: (partdiff (f1,x,i)) . One = <*(partdiff (g1,y,i))*> by Th15;
reconsider d2 = partdiff (g2,y,i) as Element of REAL by XREAL_0:def 1;
reconsider Pd2 = <*d2*> as Element of REAL 1 by FINSEQ_2:98;
reconsider d1 = partdiff (g1,y,i) as Element of REAL by XREAL_0:def 1;
reconsider Pd1 = <*d1*> as Element of REAL 1 by FINSEQ_2:98;
A6: the carrier of (REAL-NS n) = REAL n by REAL_NS1:def 4;
rng g2 c= dom ((proj (1,1)) ") by Th2;
then A7: dom (((proj (1,1)) ") * g2) = dom g2 by RELAT_1:27;
rng g1 c= dom ((proj (1,1)) ") by Th2;
then A8: dom (((proj (1,1)) ") * g1) = dom g1 by RELAT_1:27;
then dom (f1 - f2) = (dom g1) /\ (dom g2) by A7, VFUNCT_1:def 2;
then A9: dom (f1 - f2) = dom (g1 - g2) by VALUED_1:12;
A10: rng (g1 - g2) c= dom ((proj (1,1)) ") by Th2;
then A11: dom (((proj (1,1)) ") * (g1 - g2)) = dom (g1 - g2) by RELAT_1:27;

A12: now :: thesis: for x being Element of (REAL-NS n) st x in dom (f1 - f2) holds
(f1 - f2) . x = (<>* (g1 - g2)) . x

let x be Element of (REAL-NS n); :: thesis: ( x in dom (f1 - f2) implies (f1 - f2) . x = (<>* (g1 - g2)) . x )
assume A13: x in dom (f1 - f2) ; :: thesis: (f1 - f2) . x = (<>* (g1 - g2)) . x
then (f1 - f2) . x = (f1 - f2) /. x by PARTFUN1:def 6;
then A14: (f1 - f2) . x = (f1 /. x) - (f2 /. x) by A13, VFUNCT_1:def 2;
A15: x in (dom f1) /\ (dom f2) by A13, VFUNCT_1:def 2;
then x in dom f1 by XBOOLE_0:def 4;
then A16: f1 /. x = (((proj (1,1)) ") * g1) . x by PARTFUN1:def 6;
x in dom f2 by A15, XBOOLE_0:def 4;
then A17: f2 /. x = (((proj (1,1)) ") * g2) . x by PARTFUN1:def 6;
x in dom g2 by A7, A15, XBOOLE_0:def 4;
then A18: f2 /. x = ((proj (1,1)) ") . (g2 . x) by A17, FUNCT_1:13;
x in dom g1 by A8, A15, XBOOLE_0:def 4;
then A19: f1 /. x = ((proj (1,1)) ") . (g1 . x) by A16, FUNCT_1:13;
(<>* (g1 - g2)) . x = ((proj (1,1)) ") . ((g1 - g2) . x) by A9, A11, A13, FUNCT_1:12;
then (<>* (g1 - g2)) . x = ((proj (1,1)) ") . ((g1 . x) - (g2 . x)) by A9, A13, VALUED_1:13;
hence (f1 - f2) . x = (<>* (g1 - g2)) . x by A14, A19, A18, Th2, Th3; :: thesis: verum

end;

A20: f2 is_partial_differentiable_in x,i by A2, Th14;
then A21: (partdiff (f2,x,i)) . One = <*(partdiff (g2,y,i))*> by Th15;
A22: f1 - f2 is_partial_differentiable_in x,i by A4, A20, Th30;
dom (f1 - f2) = dom (<>* (g1 - g2)) by A9, A10, RELAT_1:27;
then A23: f1 - f2 = <>* (g1 - g2) by A6, A3, A12, PARTFUN1:5;
then <*(partdiff ((g1 - g2),y,i))*> = (partdiff ((f1 - f2),x,i)) . <*1*> by A4, A20, Th15, Th30
.= ((partdiff (f1,x,i)) - (partdiff (f2,x,i))) . <*1*> by A4, A20, Th30
.= ((partdiff (f1,x,i)) . One) - ((partdiff (f2,x,i)) . One) by LOPBAN_1:40
.= Pd1 - Pd2 by A5, A21, REAL_NS1:5
.= <*((partdiff (g1,y,i)) - (partdiff (g2,y,i)))*> by RVSUM_1:29 ;
then partdiff ((g1 - g2),y,i) = <*((partdiff (g1,y,i)) - (partdiff (g2,y,i)))*> . 1 ;
hence ( g1 - g2 is_partial_differentiable_in y,i & partdiff ((g1 - g2),y,i) = (partdiff (g1,y,i)) - (partdiff (g2,y,i)) ) by A23, A22, Th14; :: thesis: verum