let i be Element of NAT ; :: thesis: for n being non zero Element of NAT

for g being PartFunc of REAL,(REAL-NS n)

for x0 being Real st 1 <= i & i <= n & g is_differentiable_in x0 holds

( (Proj (i,n)) * g is_differentiable_in x0 & (Proj (i,n)) . (diff (g,x0)) = diff (((Proj (i,n)) * g),x0) )

let n be non zero Element of NAT ; :: thesis: for g being PartFunc of REAL,(REAL-NS n)

for x0 being Real st 1 <= i & i <= n & g is_differentiable_in x0 holds

( (Proj (i,n)) * g is_differentiable_in x0 & (Proj (i,n)) . (diff (g,x0)) = diff (((Proj (i,n)) * g),x0) )

let g be PartFunc of REAL,(REAL-NS n); :: thesis: for x0 being Real st 1 <= i & i <= n & g is_differentiable_in x0 holds

( (Proj (i,n)) * g is_differentiable_in x0 & (Proj (i,n)) . (diff (g,x0)) = diff (((Proj (i,n)) * g),x0) )

let x0 be Real; :: thesis: ( 1 <= i & i <= n & g is_differentiable_in x0 implies ( (Proj (i,n)) * g is_differentiable_in x0 & (Proj (i,n)) . (diff (g,x0)) = diff (((Proj (i,n)) * g),x0) ) )

assume A1: ( 1 <= i & i <= n & g is_differentiable_in x0 ) ; :: thesis: ( (Proj (i,n)) * g is_differentiable_in x0 & (Proj (i,n)) . (diff (g,x0)) = diff (((Proj (i,n)) * g),x0) )

then consider N being Neighbourhood of x0 such that

A2: ( N c= dom g & ex DFG being LinearFunc of (REAL-NS n) ex GR being RestFunc of (REAL-NS n) st

( diff (g,x0) = DFG /. 1 & ( for x being Real st x in N holds

(g /. x) - (g /. x0) = (DFG /. (x - x0)) + (GR /. (x - x0)) ) ) ) by NDIFF_3:def 4;

consider GR being RestFunc of (REAL-NS n), DFG being LinearFunc of (REAL-NS n) such that

A3: ( diff (g,x0) = DFG /. 1 & ( for x being Real st x in N holds

(g /. x) - (g /. x0) = (DFG /. (x - x0)) + (GR /. (x - x0)) ) ) by A2;

consider LP being Point of (REAL-NS n) such that

A4: for p being Real holds DFG /. p = p * LP by NDIFF_3:def 2;

reconsider PG = Proj (i,n) as Function of (REAL-NS n),(REAL-NS 1) ;

reconsider L = (Proj (i,n)) * DFG as Function of REAL,(REAL-NS 1) ;

A5: for r being Real holds L /. r = r * ((Proj (i,n)) . LP)

A7: GR is total by NDIFF_3:def 1;

then reconsider FGR = GR as Function of REAL,(REAL-NS n) ;

A8: (Proj (i,n)) * FGR is Function of REAL,(REAL-NS 1) ;

(Proj (i,n)) * GR is RestFunc of (REAL-NS 1)

set pg = (Proj (i,n)) * g;

A20: dom (Proj (i,n)) = the carrier of (REAL-NS n) by FUNCT_2:def 1;

then rng g c= dom (Proj (i,n)) ;

then A21: dom g = dom ((Proj (i,n)) * g) by RELAT_1:27;

A22: dom (Proj (i,n)) = REAL n by A20, REAL_NS1:def 4;

A23: for x being Real st x in N holds

(((Proj (i,n)) * g) /. x) - (((Proj (i,n)) * g) /. x0) = (L /. (x - x0)) + (R /. (x - x0))

L /. jj = 1 * ((Proj (i,n)) . LP) by A5

.= (Proj (i,n)) . LP by RLVECT_1:def 8

.= (Proj (i,n)) . (1 * LP) by RLVECT_1:def 8

