let n be non zero Element of NAT ; :: thesis: for g being PartFunc of REAL,(REAL-NS n)
for x0 being Real 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 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; :: 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 S1[ 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 Nat st k in Seg n holds
ex dk being Element of REAL st S1[k,dk]
proof
let k be Nat; :: thesis: ( k in Seg n implies ex dk being Element of REAL st S1[k,dk] )
A3: k in NAT by ORDINAL1:def 12;
assume k in Seg n ; :: thesis: ex dk being Element of REAL st S1[k,dk]
then ( 1 <= k & k <= n ) by FINSEQ_1:1;
then (Proj (k,n)) * g is_differentiable_in x0 by A1, A3;
then consider Nk being Neighbourhood of x0 such that
A4: ( 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 such that
A5: ( 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: S1[k,dk]
thus 0 < dk by A5; :: 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 A5, A4; :: 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
A6: ( 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 A4;
A7: 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 A8: 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
A9: for p being Real holds L /. p = p * L1 by NDIFF_3:def 2;
A10: diff (((Proj (k,n)) * g),x0) = 1 * L1 by A9, A6
.= L1 by RLVECT_1:def 8 ;
A11: L /. (x - x0) = (x - x0) * (diff (((Proj (k,n)) * g),x0)) by A10, A9;
thus (((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((x - x0) * (diff (((Proj (k,n)) * g),x0))) + (Rk /. (x - x0)) by A11, A6, A8; :: 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 A5, A7; :: thesis: verum
end;
end;
consider d being FinSequence of REAL such that
A12: ( dom d = Seg n & ( for k being Nat st k in Seg n holds
S1[k,d /. k] ) ) from RECDEF_1:sch 17(A2);
 set d0 = min d;
len d = n by A12, FINSEQ_1:def 3;
then A13: min_p d in dom d by RFINSEQ2:def 2;
then d /. (min_p d) > 0 by A12;
then A14: min d > 0 by A13, PARTFUN1:def 6;
defpred S2[ 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))) ) );
A15: for x being Element of REAL ex y being Point of (REAL-NS n) st S2[x,y]
proof
let x be Element of REAL ; :: thesis: ex y being Point of (REAL-NS n) st S2[x,y]
defpred S3[ Nat, set ] means $2 = (proj (1,1)) . (x * (diff (((Proj ($1,n)) * g),x0)));
A16: for i being Nat st i in Seg n holds
ex r being Element of REAL st S3[i,r]
proof
let i be Nat; :: thesis: ( i in Seg n implies ex r being Element of REAL st S3[i,r] )
assume i in Seg n ; :: thesis: ex r being Element of REAL st S3[i,r]
(proj (1,1)) . (x * (diff (((Proj (i,n)) * g),x0))) in REAL by XREAL_0:def 1;
hence ex r being Element of REAL st S3[i,r] ; :: thesis: verum
end;
consider y being FinSequence of REAL such that
A17: ( dom y = Seg n & ( for i being Nat st i in Seg n holds
S3[i,y /. i] ) ) from RECDEF_1:sch 17(A16);
 len y = n by A17, FINSEQ_1:def 3;
then reconsider y = y as Element of REAL n by FINSEQ_2:92;
A18: 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 ( S3[i,y /. i] & y /. i = y . i ) by A17, 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 A18;
hence ex y0 being Point of (REAL-NS n) st S2[x,y0] ; :: thesis: verum
end;
consider L being Function of REAL,(REAL-NS n) such that
A19: for x being Element of REAL holds S2[x,L . x] from FUNCT_2:sch 3(A15);
 A20: for x being Real holds S2[x,L /. x]
proof
let x be Real; :: thesis: S2[x,L /. x]
reconsider x = x as Element of REAL by XREAL_0:def 1;
S2[x,L /. x] by A19;
hence S2[x,L /. x] ; :: thesis: verum
end;
for r being Real holds L /. r = r * (L /. jj)
proof
let r be Real; :: thesis: L /. r = r * (L /. jj)
consider Lx being Element of REAL n such that
A21: ( 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 A20;
A22: 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 A21;
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
A23: ( 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 A20;
A24: dom (r * Lx) = Seg n by FINSEQ_2:124;
then A25: 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 A26: ( Lx . i = (proj (1,1)) . (diff (((Proj (i,n)) * g),x0)) & Lrx . i = (proj (1,1)) . (r * (diff (((Proj (i,n)) * g),x0))) ) by A22, A23, A24;
A27: (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;
A28: Diffx = diff (((Proj (i,n)) * g),x0) by RLVECT_1:def 8;
Diffrx = r * Diffx by A27, REAL_NS1:3;
then Lrx . i0 = (r * Diffx) . 1 by A26, PDIFF_1:def 1;
then Lrx . i0 = r * (Diffx . 1) by RVSUM_1:45;
then Lrx . i0 = r * (Lx . i0) by A26, A28, PDIFF_1:def 1;
hence (r * Lx) . i0 = Lrx . i0 by RVSUM_1:45; :: thesis: verum
end;
then r * Lx = Lrx by A25, FINSEQ_1:13;
hence L /. r = r * (L /. jj) by A21, A23, 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 H1( 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
A29: for x being Element of REAL holds R . x = H1(x) from FUNCT_2:sch 4();
 A30: 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
A31: i in Seg n and
A32: 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)
A33: |.(x0 - x0).| = 0 by COMPLEX1:44;
A34: ( 0 < d /. i & ].(x0 - (d /. i)),(x0 + (d /. i)).[ c= dom ((Proj (i,n)) * g) ) by A31, A12;
then x0 in ].(x0 - (d /. i)),(x0 + (d /. i)).[ by A33, RCOMP_1:1;
then A35: x0 in dom ((Proj (i,n)) * g) by A34;
A36: 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) ;
A37: ( - 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 A38: (gxx0 + (- gx0)) + (- Lx) = ((g /. (x + x0)) + ((- 1) * (g /. x0))) + ((- 1) * (L /. x)) by A37, REAL_NS1:2;
gxx0 - gx0 = (g /. (x + x0)) - (g /. x0) by REAL_NS1:5;
then A39: ((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 A29;
then ((Proj (i,n)) * R) . x = ((Proj (i,n)) . ((g /. (x + x0)) + ((- 1) * (g /. x0)))) + ((Proj (i,n)) . ((- 1) * (L /. x))) by A39, A38, PDIFF_6:26;
then A40: ((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 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 A40, RLVECT_1:16;
then A41: ((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 A42: ( g /. (x + x0) in dom (Proj (i,n)) & g /. x0 in dom (Proj (i,n)) ) by FUNCT_2:def 1;
A43: (Proj (i,n)) . (g /. (x + x0)) = (Proj (i,n)) /. (g /. (x + x0))
.= ((Proj (i,n)) * g) /. (x + x0) by A32, A42, PARTFUN2:4 ;
(Proj (i,n)) . (g /. x0) = (Proj (i,n)) /. (g /. x0)
.= ((Proj (i,n)) * g) /. x0 by A35, A36, A42, 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 A41, A43, 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 A44: r > 0 ; :: thesis: ex d being Real st
( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds
(|.z.| ") * ||.(R /. z).|| < r ) )
reconsider r0 = ((sqrt n) ") * r as Element of REAL by XREAL_0:def 1;
A45: sqrt n > 0 by SQUARE_1:25;
then A46: r0 > 0 by A44, XREAL_1:129;
defpred S3[ Nat, Real] means ( $2 > 0 & ( for z being Real st z <> 0 & |.z.| < $2 holds
(|.z.| ") * ||.(((Proj ($1,n)) * R) /. z).|| < r0 ) );
A47: for k being Nat st k in Seg n holds
ex dd being Element of REAL st S3[k,dd]
proof
let k be Nat; :: thesis: ( k in Seg n implies ex dd being Element of REAL st S3[k,dd] )
A48: k in NAT by ORDINAL1:def 12;
assume A49: k in Seg n ; :: thesis: ex dd being Element of REAL st S3[k,dd]
then ( 1 <= k & k <= n ) by FINSEQ_1:1;
then (Proj (k,n)) * g is_differentiable_in x0 by A1, A48;
then consider Nk being Neighbourhood of x0 such that
A50: ( 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 such that
A51: ( 0 < d0 & Nk = ].(x0 - d0),(x0 + d0).[ ) by RCOMP_1:def 6;
reconsider d0 = d0 as Element of REAL by XREAL_0:def 1;
consider LR being LinearFunc of (REAL-NS 1), PR being RestFunc of (REAL-NS 1) such that
A52: ( 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 A50;
A53: 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 A54: 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
A55: for p being Real holds LR /. p = p * L1 by NDIFF_3:def 2;
diff (((Proj (k,n)) * g),x0) = 1 * L1 by A55, A52
.= L1 by RLVECT_1:def 8 ;
then LR /. (x - x0) = (x - x0) * (diff (((Proj (k,n)) * g),x0)) by A55;
hence (((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((x - x0) * (diff (((Proj (k,n)) * g),x0))) + (PR /. (x - x0)) by A54, A52; :: thesis: verum
end;
PR is total by NDIFF_3:def 1;
then consider d1 being Real such that
A56: ( d1 > 0 & ( for z being Real st z <> 0 & |.z.| < d1 holds
(|.z.| ") * ||.(PR /. z).|| < r0 ) ) by A46, Th23;
reconsider d1 = d1 as Element of REAL by XREAL_0:def 1;
reconsider dd = min (d0,d1) as Element of REAL by XREAL_0:def 1;
take dd ; :: thesis: S3[k,dd]
for z being Real st z <> 0 & |.z.| < dd holds
(|.z.| ") * ||.(((Proj (k,n)) * R) /. z).|| < r0
proof
let z be Real; :: thesis: ( z <> 0 & |.z.| < dd implies (|.z.| ") * ||.(((Proj (k,n)) * R) /. z).|| < r0 )
assume A57: ( z <> 0 & |.z.| < dd ) ; :: thesis: (|.z.| ") * ||.(((Proj (k,n)) * R) /. z).|| < r0
dd <= d1 by XXREAL_0:17;
then |.z.| < d1 by A57, XXREAL_0:2;
then A58: (|.z.| ") * ||.(PR /. z).|| < r0 by A57, A56;
dd <= d0 by XXREAL_0:17;
then A59: |.z.| < d0 by A57, XXREAL_0:2;
(z + x0) - x0 = z ;
then A60: z + x0 in ].(x0 - d0),(x0 + d0).[ by A59, RCOMP_1:1;
then A61: z + x0 in dom ((Proj (k,n)) * g) by A50, A51;
(((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 A60, A51, A53;
then A62: PR /. z = ((((Proj (k,n)) * g) /. (z + x0)) - (((Proj (k,n)) * g) /. x0)) - (z * (diff (((Proj (k,n)) * g),x0))) by RLVECT_4:1;
reconsider zz = z as Element of REAL by XREAL_0:def 1;
dom ((Proj (k,n)) * g) c= dom g by RELAT_1:25;
then A63: ((Proj (k,n)) * R) . z = ((((Proj (k,n)) * g) /. (z + x0)) - (((Proj (k,n)) * g) /. x0)) - (((Proj (k,n)) * L) . zz) by A61, A49, A30;
consider y being Element of REAL n such that
A64: ( 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 A20;
A65: y . k = (proj (1,1)) . (z * (diff (((Proj (k,n)) * g),x0))) by A64, A49;
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
A66: 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 /. zz) by FUNCT_1:13;
then ((Proj (k,n)) * L) . z = <*((proj (k,n)) . y1)*> by A64, PDIFF_1:def 4;
then ((Proj (k,n)) * L) . z = <*((proj (1,1)) . (z * (diff (((Proj (k,n)) * g),x0))))*> by A65, PDIFF_1:def 1;
then (|.z.| ") * ||.(((Proj (k,n)) * R) /. zz).|| < r0 by A58, A62, A63, A66, PDIFF_1:1;
hence (|.z.| ") * ||.(((Proj (k,n)) * R) /. z).|| < r0 ; :: thesis: verum
end;
hence S3[k,dd] by A51, A56, XXREAL_0:21; :: thesis: verum
end;
consider dd being FinSequence of REAL such that
A67: ( dom dd = Seg n & ( for i being Nat st i in Seg n holds
S3[i,dd /. i] ) ) from RECDEF_1:sch 17(A47);
 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 A67, FINSEQ_1:def 3;
then A68: min_p dd in dom dd by RFINSEQ2:def 2;
then A69: dd /. (min_p dd) > 0 by A67;
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 A70: ( z <> 0 & |.z.| < d ) ; :: thesis: (|.z.| ") * ||.(R /. z).|| < r
reconsider z = z as Element of REAL by XREAL_0:def 1;
reconsider Rz = R /. z as Element of REAL n by REAL_NS1:def 4;
reconsider zr0 = (|.z.| * r0) ^2 as Element of REAL by XREAL_0:def 1;
reconsider R0 = n |-> zr0 as Element of n -tuples_on REAL ;
reconsider SRz = sqr Rz as Element of n -tuples_on REAL ;
A71: |.z.| > 0 by A70, COMPLEX1:47;
A72: 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 A73: 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 A74: (sqr Rz) . i = (Rz . i) ^2 by RVSUM_1:def 2;
( 1 <= i & i <= n ) by A73, FINSEQ_1:1;
then ( 1 <= i & i <= len dd ) by A67, FINSEQ_1:def 3;
then d <= dd . i by RFINSEQ2:2;
then d <= dd /. i by A73, A67, PARTFUN1:def 6;
then |.z.| < dd /. i by A70, XXREAL_0:2;
then (|.z.| ") * ||.(((Proj (i,n)) * R) /. z).|| < r0 by A70, A73, A67;
then A75: ||.(((Proj (i,n)) * R) /. z).|| < r0 / (|.z.| ") by A71, XREAL_1:81;
Rz . i in REAL by XREAL_0:def 1;
then 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.| * r0 by A75, JORDAN2C:10;
then |.(Rz . i).| ^2 < (|.z.| * r0) ^2 by COMPLEX1:46, SQUARE_1:16;
then (Rz . i0) ^2 < (|.z.| * r0) ^2 by COMPLEX1:75;
hence SRz . i0 < R0 . i0 by A73, A74, FINSEQ_2:57; :: thesis: verum
end;
A76: 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;
A77: (|.z.| * r0) ^2 >= 0 by XREAL_1:63;
A78: 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 A72; :: thesis: verum
end;
A79: sqrt n > 0 by SQUARE_1:25;
for i0 being Nat st i0 in Seg n holds
SRz . i0 <= R0 . i0 by A72;
then Sum SRz < Sum R0 by A78, RVSUM_1:83;
then Sum (sqr Rz) < n * ((|.z.| * r0) ^2) by RVSUM_1:80;
then |.Rz.| < sqrt (n * ((|.z.| * r0) ^2)) by A76, RVSUM_1:84, SQUARE_1:27;
then |.Rz.| < (sqrt n) * (sqrt ((|.z.| * r0) ^2)) by A77, SQUARE_1:29;
then |.Rz.| < (sqrt n) * |.(|.z.| * r0).| by COMPLEX1:72;
then |.Rz.| < (sqrt n) * (|.z.| * r0) by A45, A44, A71, ABSVALUE:def 1;
then |.Rz.| < ((sqrt n) * r0) * |.z.| ;
then |.Rz.| / |.z.| < (sqrt n) * r0 by A71, XREAL_1:83;
then (|.z.| ") * ||.(R /. z).|| < ((sqrt n) * ((sqrt n) ")) * r by REAL_NS1:1;
then (|.z.| ") * ||.(R /. z).|| < 1 * r by A79, XCMPLX_0:def 7;
then (|.z.| ") * ||.(R /. z).|| < r ;
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 A69, A68, 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 A14, RCOMP_1:def 6;
now :: thesis: for x being object st x in N holds
x in dom g
let x be object ; :: thesis: ( x in N implies x in dom g )
assume A80: x in N ; :: thesis: x in dom g
then reconsider y = x as Real ;
A81: |.(y - x0).| < min d by A80, RCOMP_1:1;
1 <= n by NAT_1:14;
then A82: ( 1 in Seg n & 1 in dom d ) by A12;
then A83: ].(x0 - (d /. 1)),(x0 + (d /. 1)).[ c= dom ((Proj (1,n)) * g) by A12;
dom ((Proj (1,n)) * g) c= dom g by RELAT_1:25;
then A84: ].(x0 - (d /. 1)),(x0 + (d /. 1)).[ c= dom g by A83;
len d = n by A12, 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 A82, PARTFUN1:def 6;
then |.(y - x0).| < d /. 1 by A81, XXREAL_0:2;
then y in ].(x0 - (d /. 1)),(x0 + (d /. 1)).[ by RCOMP_1:1;
hence x in dom g by A84; :: thesis: verum
end;
then A85: N c= dom g ;
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))
A86: dom R = REAL by PARTFUN1:def 2;
reconsider dxx0 = x - x0 as Element of REAL by XREAL_0:def 1;
R /. (x - x0) = R . dxx0 by A86, PARTFUN1:def 6
.= ((g /. ((x - x0) + x0)) - (g /. x0)) - (L /. (x - x0)) by A29 ;
then R /. (x - x0) = ((g /. x) - (g /. x0)) + (- (L0 /. (x - x0))) ;
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 A85, NDIFF_3:def 3; :: thesis: verum