let m, n be non zero Nat; :: thesis: for g being PartFunc of (REAL-NS m),(REAL-NS n)
for x0 being Point of (REAL-NS m) holds
( g is_differentiable_in x0 iff for i being Nat st 1 <= i & i <= n holds
(Proj (i,n)) * g is_differentiable_in x0 )
let g be PartFunc of (REAL-NS m),(REAL-NS n); :: thesis: for x0 being Point of (REAL-NS m) holds
( g is_differentiable_in x0 iff for i being Nat st 1 <= i & i <= n holds
(Proj (i,n)) * g is_differentiable_in x0 )
let x0 be Point of (REAL-NS m); :: thesis: ( g is_differentiable_in x0 iff for i being Nat st 1 <= i & i <= n holds
(Proj (i,n)) * g is_differentiable_in x0 )
set RB = R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n));
( ( for i being Nat st 1 <= i & i <= n holds
(Proj (i,n)) * g is_differentiable_in x0 ) implies g is_differentiable_in x0 )

proof

assume A1: for i being Nat st 1 <= i & i <= n holds
(Proj (i,n)) * g is_differentiable_in x0 ; :: thesis: g is_differentiable_in x0
defpred S₁[ Nat, Element of REAL ] means ( $2 > 0 & { y where y is Point of (REAL-NS m) : ||.(y - x0).|| < $2 } c= dom ((Proj ($1,n)) * g) & ex Ri being RestFunc of (REAL-NS m),(REAL-NS 1) st
for x being Point of (REAL-NS m) st x in { y where y is Point of (REAL-NS m) : ||.(y - x0).|| < $2 } holds
(((Proj ($1,n)) * g) /. x) - (((Proj ($1,n)) * g) /. x0) = ((diff (((Proj ($1,n)) * g),x0)) . (x - x0)) + (Ri /. (x - x0)) );
A2: for k being Nat st k in Seg n holds
ex dk being Element of REAL st S₁[k,dk]

proof