.= (Proj (i,n)) . (diff (g,x0)) by A3, A4 ;

hence (Proj (i,n)) . (diff (g,x0)) = diff (((Proj (i,n)) * g),x0) by A39, A2, A21, A23, NDIFF_3:def 4; :: thesis: verum

for g being PartFunc of REAL,(REAL-NS n)

for x0 being Real st 1 <= i & i <= n & g is_differentiable_in x0 holds

( (Proj (i,n)) * g is_differentiable_in x0 & (Proj (i,n)) . (diff (g,x0)) = diff (((Proj (i,n)) * g),x0) )

let n be non zero Element of NAT ; :: thesis: for g being PartFunc of REAL,(REAL-NS n)

for x0 being Real st 1 <= i & i <= n & g is_differentiable_in x0 holds

( (Proj (i,n)) * g is_differentiable_in x0 & (Proj (i,n)) . (diff (g,x0)) = diff (((Proj (i,n)) * g),x0) )

let g be PartFunc of REAL,(REAL-NS n); :: thesis: for x0 being Real st 1 <= i & i <= n & g is_differentiable_in x0 holds

( (Proj (i,n)) * g is_differentiable_in x0 & (Proj (i,n)) . (diff (g,x0)) = diff (((Proj (i,n)) * g),x0) )

let x0 be Real; :: thesis: ( 1 <= i & i <= n & g is_differentiable_in x0 implies ( (Proj (i,n)) * g is_differentiable_in x0 & (Proj (i,n)) . (diff (g,x0)) = diff (((Proj (i,n)) * g),x0) ) )

assume A1: ( 1 <= i & i <= n & g is_differentiable_in x0 ) ; :: thesis: ( (Proj (i,n)) * g is_differentiable_in x0 & (Proj (i,n)) . (diff (g,x0)) = diff (((Proj (i,n)) * g),x0) )

then consider N being Neighbourhood of x0 such that

A2: ( N c= dom g & ex DFG being LinearFunc of (REAL-NS n) ex GR being RestFunc of (REAL-NS n) st

( diff (g,x0) = DFG /. 1 & ( for x being Real st x in N holds

(g /. x) - (g /. x0) = (DFG /. (x - x0)) + (GR /. (x - x0)) ) ) ) by NDIFF_3:def 4;

consider GR being RestFunc of (REAL-NS n), DFG being LinearFunc of (REAL-NS n) such that

A3: ( diff (g,x0) = DFG /. 1 & ( for x being Real st x in N holds

(g /. x) - (g /. x0) = (DFG /. (x - x0)) + (GR /. (x - x0)) ) ) by A2;

consider LP being Point of (REAL-NS n) such that

A4: for p being Real holds DFG /. p = p * LP by NDIFF_3:def 2;

reconsider PG = Proj (i,n) as Function of (REAL-NS n),(REAL-NS 1) ;

reconsider L = (Proj (i,n)) * DFG as Function of REAL,(REAL-NS 1) ;

A5: for r being Real holds L /. r = r * ((Proj (i,n)) . LP)

proof

then reconsider L = L as LinearFunc of (REAL-NS 1) by NDIFF_3:def 2;
let r be Real; :: thesis: L /. r = r * ((Proj (i,n)) . LP)

reconsider r = r as Element of REAL by XREAL_0:def 1;

A6: dom L = REAL by FUNCT_2:def 1;

DFG /. r = r * LP by A4;

then (Proj (i,n)) . (DFG /. r) = r * ((Proj (i,n)) . LP) by PDIFF_6:27;

then L /. r = r * ((Proj (i,n)) . LP) by A6, FUNCT_1:12;

hence L /. r = r * ((Proj (i,n)) . LP) ; :: thesis: verum

end;reconsider r = r as Element of REAL by XREAL_0:def 1;

A6: dom L = REAL by FUNCT_2:def 1;

DFG /. r = r * LP by A4;

then (Proj (i,n)) . (DFG /. r) = r * ((Proj (i,n)) . LP) by PDIFF_6:27;

