let n be non empty Element of NAT ; :: thesis: for g being PartFunc of REAL,(REAL-NS n)
for x0 being real number holds
( g is_differentiable_in x0 iff for i being Element of NAT st 1 <= i & i <= n holds
(Proj (i,n)) * g is_differentiable_in x0 )
let g be PartFunc of REAL,(REAL-NS n); :: thesis: for x0 being real number holds
( g is_differentiable_in x0 iff for i being Element of NAT st 1 <= i & i <= n holds
(Proj (i,n)) * g is_differentiable_in x0 )
let x0 be real number ; :: thesis: ( g is_differentiable_in x0 iff for i being Element of NAT st 1 <= i & i <= n holds
(Proj (i,n)) * g is_differentiable_in x0 )
thus ( g is_differentiable_in x0 implies for i being Element of NAT st 1 <= i & i <= n holds
(Proj (i,n)) * g is_differentiable_in x0 ) by Th24; :: thesis: ( ( for i being Element of NAT st 1 <= i & i <= n holds
(Proj (i,n)) * g is_differentiable_in x0 ) implies g is_differentiable_in x0 )
assume A1: for i being Element of NAT st 1 <= i & i <= n holds
(Proj (i,n)) * g is_differentiable_in x0 ; :: thesis: g is_differentiable_in x0
defpred S₁[ Element of NAT , Element of REAL ] means ( $2 > 0 & ].(x0 - $2),(x0 + $2).[ c= dom ((Proj ($1,n)) * g) & ex Ri being RestFunc of (REAL-NS 1) st
for x being Real st x in ].(x0 - $2),(x0 + $2).[ holds
(((Proj ($1,n)) * g) /. x) - (((Proj ($1,n)) * g) /. x0) = ((x - x0) * (diff (((Proj ($1,n)) * g),x0))) + (Ri /. (x - x0)) );
A2: for k being Element of NAT st k in Seg n holds
ex dk being Element of REAL st S₁[k,dk]

proof