let k be 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 Rk being RestFunc of (REAL-NS m),(REAL-NS 1) st
for x being Point of (REAL-NS m) st x in Nk holds
(((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((diff (((Proj (k,n)) * g),x0)) . (x - x0)) + (Rk /. (x - x0)) ) by NDIFF_1:def 7;
consider dk being Real such that
A4: ( 0 < dk & { y where y is Point of (REAL-NS m) : ||.(y - x0).|| < dk } c= Nk ) by NFCONT_1:def 1;
reconsider dk = dk as Element of REAL by XREAL_0:def 1;
take dk ; :: thesis: S₁[k,dk]
thus 0 < dk by A4; :: thesis: ( { y where y is Point of (REAL-NS m) : ||.(y - x0).|| < dk } c= dom ((Proj (k,n)) * g) & ex Ri being RestFunc of (REAL-NS m),(REAL-NS 1) st
for x being Point of (REAL-NS m) st x in { y where y is Point of (REAL-NS m) : ||.(y - x0).|| < dk } holds
(((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((diff (((Proj (k,n)) * g),x0)) . (x - x0)) + (Ri /. (x - x0)) )
thus { y where y is Point of (REAL-NS m) : ||.(y - x0).|| < dk } c= dom ((Proj (k,n)) * g) by A4, A3, XBOOLE_1:1; :: thesis: ex Ri being RestFunc of (REAL-NS m),(REAL-NS 1) st
for x being Point of (REAL-NS m) st x in { y where y is Point of (REAL-NS m) : ||.(y - x0).|| < dk } holds
(((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((diff (((Proj (k,n)) * g),x0)) . (x - x0)) + (Ri /. (x - x0))
thus ex Rk being RestFunc of (REAL-NS m),(REAL-NS 1) st
for x being Point of (REAL-NS m) st x in { y where y is Point of (REAL-NS m) : ||.(y - x0).|| < dk } holds
(((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((diff (((Proj (k,n)) * g),x0)) . (x - x0)) + (Rk /. (x - x0)) :: thesis: verum

proof

consider Rk being RestFunc of (REAL-NS m),(REAL-NS 1) such that
A5: for x being Point of (REAL-NS m) st x in Nk holds
(((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((diff (((Proj (k,n)) * g),x0)) . (x - x0)) + (Rk /. (x - x0)) by A3;
take Rk ; :: thesis: for x being Point of (REAL-NS m) st x in { y where y is Point of (REAL-NS m) : ||.(y - x0).|| < dk } holds
(((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((diff (((Proj (k,n)) * g),x0)) . (x - x0)) + (Rk /. (x - x0))
thus for x being Point of (REAL-NS m) st x in { y where y is Point of (REAL-NS m) : ||.(y - x0).|| < dk } holds
(((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((diff (((Proj (k,n)) * g),x0)) . (x - x0)) + (Rk /. (x - x0)) by A4, A5; :: thesis: verum

end;

end;

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

proof

let x be Point of (REAL-NS m); :: thesis: ex y being Point of (REAL-NS n) st S₂[x,y]
defpred S₃[ Nat, set ] means $2 = (proj (1,1)) . ((diff (((Proj ($1,n)) * g),x0)) . x);
A10: for i being Nat st i in Seg n holds
ex r being Element of REAL st S₃[i,r]

proof

let i be Nat; :: thesis: ( i in Seg n implies ex r being Element of REAL st S₃[i,r] )
assume i in Seg n ; :: thesis: ex r being Element of REAL st S₃[i,r]
(proj (1,1)) . ((diff (((Proj (i,n)) * g),x0)) . x) in REAL by XREAL_0:def 1;
hence ex r being Element of REAL st S₃[i,r] ; :: thesis: verum

end;

consider y being FinSequence of REAL such that
A11: ( dom y = Seg n & ( for i being Nat st i in Seg n holds
S₃[i,y /. i] ) ) from RECDEF_1:sch 17(A10);
reconsider nn = n as Element of NAT by ORDINAL1:def 12;
len y = nn by A11, FINSEQ_1:def 3;
then reconsider y = y as Element of REAL n by FINSEQ_2:92;

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

let i be Nat; :: thesis: ( i in Seg n implies y . i = (proj (1,1)) . ((diff (((Proj (i,n)) * g),x0)) . x) )
assume i in Seg n ; :: thesis: y . i = (proj (1,1)) . ((diff (((Proj (i,n)) * g),x0)) . x)
then ( S₃[i,y /. i] & y /. i = y . i ) by A11, PARTFUN1:def 6;
hence y . i = (proj (1,1)) . ((diff (((Proj (i,n)) * g),x0)) . x) ; :: 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 Nat st i in Seg n holds
y . i = (proj (1,1)) . ((diff (((Proj (i,n)) * g),x0)) . x) ) ) by A12;
hence ex y0 being Point of (REAL-NS n) st S₂[x,y0] ; :: thesis: verum

end;

consider L being Function of (REAL-NS m),(REAL-NS n) such that
A13: for x being Point of (REAL-NS m) holds S₂[x,L . x] from FUNCT_2:sch 3(A9);
A14: for x, y being VECTOR of (REAL-NS m) holds L . (x + y) = (L . x) + (L . y)

proof

let x, y be VECTOR of (REAL-NS m); :: thesis: L . (x + y) = (L . x) + (L . y)
consider Lx being Element of REAL n such that
A15: ( L . x = Lx & ( for i being Nat st i in Seg n holds
Lx . i = (proj (1,1)) . ((diff (((Proj (i,n)) * g),x0)) . x) ) ) by A13;
consider Ly being Element of REAL n such that
A16: ( L . y = Ly & ( for i being Nat st i in Seg n holds
Ly . i = (proj (1,1)) . ((diff (((Proj (i,n)) * g),x0)) . y) ) ) by A13;
consider Lxy being Element of REAL n such that
A17: ( L . (x + y) = Lxy & ( for i being Nat st i in Seg n holds
Lxy . i = (proj (1,1)) . ((diff (((Proj (i,n)) * g),x0)) . (x + y)) ) ) by A13;
dom Lxy = Seg n by FINSEQ_1:89;
then A18: dom Lxy = dom (Lx + Ly) by FINSEQ_1:89;
for i0 being Nat st i0 in dom Lxy holds
Lxy . i0 = (Lx + Ly) . i0

proof

let i0 be Nat; :: thesis: ( i0 in dom Lxy implies Lxy . i0 = (Lx + Ly) . i0 )
reconsider i = i0 as Nat ;
assume i0 in dom Lxy ; :: thesis: Lxy . i0 = (Lx + Ly) . i0
then i in Seg n by FINSEQ_1:89;
then A19: ( Lxy . i = (proj (1,1)) . ((diff (((Proj (i,n)) * g),x0)) . (x + y)) & Lx . i = (proj (1,1)) . ((diff (((Proj (i,n)) * g),x0)) . x) & Ly . i = (proj (1,1)) . ((diff (((Proj (i,n)) * g),x0)) . y) ) by A15, A16, A17;
diff (((Proj (i,n)) * g),x0) is LinearOperator of (REAL-NS m),(REAL-NS 1) by LOPBAN_1:def 9;
then A20: (diff (((Proj (i,n)) * g),x0)) . (x + y) = ((diff (((Proj (i,n)) * g),x0)) . x) + ((diff (((Proj (i,n)) * g),x0)) . y) by VECTSP_1:def 20;
reconsider Diffxy = (diff (((Proj (i,n)) * g),x0)) . (x + y) as Element of REAL 1 by REAL_NS1:def 4;
reconsider Diffx = (diff (((Proj (i,n)) * g),x0)) . x as Element of REAL 1 by REAL_NS1:def 4;
reconsider Diffy = (diff (((Proj (i,n)) * g),x0)) . y as Element of REAL 1 by REAL_NS1:def 4;
Diffxy = Diffx + Diffy by A20, REAL_NS1:2;
then Lxy . i0 = (Diffx + Diffy) . 1 by A19, PDIFF_1:def 1;
then Lxy . i0 = (Diffx . 1) + (Diffy . 1) by RVSUM_1:11;
then Lxy . i0 = (Lx . i0) + (Diffy . 1) by A19, PDIFF_1:def 1;
then Lxy . i0 = (Lx . i0) + (Ly . i0) by A19, PDIFF_1:def 1;
hence Lxy . i0 = (Lx + Ly) . i0 by RVSUM_1:11; :: thesis: verum

end;

then Lxy = Lx + Ly by A18, FINSEQ_1:13;
hence L . (x + y) = (L . x) + (L . y) by A15, A16, A17, REAL_NS1:2; :: thesis: verum

end;

for x being VECTOR of (REAL-NS m)
for r being Real holds L . (r * x) = r * (L . x)

proof

let x be VECTOR of (REAL-NS m); :: thesis: for r being Real holds L . (r * x) = r * (L . x)
let r be Real; :: thesis: L . (r * x) = r * (L . x)
consider Lx being Element of REAL n such that
A21: ( L . x = Lx & ( for i being Nat st i in Seg n holds
Lx . i = (proj (1,1)) . ((diff (((Proj (i,n)) * g),x0)) . x) ) ) by A13;
consider Lrx being Element of REAL n such that
A22: ( L . (r * x) = Lrx & ( for i being Nat st i in Seg n holds
Lrx . i = (proj (1,1)) . ((diff (((Proj (i,n)) * g),x0)) . (r * x)) ) ) by A13;
dom (r * Lx) = Seg n by FINSEQ_1:89;
then A23: dom (r * Lx) = dom Lrx by FINSEQ_1:89;
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 Nat ;
assume i0 in dom (r * Lx) ; :: thesis: (r * Lx) . i0 = Lrx . i0
then i0 in Seg n by FINSEQ_1:89;
then A24: ( Lx . i = (proj (1,1)) . ((diff (((Proj (i,n)) * g),x0)) . x) & Lrx . i = (proj (1,1)) . ((diff (((Proj (i,n)) * g),x0)) . (r * x)) ) by A21, A22;
diff (((Proj (i,n)) * g),x0) is LinearOperator of (REAL-NS m),(REAL-NS 1) by LOPBAN_1:def 9;
then A25: (diff (((Proj (i,n)) * g),x0)) . (r * x) = r * ((diff (((Proj (i,n)) * g),x0)) . x) by LOPBAN_1:def 5;
reconsider Diffrx = (diff (((Proj (i,n)) * g),x0)) . (r * x) as Element of REAL 1 by REAL_NS1:def 4;
reconsider Diffx = (diff (((Proj (i,n)) * g),x0)) . x as Element of REAL 1 by REAL_NS1:def 4;
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, 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 * x) = r * (L . x) by A21, A22, REAL_NS1:3; :: thesis: verum

end;

then reconsider L = L as LinearOperator of (REAL-NS m),(REAL-NS n) by A14, LOPBAN_1:def 5, VECTSP_1:def 20;
reconsider L0 = L as Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))) by LOPBAN_1:def 9;
deffunc H₁( Element of (REAL-NS m)) -> Element of the carrier of (REAL-NS n) = ((g /. ($1 + x0)) - (g /. x0)) - (L . $1);
consider R being Function of (REAL-NS m),(REAL-NS n) such that
A26: for x being Element of (REAL-NS m) holds R . x = H₁(x) from FUNCT_2:sch 4();
A27: for x being Element of (REAL-NS m)
for i being 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-NS m); :: thesis: for i being 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 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
A28: i in Seg n and
A29: 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)
x0 - x0 = 0. (REAL-NS m) by RLVECT_1:15;
then x0 - x0 = 0* m by REAL_NS1:def 4;
then ||.(x0 - x0).|| = |.(0* m).| by REAL_NS1:1;
then A30: ||.(x0 - x0).|| = 0 by EUCLID:7;
A31: ( 0 < d /. i & { y where y is Point of (REAL-NS m) : ||.(y - x0).|| < d /. i } c= dom ((Proj (i,n)) * g) ) by A28, A6;
then x0 in { y where y is Point of (REAL-NS m) : ||.(y - x0).|| < d /. i } by A30;
then A32: x0 in dom ((Proj (i,n)) * g) by A31;
A33: 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 Lx1 = L . x as Point of (REAL-NS n) ;
A34: ( - 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 A35: (gxx0 + (- gx0)) + (- Lx) = ((g /. (x + x0)) + ((- 1) * (g /. x0))) + ((- 1) * (L . x)) by A34, REAL_NS1:2;
gxx0 - gx0 = (g /. (x + x0)) - (g /. x0) by REAL_NS1:5;
then A36: ((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 A26;
then ((Proj (i,n)) * R) . x = ((Proj (i,n)) . ((g /. (x + x0)) + ((- 1) * (g /. x0)))) + ((Proj (i,n)) . ((- 1) * (L . x))) by A36, A35, Th26;
then A37: ((Proj (i,n)) * R) . x = (((Proj (i,n)) . (g /. (x + x0))) + ((Proj (i,n)) . ((- 1) * (g /. x0)))) + ((Proj (i,n)) . ((- 1) * (L . x))) by Th26;
( (Proj (i,n)) . ((- 1) * (g /. x0)) = (- 1) * ((Proj (i,n)) . (g /. x0)) & (Proj (i,n)) . ((- 1) * Lx1) = (- 1) * ((Proj (i,n)) . Lx1) ) by Th27;
then ((Proj (i,n)) * R) . x = (((Proj (i,n)) . (g /. (x + x0))) + (- ((Proj (i,n)) . (g /. x0)))) + ((- 1) * ((Proj (i,n)) . (L . x))) by A37, RLVECT_1:16;
then ((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;
then ((Proj (i,n)) * R) . x = (((Proj (i,n)) . (g /. (x + x0))) - ((Proj (i,n)) . (g /. x0))) + (- ((Proj (i,n)) . (L . x))) by RLVECT_1:def 11;
then A38: ((Proj (i,n)) * R) . x = (((Proj (i,n)) . (g /. (x + x0))) - ((Proj (i,n)) . (g /. x0))) - ((Proj (i,n)) . (L . x)) by RLVECT_1:def 11;
( g /. (x + x0) in the carrier of (REAL-NS n) & g /. x0 in the carrier of (REAL-NS n) ) ;
then A39: ( g /. (x + x0) in dom (Proj (i,n)) & g /. x0 in dom (Proj (i,n)) ) by FUNCT_2:def 1;
A40: (Proj (i,n)) . (g /. (x + x0)) = (Proj (i,n)) /. (g /. (x + x0))
.= ((Proj (i,n)) * g) /. (x + x0) by A29, A39, PARTFUN2:4 ;
(Proj (i,n)) . (g /. x0) = (Proj (i,n)) /. (g /. x0)
.= ((Proj (i,n)) * g) /. x0 by A32, A33, A39, 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 A38, A40, FUNCT_2:15; :: thesis: verum

end;

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

proof

let k be Nat; :: thesis: ( k in Seg n implies ex dd being Element of REAL st S₃[k,dd] )
assume A45: 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
A46: ( Nk c= dom ((Proj (k,n)) * g) & ex PR being RestFunc of (REAL-NS m),(REAL-NS 1) st
for x being Point of (REAL-NS m) st x in Nk holds
(((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((diff (((Proj (k,n)) * g),x0)) . (x - x0)) + (PR /. (x - x0)) ) by NDIFF_1:def 7;
consider d0 being Real such that
A47: ( 0 < d0 & { y where y is Point of (REAL-NS m) : ||.(y - x0).|| < d0 } c= Nk ) by NFCONT_1:def 1;
consider PR being RestFunc of (REAL-NS m),(REAL-NS 1) such that
A48: for x being Point of (REAL-NS m) st x in Nk holds
(((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((diff (((Proj (k,n)) * g),x0)) . (x - x0)) + (PR /. (x - x0)) by A46;
PR is total by NDIFF_1:def 5;
then consider d1 being Real such that
A49: ( d1 > 0 & ( for z being Point of (REAL-NS m) st z <> 0. (REAL-NS m) & ||.z.|| < d1 holds
(||.z.|| ") * ||.(PR /. z).|| < ((sqrt n) ") * r ) ) by A43, NDIFF_1:23;
reconsider d0 = d0, d1 = d1 as Real ;
reconsider dd = min (d0,d1) as Element of REAL by XREAL_0:def 1;
take dd ; :: thesis: S₃[k,dd]
for z being Point of (REAL-NS m) st z <> 0. (REAL-NS m) & ||.z.|| < dd holds
(||.z.|| ") * ||.(((Proj (k,n)) * R) /. z).|| < ((sqrt n) ") * r

proof

let z be Point of (REAL-NS m); :: thesis: ( z <> 0. (REAL-NS m) & ||.z.|| < dd implies (||.z.|| ") * ||.(((Proj (k,n)) * R) /. z).|| < ((sqrt n) ") * r )
assume A50: ( z <> 0. (REAL-NS m) & ||.z.|| < dd ) ; :: thesis: (||.z.|| ") * ||.(((Proj (k,n)) * R) /. z).|| < ((sqrt n) ") * r
dd <= d1 by XXREAL_0:17;
then ||.z.|| < d1 by A50, XXREAL_0:2;
then A51: (||.z.|| ") * ||.(PR /. z).|| < ((sqrt n) ") * r by A50, A49;
dd <= d0 by XXREAL_0:17;
then A52: ||.z.|| < d0 by A50, XXREAL_0:2;
A53: (z + x0) - x0 = z by RLVECT_4:1;
then A54: z + x0 in { y where y is Point of (REAL-NS m) : ||.(y - x0).|| < d0 } by A52;
then z + x0 in Nk by A47;
then A55: z + x0 in dom ((Proj (k,n)) * g) by A46;
(((Proj (k,n)) * g) /. (z + x0)) - (((Proj (k,n)) * g) /. x0) = ((diff (((Proj (k,n)) * g),x0)) . ((z + x0) - x0)) + (PR /. ((z + x0) - x0)) by A54, A47, A48;
then A56: PR /. z = ((((Proj (k,n)) * g) /. (z + x0)) - (((Proj (k,n)) * g) /. x0)) - ((diff (((Proj (k,n)) * g),x0)) . z) by A53, RLVECT_4:1;
dom ((Proj (k,n)) * g) c= dom g by RELAT_1:25;
then A57: ((Proj (k,n)) * R) . z = ((((Proj (k,n)) * g) /. (z + x0)) - (((Proj (k,n)) * g) /. x0)) - (((Proj (k,n)) * L) . z) by A55, A45, A27;
consider y being Element of REAL n such that
A58: ( L . z = y & ( for i being Nat st i in Seg n holds
y . i = (proj (1,1)) . ((diff (((Proj (i,n)) * g),x0)) . z) ) ) by A13;
A59: y . k = (proj (1,1)) . ((diff (((Proj (k,n)) * g),x0)) . z) by A58, A45;
(diff (((Proj (k,n)) * g),x0)) . z is Element of REAL 1 by REAL_NS1:def 4;
then consider Dk being Element of REAL such that
A60: (diff (((Proj (k,n)) * g),x0)) . z = <*Dk*> by FINSEQ_2:97;
reconsider y1 = y as Point of (REAL-NS n) by REAL_NS1:def 4;
dom L = the carrier of (REAL-NS m) 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 A58, PDIFF_1:def 4;
then ((Proj (k,n)) * L) . z = <*((proj (1,1)) . ((diff (((Proj (k,n)) * g),x0)) . z))*> by A59, PDIFF_1:def 1;
hence (||.z.|| ") * ||.(((Proj (k,n)) * R) /. z).|| < ((sqrt n) ") * r by A51, A56, A57, A60, PDIFF_1:1; :: thesis: verum

end;

hence S₃[k,dd] by A47, A49, XXREAL_0:21; :: thesis: verum

end;

consider dd being FinSequence of REAL such that
A61: ( dom dd = Seg n & ( for i being Nat st i in Seg n holds
S₃[i,dd /. i] ) ) from RECDEF_1:sch 17(A44);
set d = min dd;
take min dd ; :: thesis: ( min dd > 0 & ( for z being Point of (REAL-NS m) st z <> 0. (REAL-NS m) & ||.z.|| < min dd holds
(||.z.|| ") * ||.(R /. z).|| < r ) )
reconsider nn = n as Element of NAT by ORDINAL1:def 12;
len dd = nn by A61, FINSEQ_1:def 3;
then A62: min_p dd in dom dd by RFINSEQ2:def 2;
then A63: dd /. (min_p dd) > 0 by A61;
for z being Point of (REAL-NS m) st z <> 0. (REAL-NS m) & ||.z.|| < min dd holds
(||.z.|| ") * ||.(R /. z).|| < r

proof

let z be Point of (REAL-NS m); :: thesis: ( z <> 0. (REAL-NS m) & ||.z.|| < min dd implies (||.z.|| ") * ||.(R /. z).|| < r )
assume A64: ( z <> 0. (REAL-NS m) & ||.z.|| < min dd ) ; :: thesis: (||.z.|| ") * ||.(R /. z).|| < r
reconsider Rz = R /. z as Element of REAL n by REAL_NS1:def 4;
reconsider zr = (||.z.|| * (((sqrt n) ") * r)) ^2 as Element of REAL by XREAL_0:def 1;
reconsider R0 = n |-> zr as Element of n -tuples_on REAL ;
reconsider SRz = sqr Rz as Element of n -tuples_on REAL ;
||.z.|| <> 0 by A64, NORMSP_0:def 5;
then A65: ||.z.|| > 0 by NORMSP_1:4;
A66: 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 Nat ;
assume A67: 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 A68: (sqr Rz) . i = (Rz . i) ^2 by RVSUM_1:def 2;
reconsider nn = n as Element of NAT by ORDINAL1:def 12;
( 1 <= i & i <= nn ) by A67, FINSEQ_1:1;
then ( 1 <= i & i <= len dd ) by A61, FINSEQ_1:def 3;
then min dd <= dd . i by RFINSEQ2:2;
then min dd <= dd /. i by A67, A61, PARTFUN1:def 6;
then ||.z.|| < dd /. i by A64, XXREAL_0:2;
then (||.z.|| ") * ||.(((Proj (i,n)) * R) /. z).|| < ((sqrt n) ") * r by A64, A67, A61;
then A69: ||.(((Proj (i,n)) * R) /. z).|| < (((sqrt n) ") * r) / (||.z.|| ") by A65, 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.|| * (((sqrt n) ") * r) by A69, 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 A67, A68, FINSEQ_2:57; :: thesis: verum

end;

A70: 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;

A71: (||.z.|| * (((sqrt n) ") * r)) ^2 >= 0 by XREAL_1:63;
A72: 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 A66; :: thesis: verum

end;

A73: sqrt n > 0 by SQUARE_1:25;
for i0 being Nat st i0 in Seg n holds
SRz . i0 <= R0 . i0 by A66;
then Sum SRz < Sum R0 by A72, 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 A70, RVSUM_1:84, SQUARE_1:27;
then |.Rz.| < (sqrt n) * (sqrt ((||.z.|| * (((sqrt n) ") * r)) ^2)) by A71, SQUARE_1:29;
then |.Rz.| < (sqrt n) * |.(||.z.|| * (((sqrt n) ") * r)).| by COMPLEX1:72;
then |.Rz.| < (sqrt n) * (||.z.|| * (((sqrt n) ") * r)) by A42, A41, A65, ABSVALUE:def 1;
then |.Rz.| < ((sqrt n) * (((sqrt n) ") * r)) * ||.z.|| ;
then |.Rz.| / ||.z.|| < (sqrt n) * (((sqrt n) ") * r) by A65, XREAL_1:83;
then (||.z.|| ") * ||.(R /. z).|| < ((sqrt n) * ((sqrt n) ")) * r by REAL_NS1:1;
then (||.z.|| ") * ||.(R /. z).|| < 1 * r by A73, XCMPLX_0:def 7;
hence (||.z.|| ") * ||.(R /. z).|| < r ; :: thesis: verum

end;

hence ( min dd > 0 & ( for z being Point of (REAL-NS m) st z <> 0. (REAL-NS m) & ||.z.|| < min dd holds
(||.z.|| ") * ||.(R /. z).|| < r ) ) by A63, A62, PARTFUN1:def 6; :: thesis: verum

end;

then reconsider R = R as RestFunc of (REAL-NS m),(REAL-NS n) by NDIFF_1:23;
set N = { y where y is Point of (REAL-NS m) : ||.(y - x0).|| < min d } ;
reconsider N = { y where y is Point of (REAL-NS m) : ||.(y - x0).|| < min d } as Neighbourhood of x0 by A8, NFCONT_1:3;

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 x in N ; :: thesis: x in dom g
then consider y being Point of (REAL-NS m) such that
A74: ( x = y & ||.(y - x0).|| < min d ) ;
1 <= n by NAT_1:14;
then A75: ( 1 in Seg n & 1 in dom d ) by A6;
then A76: { z where z is Point of (REAL-NS m) : ||.(z - x0).|| < d /. 1 } c= dom ((Proj (1,n)) * g) by A6;
dom ((Proj (1,n)) * g) c= dom g by RELAT_1:25;
then A77: { z where z is Point of (REAL-NS m) : ||.(z - x0).|| < d /. 1 } c= dom g by A76, XBOOLE_1:1;
reconsider nn = n as Element of NAT by ORDINAL1:def 12;
len d = nn by A6, 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 A75, PARTFUN1:def 6;
then ||.(y - x0).|| < d /. 1 by A74, XXREAL_0:2;
then y in { z where z is Point of (REAL-NS m) : ||.(z - x0).|| < d /. 1 } ;
hence x in dom g by A74, A77; :: thesis: verum

end;

then A78: N c= dom g by TARSKI:def 3;
ex L being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))) ex R being RestFunc of (REAL-NS m),(REAL-NS n) st
for x being Point of (REAL-NS m) 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 m),(REAL-NS n) st
for x being Point of (REAL-NS m) st x in N holds
(g /. x) - (g /. x0) = (L0 . (x - x0)) + (R /. (x - x0))
take R ; :: thesis: for x being Point of (REAL-NS m) st x in N holds
(g /. x) - (g /. x0) = (L0 . (x - x0)) + (R /. (x - x0))

hereby :: thesis: verum

let x be Point of (REAL-NS m); :: 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))
A79: dom R = the carrier of (REAL-NS m) by PARTFUN1:def 2;
R . (x - x0) = ((g /. ((x - x0) + x0)) - (g /. x0)) - (L . (x - x0)) by A26;
then R . (x - x0) = ((g /. (x - (x0 - x0))) - (g /. x0)) - (L0 . (x - x0)) by RLVECT_1:29;
then R . (x - x0) = ((g /. (x - (x0 + (- x0)))) - (g /. x0)) - (L0 . (x - x0)) by RLVECT_1:def 11;
then R . (x - x0) = ((g /. (x - (0. (REAL-NS m)))) - (g /. x0)) - (L0 . (x - x0)) by RLVECT_1:5;
then R . (x - x0) = ((g /. x) - (g /. x0)) - (L0 . (x - x0)) by RLVECT_1:13;
then R . (x - x0) = ((g /. x) - (g /. x0)) + (- (L0 . (x - x0))) by RLVECT_1:def 11;
then R /. (x - x0) = ((g /. x) - (g /. x0)) + (- (L0 . (x - x0))) by A79, 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;

end;

hence g is_differentiable_in x0 by A78, NDIFF_1:def 6; :: thesis: verum

end;

hence ( g is_differentiable_in x0 iff for i being Nat st 1 <= i & i <= n holds
(Proj (i,n)) * g is_differentiable_in x0 ) by Th28; :: thesis: verum