then L /. r = r * ((Proj (i,n)) . LP) by A6, FUNCT_1:12;

hence L /. r = r * ((Proj (i,n)) . LP) ; :: thesis: verum

A7: GR is total by NDIFF_3:def 1;

then reconsider FGR = GR as Function of REAL,(REAL-NS n) ;

A8: (Proj (i,n)) * FGR is Function of REAL,(REAL-NS 1) ;

(Proj (i,n)) * GR is RestFunc of (REAL-NS 1)

proof

then reconsider R = (Proj (i,n)) * GR as RestFunc of (REAL-NS 1) ;
A9:
dom GR = REAL
by A7, PARTFUN1:def 2;

reconsider R = (Proj (i,n)) * GR as PartFunc of REAL,(REAL-NS 1) ;

for r being Real st r > 0 holds

ex d being Real st

( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds

(|.z.| ") * ||.(R /. z).|| < r ) )

end;reconsider R = (Proj (i,n)) * GR as PartFunc of REAL,(REAL-NS 1) ;

for r being Real st r > 0 holds

ex d being Real st

( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds

(|.z.| ") * ||.(R /. z).|| < r ) )

proof

hence
(Proj (i,n)) * GR is RestFunc of (REAL-NS 1)
by A8, Th23; :: thesis: verum
let r be Real; :: thesis: ( r > 0 implies ex d being Real st

( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds

(|.z.| ") * ||.(R /. z).|| < r ) ) )

assume r > 0 ; :: thesis: ex d being Real st

( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds

(|.z.| ") * ||.(R /. z).|| < r ) )

then consider d being Real such that

A10: ( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds

(|.z.| ") * ||.(GR /. z).|| < r ) ) by A7, Th23;

take d ; :: thesis: ( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds

(|.z.| ") * ||.(R /. z).|| < r ) )

thus d > 0 by A10; :: thesis: for z being Real st z <> 0 & |.z.| < d holds

(|.z.| ") * ||.(R /. z).|| < r

let z be Real; :: thesis: ( z <> 0 & |.z.| < d implies (|.z.| ") * ||.(R /. z).|| < r )

assume A11: ( z <> 0 & |.z.| < d ) ; :: thesis: (|.z.| ") * ||.(R /. z).|| < r

reconsider z = z as Element of REAL by XREAL_0:def 1;

A12: GR /. z = GR . z by A9, PARTFUN1:def 6;

A13: i in Seg n by A1;

reconsider GRz = GR /. z as Point of (REAL-NS n) ;

reconsider GRz1 = GRz as Element of REAL n by REAL_NS1:def 4;

reconsider GRzi = GRz1 . i as Element of REAL by XREAL_0:def 1;

dom (Proj (i,n)) = the carrier of (REAL-NS n) by PARTFUN1:def 2;

then A14: z in dom ((Proj (i,n)) * GR) by A9, A12, FUNCT_1:11;

then ((Proj (i,n)) * GR) . z = (Proj (i,n)) . (GR . z) by FUNCT_1:12

.= <*((proj (i,n)) . GRz1)*> by A12, PDIFF_1:def 4 ;

then A15: ((Proj (i,n)) * GR) . z = <*GRzi*> by PDIFF_1:def 1;

A16: |.GRzi.| <= ||.(GR /. z).|| by A13, REAL_NS1:9;

A17: 0 <= |.z.| by COMPLEX1:46;

0 <= |.GRzi.| by COMPLEX1:46;

then A18: (|.z.| ") * |.GRzi.| <= (|.z.| ") * ||.(GR /. z).|| by A16, A17, XREAL_1:66;

(|.z.| ") * ||.(GR /. z).|| < r by A10, A11;

then A19: (|.z.| ") * |.GRzi.| < r by A18, XXREAL_0:2;

((Proj (i,n)) * GR) . z in rng ((Proj (i,n)) * GR) by A14, FUNCT_1:3;

then reconsider Rz = ((Proj (i,n)) * GR) . z as VECTOR of (REAL-NS 1) ;

set VGRzi = <*GRzi*>;

<*GRzi*> is Element of REAL 1 by FINSEQ_2:98;

then ||.Rz.|| = |.<*GRzi*>.| by A15, REAL_NS1:1;

then (|.z.| ") * ||.Rz.|| < r by A19, JORDAN2C:10;

hence (|.z.| ") * ||.(R /. z).|| < r by A14, PARTFUN1:def 6; :: thesis: verum

end;( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds

(|.z.| ") * ||.(R /. z).|| < r ) ) )

assume r > 0 ; :: thesis: ex d being Real st

( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds

(|.z.| ") * ||.(R /. z).|| < r ) )

then consider d being Real such that

A10: ( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds

(|.z.| ") * ||.(GR /. z).|| < r ) ) by A7, Th23;

take d ; :: thesis: ( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds

(|.z.| ") * ||.(R /. z).|| < r ) )

thus d > 0 by A10; :: thesis: for z being Real st z <> 0 & |.z.| < d holds

(|.z.| ") * ||.(R /. z).|| < r

let z be Real; :: thesis: ( z <> 0 & |.z.| < d implies (|.z.| ") * ||.(R /. z).|| < r )

assume A11: ( z <> 0 & |.z.| < d ) ; :: thesis: (|.z.| ") * ||.(R /. z).|| < r

reconsider z = z as Element of REAL by XREAL_0:def 1;

A12: GR /. z = GR . z by A9, PARTFUN1:def 6;

A13: i in Seg n by A1;

reconsider GRz = GR /. z as Point of (REAL-NS n) ;

reconsider GRz1 = GRz as Element of REAL n by REAL_NS1:def 4;

reconsider GRzi = GRz1 . i as Element of REAL by XREAL_0:def 1;

dom (Proj (i,n)) = the carrier of (REAL-NS n) by PARTFUN1:def 2;

then A14: z in dom ((Proj (i,n)) * GR) by A9, A12, FUNCT_1:11;

then ((Proj (i,n)) * GR) . z = (Proj (i,n)) . (GR . z) by FUNCT_1:12

.= <*((proj (i,n)) . GRz1)*> by A12, PDIFF_1:def 4 ;

then A15: ((Proj (i,n)) * GR) . z = <*GRzi*> by PDIFF_1:def 1;

A16: |.GRzi.| <= ||.(GR /. z).|| by A13, REAL_NS1:9;

A17: 0 <= |.z.| by COMPLEX1:46;

0 <= |.GRzi.| by COMPLEX1:46;

then A18: (|.z.| ") * |.GRzi.| <= (|.z.| ") * ||.(GR /. z).|| by A16, A17, XREAL_1:66;

(|.z.| ") * ||.(GR /. z).|| < r by A10, A11;

then A19: (|.z.| ") * |.GRzi.| < r by A18, XXREAL_0:2;

((Proj (i,n)) * GR) . z in rng ((Proj (i,n)) * GR) by A14, FUNCT_1:3;

then reconsider Rz = ((Proj (i,n)) * GR) . z as VECTOR of (REAL-NS 1) ;

set VGRzi = <*GRzi*>;

<*GRzi*> is Element of REAL 1 by FINSEQ_2:98;

then ||.Rz.|| = |.<*GRzi*>.| by A15, REAL_NS1:1;

then (|.z.| ") * ||.Rz.|| < r by A19, JORDAN2C:10;

hence (|.z.| ") * ||.(R /. z).|| < r by A14, PARTFUN1:def 6; :: thesis: verum

set pg = (Proj (i,n)) * g;

A20: dom (Proj (i,n)) = the carrier of (REAL-NS n) by FUNCT_2:def 1;

then rng g c= dom (Proj (i,n)) ;

then A21: dom g = dom ((Proj (i,n)) * g) by RELAT_1:27;

A22: dom (Proj (i,n)) = REAL n by A20, REAL_NS1:def 4;

A23: for x being Real st x in N holds

(((Proj (i,n)) * g) /. x) - (((Proj (i,n)) * g) /. x0) = (L /. (x - x0)) + (R /. (x - x0))

proof

hence A39:
(Proj (i,n)) * g is_differentiable_in x0
by A2, A21, NDIFF_3:def 3; :: thesis: (Proj (i,n)) . (diff (g,x0)) = diff (((Proj (i,n)) * g),x0)
let x be Real; :: thesis: ( x in N implies (((Proj (i,n)) * g) /. x) - (((Proj (i,n)) * g) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) )

end;now :: thesis: ( x in N & x in N implies (((Proj (i,n)) * g) /. x) - (((Proj (i,n)) * g) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) )

hence
( x in N implies (((Proj (i,n)) * g) /. x) - (((Proj (i,n)) * g) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) )
; :: thesis: verumassume A24:
x in N
; :: thesis: ( x in N implies (((Proj (i,n)) * g) /. x) - (((Proj (i,n)) * g) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) )

then A25: (g /. x) - (g /. x0) = (DFG /. (x - x0)) + (GR /. (x - x0)) by A3;

A26: x0 in N by RCOMP_1:16;

then A27: ( ((Proj (i,n)) * g) /. x = ((Proj (i,n)) * g) . x & ((Proj (i,n)) * g) /. x0 = ((Proj (i,n)) * g) . x0 ) by A2, A21, A24, PARTFUN1:def 6;

A28: ( g /. x = g . x & g /. x0 = g . x0 ) by A2, A24, A26, PARTFUN1:def 6;

reconsider PGSx = (((Proj (i,n)) * g) /. x) - (((Proj (i,n)) * g) /. x0) as Element of REAL 1 by REAL_NS1:def 4;

((Proj (i,n)) * g) . x in rng ((Proj (i,n)) * g) by A2, A21, A24, FUNCT_1:3;

then reconsider PGdx = ((Proj (i,n)) * g) . x as Element of REAL 1 by REAL_NS1:def 4;

((Proj (i,n)) * g) . x0 in rng ((Proj (i,n)) * g) by A2, A21, A26, FUNCT_1:3;

then reconsider PGdx0 = ((Proj (i,n)) * g) . x0 as Element of REAL 1 by REAL_NS1:def 4;

g . x in rng g by A2, A24, FUNCT_1:3;

then reconsider Gx = g . x as Element of REAL n by REAL_NS1:def 4;

g . x0 in rng g by A2, A26, FUNCT_1:3;

then reconsider Gx0 = g . x0 as Element of REAL n by REAL_NS1:def 4;

set ProjGx = (Proj (i,n)) . (g . x);

Gx in dom (Proj (i,n)) by A22;

then (Proj (i,n)) . (g . x) in rng (Proj (i,n)) by FUNCT_1:3;

then reconsider ProjGx = (Proj (i,n)) . (g . x) as Element of REAL 1 by REAL_NS1:def 4;

set ProjGx0 = (Proj (i,n)) . (g . x0);

Gx0 in dom (Proj (i,n)) by A22;

then (Proj (i,n)) . (g . x0) in rng (Proj (i,n)) by FUNCT_1:3;

then reconsider ProjGx0 = (Proj (i,n)) . (g . x0) as Element of REAL 1 by REAL_NS1:def 4;

reconsider Gx1 = Gx as Element of (REAL-NS n) by REAL_NS1:def 4;

reconsider Gx01 = Gx0 as Element of (REAL-NS n) by REAL_NS1:def 4;

reconsider Gsx = g /. x as Element of REAL n by REAL_NS1:def 4;

reconsider Gsx0 = g /. x0 as Element of REAL n by REAL_NS1:def 4;

reconsider dxx0 = x - x0 as Element of REAL by XREAL_0:def 1;

reconsider Ldxx0 = L /. (x - x0) as Element of (REAL-NS 1) ;

A29: dom R = REAL by A8, PARTFUN1:def 2;

then A30: R /. (x - x0) = R . dxx0 by PARTFUN1:def 6;

then reconsider Rdxx0 = R . (x - x0) as Element of (REAL-NS 1) ;

reconsider Lxx0Rxx0 = (L /. (x - x0)) + (R /. (x - x0)) as Element of REAL 1 by REAL_NS1:def 4;

reconsider Ldiff = DFG /. (x - x0) as Element of REAL n by REAL_NS1:def 4;

dom DFG = REAL by FUNCT_2:def 1;

then A31: Ldiff = DFG . dxx0 by PARTFUN1:def 6;

set ProjLdiff = (Proj (i,n)) . Ldiff;

(Proj (i,n)) . Ldiff in rng (Proj (i,n)) by A20, FUNCT_1:3;

then reconsider ProjLdiff = (Proj (i,n)) . Ldiff as Element of REAL 1 by REAL_NS1:def 4;

A32: dom GR = REAL by A7, PARTFUN1:def 2;

then GR . dxx0 in rng GR by FUNCT_1:3;

then reconsider Rdiff = GR . dxx0 as Element of REAL n by REAL_NS1:def 4;

A33: Rdiff = GR /. dxx0 by A32, PARTFUN1:def 6;

set ProjRdiff = (Proj (i,n)) . Rdiff;

(Proj (i,n)) . Rdiff in rng (Proj (i,n)) by A22, FUNCT_1:3;

then reconsider ProjRdiff = (Proj (i,n)) . Rdiff as Element of REAL 1 by REAL_NS1:def 4;

dom L = REAL by FUNCT_2:def 1;

then A34: dxx0 in dom L ;

A35: L /. dxx0 = L . dxx0

.= (Proj (i,n)) . (DFG . dxx0) by A34, FUNCT_1:12

.= (Proj (i,n)) . Ldiff by A31 ;

R . (x - x0) = (Proj (i,n)) . Rdiff by A29, FUNCT_1:12;

then A36: Ldxx0 + Rdxx0 = ProjLdiff + ProjRdiff by A35, REAL_NS1:2;

(Proj (i,n)) . Ldiff = <*((proj (i,n)) . Ldiff)*> by PDIFF_1:def 4;

then A37: (Proj (i,n)) . Ldiff = <*(Ldiff . i)*> by PDIFF_1:def 1;

Rdiff in dom (Proj (i,n)) by A22;

then (Proj (i,n)) . Rdiff = <*((proj (i,n)) . Rdiff)*> by PDIFF_1:def 4;

then A38: (Proj (i,n)) . Rdiff = <*(Rdiff . i)*> by PDIFF_1:def 1;

reconsider diffGR = (DFG /. (x - x0)) + (GR /. (x - x0)) as Element of REAL n by REAL_NS1:def 4;

reconsider Rsdiff = GR /. (x - x0) as Element of REAL n by REAL_NS1:def 4;

PGSx = PGdx - PGdx0 by A27, REAL_NS1:5

.= ProjGx - PGdx0 by A2, A21, A24, FUNCT_1:12

.= ProjGx - ProjGx0 by A2, A21, A26, FUNCT_1:12

.= <*((proj (i,n)) . Gx1)*> - ProjGx0 by PDIFF_1:def 4

.= <*((proj (i,n)) . Gx1)*> - <*((proj (i,n)) . Gx01)*> by PDIFF_1:def 4

.= <*(Gx . i)*> - <*((proj (i,n)) . Gx01)*> by PDIFF_1:def 1

.= <*(Gx . i)*> - <*(Gx0 . i)*> by PDIFF_1:def 1

.= <*((Gx . i) - (Gx0 . i))*> by RVSUM_1:29

.= <*((Gsx - Gsx0) . i)*> by A28, RVSUM_1:27

.= <*(diffGR . i)*> by A25, REAL_NS1:5

.= <*((Ldiff + Rsdiff) . i)*> by REAL_NS1:2

.= <*((Ldiff . i) + (Rsdiff . i))*> by RVSUM_1:11 ;

hence ( x in N implies (((Proj (i,n)) * g) /. x) - (((Proj (i,n)) * g) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) ) by A30, A36, A37, A38, A33, RVSUM_1:13; :: thesis: verum

end;then A25: (g /. x) - (g /. x0) = (DFG /. (x - x0)) + (GR /. (x - x0)) by A3;

A26: x0 in N by RCOMP_1:16;

then A27: ( ((Proj (i,n)) * g) /. x = ((Proj (i,n)) * g) . x & ((Proj (i,n)) * g) /. x0 = ((Proj (i,n)) * g) . x0 ) by A2, A21, A24, PARTFUN1:def 6;

A28: ( g /. x = g . x & g /. x0 = g . x0 ) by A2, A24, A26, PARTFUN1:def 6;

reconsider PGSx = (((Proj (i,n)) * g) /. x) - (((Proj (i,n)) * g) /. x0) as Element of REAL 1 by REAL_NS1:def 4;

((Proj (i,n)) * g) . x in rng ((Proj (i,n)) * g) by A2, A21, A24, FUNCT_1:3;

then reconsider PGdx = ((Proj (i,n)) * g) . x as Element of REAL 1 by REAL_NS1:def 4;

((Proj (i,n)) * g) . x0 in rng ((Proj (i,n)) * g) by A2, A21, A26, FUNCT_1:3;

then reconsider PGdx0 = ((Proj (i,n)) * g) . x0 as Element of REAL 1 by REAL_NS1:def 4;

g . x in rng g by A2, A24, FUNCT_1:3;

then reconsider Gx = g . x as Element of REAL n by REAL_NS1:def 4;

g . x0 in rng g by A2, A26, FUNCT_1:3;

then reconsider Gx0 = g . x0 as Element of REAL n by REAL_NS1:def 4;

set ProjGx = (Proj (i,n)) . (g . x);

Gx in dom (Proj (i,n)) by A22;

then (Proj (i,n)) . (g . x) in rng (Proj (i,n)) by FUNCT_1:3;

then reconsider ProjGx = (Proj (i,n)) . (g . x) as Element of REAL 1 by REAL_NS1:def 4;

set ProjGx0 = (Proj (i,n)) . (g . x0);

Gx0 in dom (Proj (i,n)) by A22;

then (Proj (i,n)) . (g . x0) in rng (Proj (i,n)) by FUNCT_1:3;

then reconsider ProjGx0 = (Proj (i,n)) . (g . x0) as Element of REAL 1 by REAL_NS1:def 4;

reconsider Gx1 = Gx as Element of (REAL-NS n) by REAL_NS1:def 4;

reconsider Gx01 = Gx0 as Element of (REAL-NS n) by REAL_NS1:def 4;

reconsider Gsx = g /. x as Element of REAL n by REAL_NS1:def 4;

reconsider Gsx0 = g /. x0 as Element of REAL n by REAL_NS1:def 4;

reconsider dxx0 = x - x0 as Element of REAL by XREAL_0:def 1;

reconsider Ldxx0 = L /. (x - x0) as Element of (REAL-NS 1) ;

A29: dom R = REAL by A8, PARTFUN1:def 2;

then A30: R /. (x - x0) = R . dxx0 by PARTFUN1:def 6;

then reconsider Rdxx0 = R . (x - x0) as Element of (REAL-NS 1) ;

reconsider Lxx0Rxx0 = (L /. (x - x0)) + (R /. (x - x0)) as Element of REAL 1 by REAL_NS1:def 4;

reconsider Ldiff = DFG /. (x - x0) as Element of REAL n by REAL_NS1:def 4;

dom DFG = REAL by FUNCT_2:def 1;

then A31: Ldiff = DFG . dxx0 by PARTFUN1:def 6;

set ProjLdiff = (Proj (i,n)) . Ldiff;

(Proj (i,n)) . Ldiff in rng (Proj (i,n)) by A20, FUNCT_1:3;

then reconsider ProjLdiff = (Proj (i,n)) . Ldiff as Element of REAL 1 by REAL_NS1:def 4;

A32: dom GR = REAL by A7, PARTFUN1:def 2;

then GR . dxx0 in rng GR by FUNCT_1:3;

then reconsider Rdiff = GR . dxx0 as Element of REAL n by REAL_NS1:def 4;

A33: Rdiff = GR /. dxx0 by A32, PARTFUN1:def 6;

set ProjRdiff = (Proj (i,n)) . Rdiff;

(Proj (i,n)) . Rdiff in rng (Proj (i,n)) by A22, FUNCT_1:3;

then reconsider ProjRdiff = (Proj (i,n)) . Rdiff as Element of REAL 1 by REAL_NS1:def 4;

dom L = REAL by FUNCT_2:def 1;

then A34: dxx0 in dom L ;

A35: L /. dxx0 = L . dxx0

.= (Proj (i,n)) . (DFG . dxx0) by A34, FUNCT_1:12

.= (Proj (i,n)) . Ldiff by A31 ;

R . (x - x0) = (Proj (i,n)) . Rdiff by A29, FUNCT_1:12;

then A36: Ldxx0 + Rdxx0 = ProjLdiff + ProjRdiff by A35, REAL_NS1:2;

(Proj (i,n)) . Ldiff = <*((proj (i,n)) . Ldiff)*> by PDIFF_1:def 4;

then A37: (Proj (i,n)) . Ldiff = <*(Ldiff . i)*> by PDIFF_1:def 1;

Rdiff in dom (Proj (i,n)) by A22;

then (Proj (i,n)) . Rdiff = <*((proj (i,n)) . Rdiff)*> by PDIFF_1:def 4;

then A38: (Proj (i,n)) . Rdiff = <*(Rdiff . i)*> by PDIFF_1:def 1;

reconsider diffGR = (DFG /. (x - x0)) + (GR /. (x - x0)) as Element of REAL n by REAL_NS1:def 4;

reconsider Rsdiff = GR /. (x - x0) as Element of REAL n by REAL_NS1:def 4;

PGSx = PGdx - PGdx0 by A27, REAL_NS1:5

.= ProjGx - PGdx0 by A2, A21, A24, FUNCT_1:12

.= ProjGx - ProjGx0 by A2, A21, A26, FUNCT_1:12

.= <*((proj (i,n)) . Gx1)*> - ProjGx0 by PDIFF_1:def 4

.= <*((proj (i,n)) . Gx1)*> - <*((proj (i,n)) . Gx01)*> by PDIFF_1:def 4

.= <*(Gx . i)*> - <*((proj (i,n)) . Gx01)*> by PDIFF_1:def 1

.= <*(Gx . i)*> - <*(Gx0 . i)*> by PDIFF_1:def 1

.= <*((Gx . i) - (Gx0 . i))*> by RVSUM_1:29

.= <*((Gsx - Gsx0) . i)*> by A28, RVSUM_1:27

.= <*(diffGR . i)*> by A25, REAL_NS1:5

.= <*((Ldiff + Rsdiff) . i)*> by REAL_NS1:2

.= <*((Ldiff . i) + (Rsdiff . i))*> by RVSUM_1:11 ;

hence ( x in N implies (((Proj (i,n)) * g) /. x) - (((Proj (i,n)) * g) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) ) by A30, A36, A37, A38, A33, RVSUM_1:13; :: thesis: verum

L /. jj = 1 * ((Proj (i,n)) . LP) by A5

.= (Proj (i,n)) . LP by RLVECT_1:def 8

.= (Proj (i,n)) . (1 * LP) by RLVECT_1:def 8

.= (Proj (i,n)) . (diff (g,x0)) by A3, A4 ;

hence (Proj (i,n)) . (diff (g,x0)) = diff (((Proj (i,n)) * g),x0) by A39, A2, A21, A23, NDIFF_3:def 4; :: thesis: verum