let n be non empty Element of NAT ; :: thesis: for i being Element of 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 Element of 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 = <*1*> as VECTOR of (REAL-NS 1) by A3, FINSEQ_2:118;
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 Pd2 = <*(partdiff g2,y,i)*> as Element of REAL 1 by FINSEQ_2:118;
reconsider Pd1 = <*(partdiff g1,y,i)*> as Element of REAL 1 by FINSEQ_2:118;
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:46;
rng g1 c= dom ((proj 1,1) " ) by Th2;
then A8: dom (((proj 1,1) " ) * g1) = dom g1 by RELAT_1:46;
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:46;

A12: now

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 8;
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 8;
x in dom f2 by A15, XBOOLE_0:def 4;
then A17: f2 /. x = (((proj 1,1) " ) * g2) . x by PARTFUN1:def 8;
x in dom g2 by A7, A15, XBOOLE_0:def 4;
then A18: f2 /. x = ((proj 1,1) " ) . (g2 . x) by A17, FUNCT_1:23;
x in dom g1 by A8, A15, XBOOLE_0:def 4;
then A19: f1 /. x = ((proj 1,1) " ) . (g1 . x) by A16, FUNCT_1:23;
(<>* (g1 - g2)) . x = ((proj 1,1) " ) . ((g1 - g2) . x) by A9, A11, A13, FUNCT_1:22;
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:46;
then A23: f1 - f2 = <>* (g1 - g2) by A6, A3, A12, PARTFUN1:34;
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:46
.= Pd1 - Pd2 by A5, A21, REAL_NS1:5
.= <*((partdiff g1,y,i) - (partdiff g2,y,i))*> by RVSUM_1:50 ;
then partdiff (g1 - g2),y,i = <*((partdiff g1,y,i) - (partdiff g2,y,i))*> . 1 by FINSEQ_1:57;
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, FINSEQ_1:57; :: thesis: verum