let k be Element of NAT ; :: thesis: ( k in Seg n implies ex dk being Element of REAL st S₁[k,dk] )
assume k in Seg n ; :: thesis: ex dk being Element of REAL st S₁[k,dk]
then ( 1 <= k & k <= n ) by FINSEQ_1:1;
then (Proj (k,n)) * g is_differentiable_in x0 by A1;
then consider Nk being Neighbourhood of x0 such that
A3: ( Nk c= dom ((Proj (k,n)) * g) & ex L being LinearFunc of (REAL-NS 1) ex Rk being RestFunc of (REAL-NS 1) st
( L . 1 = diff (((Proj (k,n)) * g),x0) & ( for x being Real st x in Nk holds
(((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = (L . (x - x0)) + (Rk /. (x - x0)) ) ) ) by NDIFF_3:def 4;
consider dk being real number such that
A4: ( 0 < dk & Nk = ].(x0 - dk),(x0 + dk).[ ) by RCOMP_1:def 6;
reconsider dk = dk as Element of REAL by XREAL_0:def 1;
take dk ; :: thesis: S₁[k,dk]
thus 0 < dk by A4; :: thesis: ( ].(x0 - dk),(x0 + dk).[ c= dom ((Proj (k,n)) * g) & ex Ri being RestFunc of (REAL-NS 1) st
for x being Real st x in ].(x0 - dk),(x0 + dk).[ holds
(((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((x - x0) * (diff (((Proj (k,n)) * g),x0))) + (Ri /. (x - x0)) )
thus ].(x0 - dk),(x0 + dk).[ c= dom ((Proj (k,n)) * g) by A4, A3; :: thesis: ex Ri being RestFunc of (REAL-NS 1) st
for x being Real st x in ].(x0 - dk),(x0 + dk).[ holds
(((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((x - x0) * (diff (((Proj (k,n)) * g),x0))) + (Ri /. (x - x0))
thus ex Rk being RestFunc of (REAL-NS 1) st
for x being Real st x in ].(x0 - dk),(x0 + dk).[ holds
(((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((x - x0) * (diff (((Proj (k,n)) * g),x0))) + (Rk /. (x - x0)) :: thesis: verum

proof

consider L being LinearFunc of (REAL-NS 1), Rk being RestFunc of (REAL-NS 1) such that
A5: ( L . 1 = diff (((Proj (k,n)) * g),x0) & ( for x being Real st x in Nk holds
(((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = (L . (x - x0)) + (Rk /. (x - x0)) ) ) by A3;

A6: now :: thesis: for x being Real st x in Nk holds
(((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((x - x0) * (diff (((Proj (k,n)) * g),x0))) + (Rk /. (x - x0))

let x be Real; :: thesis: ( x in Nk implies (((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((x - x0) * (diff (((Proj (k,n)) * g),x0))) + (Rk /. (x - x0)) )
assume A7: x in Nk ; :: thesis: (((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((x - x0) * (diff (((Proj (k,n)) * g),x0))) + (Rk /. (x - x0))
consider L1 being Point of (REAL-NS 1) such that
A8: for p being Real holds L . p = p * L1 by NDIFF_3:def 2;
A9: diff (((Proj (k,n)) * g),x0) = 1 * L1 by A8, A5
.= L1 by RLVECT_1:def 8 ;
A10: L . (x - x0) = (x - x0) * (diff (((Proj (k,n)) * g),x0)) by A9, A8;
thus (((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((x - x0) * (diff (((Proj (k,n)) * g),x0))) + (Rk /. (x - x0)) by A10, A5, A7; :: thesis: verum

end;

take Rk ; :: thesis: for x being Real st x in ].(x0 - dk),(x0 + dk).[ holds
(((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((x - x0) * (diff (((Proj (k,n)) * g),x0))) + (Rk /. (x - x0))
thus for x being Real st x in ].(x0 - dk),(x0 + dk).[ holds
(((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((x - x0) * (diff (((Proj (k,n)) * g),x0))) + (Rk /. (x - x0)) by A4, A6; :: thesis: verum

end;

end;

consider d being FinSequence of REAL such that
A11: ( dom d = Seg n & ( for k being Element of NAT st k in Seg n holds
S₁[k,d /. k] ) ) from RECDEF_1:sch 17(A2);
set d0 = min d;
len d = n by A11, FINSEQ_1:def 3;
then A12: min_p d in dom d by RFINSEQ2:def 2;
then d /. (min_p d) > 0 by A11;
then A13: min d > 0 by A12, PARTFUN1:def 6;
defpred S₂[ Real, set ] means ex y being Element of REAL n st
( $2 = y & ( for i being Element of NAT st i in Seg n holds
y . i = (proj (1,1)) . ($1 * (diff (((Proj (i,n)) * g),x0))) ) );
A14: for x being Real ex y being Point of (REAL-NS n) st S₂[x,y]

proof

let x be Real; :: thesis: ex y being Point of (REAL-NS n) st S₂[x,y]
defpred S₃[ Element of NAT , set ] means $2 = (proj (1,1)) . (x * (diff (((Proj ($1,n)) * g),x0)));
A15: for i being Element of NAT st i in Seg n holds
ex r being Element of REAL st S₃[i,r] ;
consider y being FinSequence of REAL such that
A16: ( dom y = Seg n & ( for i being Element of NAT st i in Seg n holds
S₃[i,y /. i] ) ) from RECDEF_1:sch 17(A15);
len y = n by A16, FINSEQ_1:def 3;
then reconsider y = y as Element of REAL n by FINSEQ_2:92;

A17: now :: thesis: for i being Element of NAT st i in Seg n holds
y . i = (proj (1,1)) . (x * (diff (((Proj (i,n)) * g),x0)))

let i be Element of NAT ; :: thesis: ( i in Seg n implies y . i = (proj (1,1)) . (x * (diff (((Proj (i,n)) * g),x0))) )
assume i in Seg n ; :: thesis: y . i = (proj (1,1)) . (x * (diff (((Proj (i,n)) * g),x0)))
then ( S₃[i,y /. i] & y /. i = y . i ) by A16, PARTFUN1:def 6;
hence y . i = (proj (1,1)) . (x * (diff (((Proj (i,n)) * g),x0))) ; :: thesis: verum

end;

reconsider y0 = y as Point of (REAL-NS n) by REAL_NS1:def 4;
ex y being Element of REAL n st
( y0 = y & ( for i being Element of NAT st i in Seg n holds
y . i = (proj (1,1)) . (x * (diff (((Proj (i,n)) * g),x0))) ) ) by A17;
hence ex y0 being Point of (REAL-NS n) st S₂[x,y0] ; :: thesis: verum

end;

consider L being Function of REAL,(REAL-NS n) such that
A18: for x being Real holds S₂[x,L . x] from FUNCT_2:sch 3(A14);
for r being Real holds L . r = r * (L . 1)

proof

let r be Real; :: thesis: L . r = r * (L . 1)
consider Lx being Element of REAL n such that
A19: ( L . 1 = Lx & ( for i being Element of NAT st i in Seg n holds
Lx . i = (proj (1,1)) . (1 * (diff (((Proj (i,n)) * g),x0))) ) ) by A18;

A20: now :: thesis: for i being Element of NAT st i in Seg n holds
Lx . i = (proj (1,1)) . (diff (((Proj (i,n)) * g),x0))

let i be Element of NAT ; :: thesis: ( i in Seg n implies Lx . i = (proj (1,1)) . (diff (((Proj (i,n)) * g),x0)) )
assume i in Seg n ; :: thesis: Lx . i = (proj (1,1)) . (diff (((Proj (i,n)) * g),x0))
then Lx . i = (proj (1,1)) . (1 * (diff (((Proj (i,n)) * g),x0))) by A19;
hence Lx . i = (proj (1,1)) . (diff (((Proj (i,n)) * g),x0)) by RLVECT_1:def 8; :: thesis: verum

end;

consider Lrx being Element of REAL n such that
A21: ( L . r = Lrx & ( for i being Element of NAT st i in Seg n holds
Lrx . i = (proj (1,1)) . (r * (diff (((Proj (i,n)) * g),x0))) ) ) by A18;
A22: dom (r * Lx) = Seg n by FINSEQ_2:124;
then A23: dom (r * Lx) = dom Lrx by FINSEQ_2:124;
for i0 being Nat st i0 in dom (r * Lx) holds
(r * Lx) . i0 = Lrx . i0

proof

let i0 be Nat; :: thesis: ( i0 in dom (r * Lx) implies (r * Lx) . i0 = Lrx . i0 )
reconsider i = i0 as Element of NAT by ORDINAL1:def 12;
assume i0 in dom (r * Lx) ; :: thesis: (r * Lx) . i0 = Lrx . i0
then A24: ( Lx . i = (proj (1,1)) . (diff (((Proj (i,n)) * g),x0)) & Lrx . i = (proj (1,1)) . (r * (diff (((Proj (i,n)) * g),x0))) ) by A20, A21, A22;
A25: (r * 1) * (diff (((Proj (i,n)) * g),x0)) = r * (1 * (diff (((Proj (i,n)) * g),x0))) by RLVECT_1:def 8;
reconsider Diffrx = (r * 1) * (diff (((Proj (i,n)) * g),x0)) as Element of REAL 1 by REAL_NS1:def 4;
reconsider Diffx = 1 * (diff (((Proj (i,n)) * g),x0)) as Element of REAL 1 by REAL_NS1:def 4;
A26: Diffx = diff (((Proj (i,n)) * g),x0) by RLVECT_1:def 8;
Diffrx = r * Diffx by A25, REAL_NS1:3;
then Lrx . i0 = (r * Diffx) . 1 by A24, PDIFF_1:def 1;
then Lrx . i0 = r * (Diffx . 1) by RVSUM_1:45;
then Lrx . i0 = r * (Lx . i0) by A24, A26, PDIFF_1:def 1;
hence (r * Lx) . i0 = Lrx . i0 by RVSUM_1:45; :: thesis: verum

end;

then r * Lx = Lrx by A23, FINSEQ_1:13;
hence L . r = r * (L . 1) by A19, A21, REAL_NS1:3; :: thesis: verum

end;

then reconsider L = L as linear Function of REAL,(REAL-NS n) by NDIFF_3:def 2;
reconsider L0 = L as LinearFunc of (REAL-NS n) ;
deffunc H₁( Element of REAL ) -> Element of the carrier of (REAL-NS n) = ((g /. ($1 + x0)) - (g /. x0)) - (L . $1);
consider R being Function of REAL,(REAL-NS n) such that
A27: for x being Element of REAL holds R . x = H₁(x) from FUNCT_2:sch 4();
A28: for x being Element of REAL
for i being Element of NAT st i in Seg n & x + x0 in dom g holds
((Proj (i,n)) * R) . x = ((((Proj (i,n)) * g) /. (x + x0)) - (((Proj (i,n)) * g) /. x0)) - (((Proj (i,n)) * L) . x)

proof

let x be Element of REAL ; :: thesis: for i being Element of NAT st i in Seg n & x + x0 in dom g holds
((Proj (i,n)) * R) . x = ((((Proj (i,n)) * g) /. (x + x0)) - (((Proj (i,n)) * g) /. x0)) - (((Proj (i,n)) * L) . x)
let i be Element of NAT ; :: thesis: ( i in Seg n & x + x0 in dom g implies ((Proj (i,n)) * R) . x = ((((Proj (i,n)) * g) /. (x + x0)) - (((Proj (i,n)) * g) /. x0)) - (((Proj (i,n)) * L) . x) )
assume that
A29: i in Seg n and
A30: x + x0 in dom g ; :: thesis: ((Proj (i,n)) * R) . x = ((((Proj (i,n)) * g) /. (x + x0)) - (((Proj (i,n)) * g) /. x0)) - (((Proj (i,n)) * L) . x)
A31: |.(x0 - x0).| = 0 by COMPLEX1:44;
A32: ( 0 < d /. i & ].(x0 - (d /. i)),(x0 + (d /. i)).[ c= dom ((Proj (i,n)) * g) ) by A29, A11;
then x0 in ].(x0 - (d /. i)),(x0 + (d /. i)).[ by A31, RCOMP_1:1;
then A33: x0 in dom ((Proj (i,n)) * g) by A32;
A34: dom ((Proj (i,n)) * g) c= dom g by RELAT_1:25;
reconsider gxx0 = g /. (x + x0), gx0 = g /. x0, Lx = L . x as Element of REAL n by REAL_NS1:def 4;
reconsider gxx01 = g /. (x + x0), gx01 = g /. x0, Lx1 = L . x as Point of (REAL-NS n) ;
A35: ( - gx0 = (- 1) * (g /. x0) & - Lx = (- 1) * (L . x) ) by REAL_NS1:3;
then gxx0 + (- gx0) = (g /. (x + x0)) + ((- 1) * (g /. x0)) by REAL_NS1:2;
then A36: (gxx0 + (- gx0)) + (- Lx) = ((g /. (x + x0)) + ((- 1) * (g /. x0))) + ((- 1) * (L . x)) by A35, REAL_NS1:2;
A37: - 1 is Real by XREAL_0:def 1;
gxx0 - gx0 = (g /. (x + x0)) - (g /. x0) by REAL_NS1:5;
then A38: ((g /. (x + x0)) - (g /. x0)) - (L . x) = (gxx0 - gx0) - Lx by REAL_NS1:5;
((Proj (i,n)) * R) . x = (Proj (i,n)) . (R . x) by FUNCT_2:15;
then ((Proj (i,n)) * R) . x = (Proj (i,n)) . (((g /. (x + x0)) - (g /. x0)) - (L . x)) by A27;
then ((Proj (i,n)) * R) . x = ((Proj (i,n)) . ((g /. (x + x0)) + ((- 1) * (g /. x0)))) + ((Proj (i,n)) . ((- 1) * (L . x))) by A38, A36, PDIFF_6:26;
then A39: ((Proj (i,n)) * R) . x = (((Proj (i,n)) . (g /. (x + x0))) + ((Proj (i,n)) . ((- 1) * (g /. x0)))) + ((Proj (i,n)) . ((- 1) * (L . x))) by PDIFF_6:26;
( (Proj (i,n)) . ((- 1) * (g /. x0)) = (- 1) * ((Proj (i,n)) . (g /. x0)) & (Proj (i,n)) . ((- 1) * Lx1) = (- 1) * ((Proj (i,n)) . Lx1) ) by A37, PDIFF_6:27;
then ((Proj (i,n)) * R) . x = (((Proj (i,n)) . (g /. (x + x0))) + (- ((Proj (i,n)) . (g /. x0)))) + ((- 1) * ((Proj (i,n)) . (L . x))) by A39, RLVECT_1:16;
then A40: ((Proj (i,n)) * R) . x = (((Proj (i,n)) . (g /. (x + x0))) - ((Proj (i,n)) . (g /. x0))) - ((Proj (i,n)) . (L . x)) by RLVECT_1:16;
( g /. (x + x0) in the carrier of (REAL-NS n) & g /. x0 in the carrier of (REAL-NS n) ) ;
then A41: ( g /. (x + x0) in dom (Proj (i,n)) & g /. x0 in dom (Proj (i,n)) ) by FUNCT_2:def 1;
A42: (Proj (i,n)) . (g /. (x + x0)) = (Proj (i,n)) /. (g /. (x + x0))
.= ((Proj (i,n)) * g) /. (x + x0) by A30, A41, PARTFUN2:4 ;
(Proj (i,n)) . (g /. x0) = (Proj (i,n)) /. (g /. x0)
.= ((Proj (i,n)) * g) /. x0 by A33, A34, A41, PARTFUN2:4 ;
hence ((Proj (i,n)) * R) . x = ((((Proj (i,n)) * g) /. (x + x0)) - (((Proj (i,n)) * g) /. x0)) - (((Proj (i,n)) * L) . x) by A40, A42, FUNCT_2:15; :: thesis: verum

end;

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

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 A43: r > 0 ; :: thesis: ex d being Real st
( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds
(|.z.| ") * ||.(R /. z).|| < r ) )
set r0 = ((sqrt n) ") * r;
A44: sqrt n > 0 by SQUARE_1:25;
then A45: ((sqrt n) ") * r > 0 by A43, XREAL_1:129;
defpred S₃[ Element of NAT , Element of REAL ] means ( $2 > 0 & ( for z being Real st z <> 0 & |.z.| < $2 holds
(|.z.| ") * ||.(((Proj ($1,n)) * R) /. z).|| < ((sqrt n) ") * r ) );
A46: for k being Element of NAT st k in Seg n holds
ex dd being Element of REAL st S₃[k,dd]

proof

let k be Element of NAT ; :: thesis: ( k in Seg n implies ex dd being Element of REAL st S₃[k,dd] )
assume A47: k in Seg n ; :: thesis: ex dd being Element of REAL st S₃[k,dd]
then ( 1 <= k & k <= n ) by FINSEQ_1:1;
then (Proj (k,n)) * g is_differentiable_in x0 by A1;
then consider Nk being Neighbourhood of x0 such that
A48: ( Nk c= dom ((Proj (k,n)) * g) & ex LR being LinearFunc of (REAL-NS 1) ex PR being RestFunc of (REAL-NS 1) st
( LR . 1 = diff (((Proj (k,n)) * g),x0) & ( for x being Real st x in Nk holds
(((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = (LR . (x - x0)) + (PR /. (x - x0)) ) ) ) by NDIFF_3:def 4;
consider d0 being real number such that
A49: ( 0 < d0 & Nk = ].(x0 - d0),(x0 + d0).[ ) by RCOMP_1:def 6;
reconsider d0 = d0 as Real by XREAL_0:def 1;
consider LR being LinearFunc of (REAL-NS 1), PR being RestFunc of (REAL-NS 1) such that
A50: ( LR . 1 = diff (((Proj (k,n)) * g),x0) & ( for x being Real st x in Nk holds
(((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = (LR . (x - x0)) + (PR /. (x - x0)) ) ) by A48;

A51: now :: thesis: for x being Real st x in Nk holds
(((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((x - x0) * (diff (((Proj (k,n)) * g),x0))) + (PR /. (x - x0))

let x be Real; :: thesis: ( x in Nk implies (((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((x - x0) * (diff (((Proj (k,n)) * g),x0))) + (PR /. (x - x0)) )
assume A52: x in Nk ; :: thesis: (((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((x - x0) * (diff (((Proj (k,n)) * g),x0))) + (PR /. (x - x0))
consider L1 being Point of (REAL-NS 1) such that
A53: for p being Real holds LR . p = p * L1 by NDIFF_3:def 2;
diff (((Proj (k,n)) * g),x0) = 1 * L1 by A53, A50
.= L1 by RLVECT_1:def 8 ;
then LR . (x - x0) = (x - x0) * (diff (((Proj (k,n)) * g),x0)) by A53;
hence (((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((x - x0) * (diff (((Proj (k,n)) * g),x0))) + (PR /. (x - x0)) by A52, A50; :: thesis: verum

end;

PR is total by NDIFF_3:def 1;
then consider d1 being Real such that
A54: ( d1 > 0 & ( for z being Real st z <> 0 & |.z.| < d1 holds
(|.z.| ") * ||.(PR /. z).|| < ((sqrt n) ") * r ) ) by A45, Th23;
set dd = min (d0,d1);
take min (d0,d1) ; :: thesis: S₃[k, min (d0,d1)]
for z being Real st z <> 0 & |.z.| < min (d0,d1) holds
(|.z.| ") * ||.(((Proj (k,n)) * R) /. z).|| < ((sqrt n) ") * r

proof

let z be Real; :: thesis: ( z <> 0 & |.z.| < min (d0,d1) implies (|.z.| ") * ||.(((Proj (k,n)) * R) /. z).|| < ((sqrt n) ") * r )
assume A55: ( z <> 0 & |.z.| < min (d0,d1) ) ; :: thesis: (|.z.| ") * ||.(((Proj (k,n)) * R) /. z).|| < ((sqrt n) ") * r
min (d0,d1) <= d1 by XXREAL_0:17;
then |.z.| < d1 by A55, XXREAL_0:2;
then A56: (|.z.| ") * ||.(PR /. z).|| < ((sqrt n) ") * r by A55, A54;
min (d0,d1) <= d0 by XXREAL_0:17;
then A57: |.z.| < d0 by A55, XXREAL_0:2;
(z + x0) - x0 = z ;
then A58: z + x0 in ].(x0 - d0),(x0 + d0).[ by A57, RCOMP_1:1;
then A59: z + x0 in dom ((Proj (k,n)) * g) by A48, A49;
(((Proj (k,n)) * g) /. (z + x0)) - (((Proj (k,n)) * g) /. x0) = (((z + x0) - x0) * (diff (((Proj (k,n)) * g),x0))) + (PR /. ((z + x0) - x0)) by A58, A49, A51;
then A60: PR /. z = ((((Proj (k,n)) * g) /. (z + x0)) - (((Proj (k,n)) * g) /. x0)) - (z * (diff (((Proj (k,n)) * g),x0))) by RLVECT_4:1;
dom ((Proj (k,n)) * g) c= dom g by RELAT_1:25;
then A61: ((Proj (k,n)) * R) . z = ((((Proj (k,n)) * g) /. (z + x0)) - (((Proj (k,n)) * g) /. x0)) - (((Proj (k,n)) * L) . z) by A59, A47, A28;
consider y being Element of REAL n such that
A62: ( L . z = y & ( for i being Element of NAT st i in Seg n holds
y . i = (proj (1,1)) . (z * (diff (((Proj (i,n)) * g),x0))) ) ) by A18;
A63: y . k = (proj (1,1)) . (z * (diff (((Proj (k,n)) * g),x0))) by A62, A47;
z * (diff (((Proj (k,n)) * g),x0)) is Element of REAL 1 by REAL_NS1:def 4;
then consider Dk being Element of REAL such that
A64: z * (diff (((Proj (k,n)) * g),x0)) = <*Dk*> by FINSEQ_2:97;
reconsider y1 = y as Point of (REAL-NS n) by REAL_NS1:def 4;
dom L = REAL by FUNCT_2:def 1;
then ((Proj (k,n)) * L) . z = (Proj (k,n)) . (L . z) by FUNCT_1:13;
then ((Proj (k,n)) * L) . z = <*((proj (k,n)) . y1)*> by A62, PDIFF_1:def 4;
then ((Proj (k,n)) * L) . z = <*((proj (1,1)) . (z * (diff (((Proj (k,n)) * g),x0))))*> by A63, PDIFF_1:def 1;
hence (|.z.| ") * ||.(((Proj (k,n)) * R) /. z).|| < ((sqrt n) ") * r by A56, A60, A61, A64, PDIFF_1:1; :: thesis: verum

end;

hence S₃[k, min (d0,d1)] by A49, A54, XXREAL_0:21; :: thesis: verum

end;

consider dd being FinSequence of REAL such that
A65: ( dom dd = Seg n & ( for i being Element of NAT st i in Seg n holds
S₃[i,dd /. i] ) ) from RECDEF_1:sch 17(A46);
take d = min dd; :: thesis: ( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds
(|.z.| ") * ||.(R /. z).|| < r ) )
len dd = n by A65, FINSEQ_1:def 3;
then A66: min_p dd in dom dd by RFINSEQ2:def 2;
then A67: dd /. (min_p dd) > 0 by A65;
for z being Real st z <> 0 & |.z.| < d holds
(|.z.| ") * ||.(R /. z).|| < r

proof

let z be Real; :: thesis: ( z <> 0 & |.z.| < d implies (|.z.| ") * ||.(R /. z).|| < r )
assume A68: ( z <> 0 & |.z.| < d ) ; :: thesis: (|.z.| ") * ||.(R /. z).|| < r
reconsider Rz = R /. z as Element of REAL n by REAL_NS1:def 4;
reconsider R0 = n |-> ((|.z.| * (((sqrt n) ") * r)) ^2) as Element of n -tuples_on REAL ;
reconsider SRz = sqr Rz as Element of n -tuples_on REAL ;
A69: |.z.| > 0 by A68, COMPLEX1:47;
A70: for i0 being Nat st i0 in Seg n holds
SRz . i0 < R0 . i0

proof

let i0 be Nat; :: thesis: ( i0 in Seg n implies SRz . i0 < R0 . i0 )
reconsider i = i0 as Element of NAT by ORDINAL1:def 12;
assume A71: i0 in Seg n ; :: thesis: SRz . i0 < R0 . i0
then i in dom Rz by FINSEQ_2:124;
then (sqr Rz) . i = sqrreal . (Rz . i) by FUNCT_1:13;
then A72: (sqr Rz) . i = (Rz . i) ^2 by RVSUM_1:def 2;
( 1 <= i & i <= n ) by A71, FINSEQ_1:1;
then ( 1 <= i & i <= len dd ) by A65, FINSEQ_1:def 3;
then d <= dd . i by RFINSEQ2:2;
then d <= dd /. i by A71, A65, PARTFUN1:def 6;
then |.z.| < dd /. i by A68, XXREAL_0:2;
then (|.z.| ") * ||.(((Proj (i,n)) * R) /. z).|| < ((sqrt n) ") * r by A68, A71, A65;
then A73: ||.(((Proj (i,n)) * R) /. z).|| < (((sqrt n) ") * r) / (|.z.| ") by A69, XREAL_1:81;
reconsider Rzi = <*(Rz . i)*> as Element of REAL 1 by FINSEQ_2:98;
((Proj (i,n)) * R) . z = (Proj (i,n)) . (R . z) by FUNCT_2:15;
then ((Proj (i,n)) * R) . z = <*((proj (i,n)) . Rz)*> by PDIFF_1:def 4;
then ((Proj (i,n)) * R) . z = <*(Rz . i)*> by PDIFF_1:def 1;
then ||.(((Proj (i,n)) * R) . z).|| = |.Rzi.| by REAL_NS1:1;
then |.(Rz . i).| < |.z.| * (((sqrt n) ") * r) by A73, JORDAN2C:10;
then |.(Rz . i).| ^2 < (|.z.| * (((sqrt n) ") * r)) ^2 by COMPLEX1:46, SQUARE_1:16;
then (Rz . i0) ^2 < (|.z.| * (((sqrt n) ") * r)) ^2 by COMPLEX1:75;
hence SRz . i0 < R0 . i0 by A71, A72, FINSEQ_2:57; :: thesis: verum

end;

A74: for i being Nat st i in dom (sqr Rz) holds
0 <= (sqr Rz) . i

proof

let i be Nat; :: thesis: ( i in dom (sqr Rz) implies 0 <= (sqr Rz) . i )
assume i in dom (sqr Rz) ; :: thesis: 0 <= (sqr Rz) . i
then ( i in dom (sqrreal * Rz) & dom (sqrreal * Rz) c= dom Rz ) by RELAT_1:25;
then (sqr Rz) . i = sqrreal . (Rz . i) by FUNCT_1:13;
then (sqr Rz) . i = (Rz . i) ^2 by RVSUM_1:def 2;
hence 0 <= (sqr Rz) . i by XREAL_1:63; :: thesis: verum

end;

A75: (|.z.| * (((sqrt n) ") * r)) ^2 >= 0 by XREAL_1:63;
A76: ex i being Nat st
( i in Seg n & SRz . i < R0 . i )

proof

take 1 ; :: thesis: ( 1 in Seg n & SRz . 1 < R0 . 1 )
1 <= n by NAT_1:14;
hence 1 in Seg n ; :: thesis: SRz . 1 < R0 . 1
hence SRz . 1 < R0 . 1 by A70; :: thesis: verum

end;

A77: sqrt n > 0 by SQUARE_1:25;
for i0 being Nat st i0 in Seg n holds
SRz . i0 <= R0 . i0 by A70;
then Sum SRz < Sum R0 by A76, RVSUM_1:83;
then Sum (sqr Rz) < n * ((|.z.| * (((sqrt n) ") * r)) ^2) by RVSUM_1:80;
then |.Rz.| < sqrt (n * ((|.z.| * (((sqrt n) ") * r)) ^2)) by A74, RVSUM_1:84, SQUARE_1:27;
then |.Rz.| < (sqrt n) * (sqrt ((|.z.| * (((sqrt n) ") * r)) ^2)) by A75, SQUARE_1:29;
then |.Rz.| < (sqrt n) * |.(|.z.| * (((sqrt n) ") * r)).| by COMPLEX1:72;
then |.Rz.| < (sqrt n) * (|.z.| * (((sqrt n) ") * r)) by A44, A43, A69, ABSVALUE:def 1;
then |.Rz.| < ((sqrt n) * (((sqrt n) ") * r)) * |.z.| ;
then |.Rz.| / |.z.| < (sqrt n) * (((sqrt n) ") * r) by A69, XREAL_1:83;
then (|.z.| ") * ||.(R /. z).|| < ((sqrt n) * ((sqrt n) ")) * r by REAL_NS1:1;
then (|.z.| ") * ||.(R /. z).|| < 1 * r by A77, XCMPLX_0:def 7;
hence (|.z.| ") * ||.(R /. z).|| < r ; :: thesis: verum

end;

hence ( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds
(|.z.| ") * ||.(R /. z).|| < r ) ) by A67, A66, PARTFUN1:def 6; :: thesis: verum

end;

then reconsider R = R as RestFunc of (REAL-NS n) by Th23;
reconsider N = ].(x0 - (min d)),(x0 + (min d)).[ as Neighbourhood of x0 by A13, RCOMP_1:def 6;

now :: thesis: for x being set st x in N holds
x in dom g

let x be set ; :: thesis: ( x in N implies x in dom g )
assume A78: x in N ; :: thesis: x in dom g
then reconsider y = x as Real ;
A79: |.(y - x0).| < min d by A78, RCOMP_1:1;
1 <= n by NAT_1:14;
then A80: ( 1 in Seg n & 1 in dom d ) by A11;
then A81: ].(x0 - (d /. 1)),(x0 + (d /. 1)).[ c= dom ((Proj (1,n)) * g) by A11;
dom ((Proj (1,n)) * g) c= dom g by RELAT_1:25;
then A82: ].(x0 - (d /. 1)),(x0 + (d /. 1)).[ c= dom g by A81, XBOOLE_1:1;
len d = n by A11, FINSEQ_1:def 3;
then 1 <= len d by NAT_1:14;
then min d <= d . 1 by RFINSEQ2:2;
then min d <= d /. 1 by A80, PARTFUN1:def 6;
then |.(y - x0).| < d /. 1 by A79, XXREAL_0:2;
then y in ].(x0 - (d /. 1)),(x0 + (d /. 1)).[ by RCOMP_1:1;
hence x in dom g by A82; :: thesis: verum

end;

then A83: N c= dom g by TARSKI:def 3;
ex L being LinearFunc of (REAL-NS n) ex R being RestFunc of (REAL-NS n) st
for x being Real st x in N holds
(g /. x) - (g /. x0) = (L . (x - x0)) + (R /. (x - x0))

proof

take L0 ; :: thesis: ex R being RestFunc of (REAL-NS n) st
for x being Real st x in N holds
(g /. x) - (g /. x0) = (L0 . (x - x0)) + (R /. (x - x0))
take R ; :: thesis: for x being Real st x in N holds
(g /. x) - (g /. x0) = (L0 . (x - x0)) + (R /. (x - x0))
let x be Real; :: thesis: ( x in N implies (g /. x) - (g /. x0) = (L0 . (x - x0)) + (R /. (x - x0)) )
assume x in N ; :: thesis: (g /. x) - (g /. x0) = (L0 . (x - x0)) + (R /. (x - x0))
A84: dom R = REAL by PARTFUN1:def 2;
R . (x - x0) = ((g /. ((x - x0) + x0)) - (g /. x0)) - (L . (x - x0)) by A27;
then R /. (x - x0) = ((g /. x) - (g /. x0)) + (- (L0 . (x - x0))) by A84, PARTFUN1:def 6;
then (L0 . (x - x0)) + (R /. (x - x0)) = ((g /. x) - (g /. x0)) + ((- (L0 . (x - x0))) + (L0 . (x - x0))) by RLVECT_1:def 3;
then (L0 . (x - x0)) + (R /. (x - x0)) = ((g /. x) - (g /. x0)) + (0. (REAL-NS n)) by RLVECT_1:5;
hence (g /. x) - (g /. x0) = (L0 . (x - x0)) + (R /. (x - x0)) by RLVECT_1:4; :: thesis: verum

end;

hence g is_differentiable_in x0 by A83, NDIFF_3:def 3; :: thesis: verum