let n be non empty Element of NAT ; :: thesis:
let i be Element of NAT ; :: thesis:
let g1, g2 be PartFunc of REAL n, REAL ; :: thesis:
let y be Element of REAL n; :: thesis:
assume A1: ( g1 is_partial_differentiable_in y,i & g2 is_partial_differentiable_in y,i ) ; :: thesis:
A2: ( the carrier of (REAL-NS n) = REAL n & 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) ;
reconsider x = y as Point of (REAL-NS n) by REAL_NS1:def 4;
( rng g1 c= dom ((proj 1,1) " ) & rng g2 c= dom ((proj 1,1) " ) ) by Th2;
then A3: ( dom (((proj 1,1) " ) * g1) = dom g1 & dom (((proj 1,1) " ) * g2) = dom g2 ) by RELAT_1:46;
then dom (f1 - f2) = (dom g1) /\ (dom g2) by VFUNCT_1:def 2;
then A4: dom (f1 - f2) = dom (g1 - g2) by VALUED_1:12;
A5: rng (g1 - g2) c= dom ((proj 1,1) " ) by Th2;
then A6: dom (((proj 1,1) " ) * (g1 - g2)) = dom (g1 - g2) by RELAT_1:46;
A7: dom (f1 - f2) = dom (<>* (g1 - g2)) by A4, A5, RELAT_1:46;

let x be Element of the carrier of (REAL-NS n); :: thesis:
assume A8: x in dom (f1 - f2) ; :: thesis:
then A9: x in (dom f1) /\ (dom f2) by VFUNCT_1:def 2;
then A10: ( x in dom f1 & x in dom f2 ) by XBOOLE_0:def 4;
A11: ( x in dom g1 & x in dom g2 ) by A3, A9, XBOOLE_0:def 4;
(f1 - f2) . x = (f1 - f2) /. x by A8, PARTFUN1:def 8;
then A12: (f1 - f2) . x = (f1 /. x) - (f2 /. x) by A8, VFUNCT_1:def 2;
(<>* (g1 - g2)) . x = ((proj 1,1) " ) . ((g1 - g2) . x) by A4, A6, A8, FUNCT_1:22;
then A13: (<>* (g1 - g2)) . x = ((proj 1,1) " ) . ((g1 . x) - (g2 . x)) by A4, A8, VALUED_1:13;
( f1 /. x = (((proj 1,1) " ) * g1) . x & f2 /. x = (((proj 1,1) " ) * g2) . x ) by A10, PARTFUN1:def 8;
then ( f1 /. x = ((proj 1,1) " ) . (g1 . x) & f2 /. x = ((proj 1,1) " ) . (g2 . x) ) by A11, FUNCT_1:23;
hence (f1 - f2) . x = (<>* (g1 - g2)) . x by A12, A13, Th2, Th3; :: thesis:

end;

then A14: f1 - f2 = <>* (g1 - g2) by A2, A7, PARTFUN1:34;
A15: ( f1 is_partial_differentiable_in x,i & f2 is_partial_differentiable_in x,i ) by A1, Th14;
then A16: f1 - f2 is_partial_differentiable_in x,i by Th30;
reconsider One = <*1*> as VECTOR of (REAL-NS 1) by A2, FINSEQ_2:118;
A17: ( (partdiff f1,x,i) . One = <*(partdiff g1,y,i)*> & (partdiff f2,x,i) . One = <*(partdiff g2,y,i)*> ) by A15, Th15;
reconsider Pd1 = <*(partdiff g1,y,i)*> as Element of REAL 1 by FINSEQ_2:118;
reconsider Pd2 = <*(partdiff g2,y,i)*> as Element of REAL 1 by FINSEQ_2:118;
<*(partdiff (g1 - g2),y,i)*> = (partdiff (f1 - f2),x,i) . <*1*> by A14, A16, Th15
.= ((partdiff f1,x,i) - (partdiff f2,x,i)) . <*1*> by A15, Th30
.= ((partdiff f1,x,i) . One) - ((partdiff f2,x,i) . One) by LOPBAN_1:46
.= Pd1 - Pd2 by A17, 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 A14, A16, Th14, FINSEQ_1:57; :: thesis: