let m, n be non empty Element of 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 Element of 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 Element of 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 Element of 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);
set RB1 = R_NormSpace_of_BoundedLinearOperators (REAL-NS m),(REAL-NS 1);
( ( 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 )

proof

assume AS: 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 & { y where y is Point of (REAL-NS m) : ||.(y - x0).|| < $2 } c= dom ((Proj $1,n) * g) & ex Ri being REST 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)) );
A1: 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:3;
then (Proj k,n) * g is_differentiable_in x0 by AS;
then consider Nk being Neighbourhood of x0 such that
B1: ( Nk c= dom ((Proj k,n) * g) & ex Rk being REST 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
B2: ( 0 < dk & { y where y is Point of (REAL-NS m) : ||.(y - x0).|| < dk } c= Nk ) by NFCONT_1:def 3;
reconsider dk = dk as Element of REAL ;
take dk ; :: thesis: S₁[k,dk]
thus 0 < dk by B2; :: thesis: ( { y where y is Point of (REAL-NS m) : ||.(y - x0).|| < dk } c= dom ((Proj k,n) * g) & ex Ri being REST 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 B2, B1, XBOOLE_1:1; :: thesis: ex Ri being REST 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 REST 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 REST of (REAL-NS m),(REAL-NS 1) such that
B3: 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 B1;
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 B2, B3; :: thesis: verum

end;

end;

consider d being FinSequence of REAL such that
A2: ( 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(A1);
set d0 = min d;
len d = n by A2, FINSEQ_1:def 3;
then AP1: min_p d in dom d by RFINSEQ2:def 2;
then d /. (min_p d) > 0 by A2;
then AP2: min d > 0 by AP1, PARTFUN1:def 8;
defpred S₂[ set , 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) . ((diff ((Proj i,n) * g),x0) . $1) ) );
A3: 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₃[ Element of NAT , set ] means $2 = (proj 1,1) . ((diff ((Proj $1,n) * g),x0) . x);
P71: 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
P73: ( 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(P71);
len y = n by P73, FINSEQ_1:def 3;
then reconsider y = y as Element of REAL n by FINSEQ_2:110;

P77: now

let i be Element of 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 P73, PARTFUN1:def 8;
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 Element of NAT st i in Seg n holds
y . i = (proj 1,1) . ((diff ((Proj i,n) * g),x0) . x) ) ) by P77;
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
A4: for x being Point of (REAL-NS m) holds S₂[x,L . x] from FUNCT_2:sch 3(A3);
AD1: 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
B1: ( L . x = Lx & ( for i being Element of NAT st i in Seg n holds
Lx . i = (proj 1,1) . ((diff ((Proj i,n) * g),x0) . x) ) ) by A4;
consider Ly being Element of REAL n such that
B2: ( L . y = Ly & ( for i being Element of NAT st i in Seg n holds
Ly . i = (proj 1,1) . ((diff ((Proj i,n) * g),x0) . y) ) ) by A4;
consider Lxy being Element of REAL n such that
B3: ( L . (x + y) = Lxy & ( for i being Element of NAT st i in Seg n holds
Lxy . i = (proj 1,1) . ((diff ((Proj i,n) * g),x0) . (x + y)) ) ) by A4;
dom Lxy = Seg n by EUCLID:3;
then B8: dom Lxy = dom (Lx + Ly) by EUCLID:3;
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 Element of NAT by ORDINAL1:def 13;
assume i0 in dom Lxy ; :: thesis: Lxy . i0 = (Lx + Ly) . i0
then i in Seg n by EUCLID:3;
then B7: ( 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 B1, B2, B3;
diff ((Proj i,n) * g),x0 is LinearOperator of (REAL-NS m),(REAL-NS 1) by LOPBAN_1:def 10;
then B6: (diff ((Proj i,n) * g),x0) . (x + y) = ((diff ((Proj i,n) * g),x0) . x) + ((diff ((Proj i,n) * g),x0) . y) by GRCAT_1:def 13;
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 B6, REAL_NS1:2;
then Lxy . i0 = (Diffx + Diffy) . 1 by B7, PDIFF_1:def 1;
then Lxy . i0 = (Diffx . 1) + (Diffy . 1) by RVSUM_1:27;
then Lxy . i0 = (Lx . i0) + (Diffy . 1) by B7, PDIFF_1:def 1;
then Lxy . i0 = (Lx . i0) + (Ly . i0) by B7, PDIFF_1:def 1;
hence Lxy . i0 = (Lx + Ly) . i0 by RVSUM_1:27; :: thesis: verum

end;

then Lxy = Lx + Ly by B8, FINSEQ_1:17;
hence L . (x + y) = (L . x) + (L . y) by B1, B2, B3, 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
B1: ( L . x = Lx & ( for i being Element of NAT st i in Seg n holds
Lx . i = (proj 1,1) . ((diff ((Proj i,n) * g),x0) . x) ) ) by A4;
consider Lrx being Element of REAL n such that
B2: ( L . (r * x) = Lrx & ( for i being Element of NAT st i in Seg n holds
Lrx . i = (proj 1,1) . ((diff ((Proj i,n) * g),x0) . (r * x)) ) ) by A4;
dom (r * Lx) = Seg n by EUCLID:3;
then B3: dom (r * Lx) = dom Lrx by EUCLID:3;
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 13;
assume i0 in dom (r * Lx) ; :: thesis: (r * Lx) . i0 = Lrx . i0
then i0 in Seg n by EUCLID:3;
then B7: ( 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 B1, B2;
diff ((Proj i,n) * g),x0 is LinearOperator of (REAL-NS m),(REAL-NS 1) by LOPBAN_1:def 10;
then B5: (diff ((Proj i,n) * g),x0) . (r * x) = r * ((diff ((Proj i,n) * g),x0) . x) by LOPBAN_1:def 6;
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 B5, REAL_NS1:3;
then Lrx . i0 = (r * Diffx) . 1 by B7, PDIFF_1:def 1;
then Lrx . i0 = r * (Diffx . 1) by RVSUM_1:67;
then Lrx . i0 = r * (Lx . i0) by B7, PDIFF_1:def 1;
hence (r * Lx) . i0 = Lrx . i0 by RVSUM_1:67; :: thesis: verum

end;

then r * Lx = Lrx by B3, FINSEQ_1:17;
hence L . (r * x) = r * (L . x) by B1, B2, REAL_NS1:3; :: thesis: verum

end;

then reconsider L = L as LinearOperator of (REAL-NS m),(REAL-NS n) by AD1, GRCAT_1:def 13, LOPBAN_1:def 6;
reconsider L0 = L as Point of (R_NormSpace_of_BoundedLinearOperators (REAL-NS m),(REAL-NS n)) by LOPBAN_1:def 10;
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
A9: for x being Element of (REAL-NS m) holds R . x = H₁(x) from FUNCT_2:sch 4();
A10: for x being Element of (REAL-NS m)
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-NS m); :: 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
BS1: i in Seg n and
BS2: 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:28;
then x0 - x0 = 0* m by REAL_NS1:def 4;
then ||.(x0 - x0).|| = |.(0* m).| by REAL_NS1:1;
then P1: ||.(x0 - x0).|| = 0 by EUCLID:10;
P2: ( 0 < d /. i & { y where y is Point of (REAL-NS m) : ||.(y - x0).|| < d /. i } c= dom ((Proj i,n) * g) ) by BS1, A2;
then x0 in { y where y is Point of (REAL-NS m) : ||.(y - x0).|| < d /. i } by P1;
then P3: x0 in dom ((Proj i,n) * g) by P2;
P4: dom ((Proj i,n) * g) c= dom g by RELAT_1:44;
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) ;
B0: ( - 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 B2: (gxx0 + (- gx0)) + (- Lx) = ((g /. (x + x0)) + ((- 1) * (g /. x0))) + ((- 1) * (L . x)) by B0, REAL_NS1:2;
gxx0 - gx0 = (g /. (x + x0)) - (g /. x0) by REAL_NS1:5;
then B1: ((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:21;
then ((Proj i,n) * R) . x = (Proj i,n) . (((g /. (x + x0)) - (g /. x0)) - (L . x)) by A9;
then ((Proj i,n) * R) . x = ((Proj i,n) . ((g /. (x + x0)) + ((- 1) * (g /. x0)))) + ((Proj i,n) . ((- 1) * (L . x))) by B1, B2, DPREP1201;
then B3: ((Proj i,n) * R) . x = (((Proj i,n) . (g /. (x + x0))) + ((Proj i,n) . ((- 1) * (g /. x0)))) + ((Proj i,n) . ((- 1) * (L . x))) by DPREP1201;
( (Proj i,n) . ((- 1) * (g /. x0)) = (- 1) * ((Proj i,n) . (g /. x0)) & (Proj i,n) . ((- 1) * Lx1) = (- 1) * ((Proj i,n) . Lx1) ) by DPREP1202;
then ((Proj i,n) * R) . x = (((Proj i,n) . (g /. (x + x0))) + (- ((Proj i,n) . (g /. x0)))) + ((- 1) * ((Proj i,n) . (L . x))) by B3, RLVECT_1:29;
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:29;
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 14;
then C0: ((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 14;
( g /. (x + x0) in the carrier of (REAL-NS n) & g /. x0 in the carrier of (REAL-NS n) ) ;
then C1: ( g /. (x + x0) in dom (Proj i,n) & g /. x0 in dom (Proj i,n) ) by FUNCT_2:def 1;
C2: (Proj i,n) . (g /. (x + x0)) = (Proj i,n) /. (g /. (x + x0))
.= ((Proj i,n) * g) /. (x + x0) by BS2, C1, PARTFUN2:9 ;
(Proj i,n) . (g /. x0) = (Proj i,n) /. (g /. x0)
.= ((Proj i,n) * g) /. x0 by P3, P4, C1, PARTFUN2:9 ;
hence ((Proj i,n) * R) . x = ((((Proj i,n) * g) /. (x + x0)) - (((Proj i,n) * g) /. x0)) - (((Proj i,n) * L) . x) by C0, C2, FUNCT_2:21; :: 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 B1: 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;
DD0: sqrt n > 0 by SQUARE_1:93;
then DE0: ((sqrt n) " ) * r > 0 by B1, XREAL_1:131;
defpred S₃[ Element of 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 ) );
DD1: 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 D0: k in Seg n ; :: thesis: ex dd being Element of REAL st S₃[k,dd]
then ( 1 <= k & k <= n ) by FINSEQ_1:3;
then (Proj k,n) * g is_differentiable_in x0 by AS;
then consider Nk being Neighbourhood of x0 such that
D1: ( Nk c= dom ((Proj k,n) * g) & ex PR being REST 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
D2: ( 0 < d0 & { y where y is Point of (REAL-NS m) : ||.(y - x0).|| < d0 } c= Nk ) by NFCONT_1:def 3;
consider PR being REST of (REAL-NS m),(REAL-NS 1) such that
D3: 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 D1;
PR is total by NDIFF_1:def 5;
then consider d1 being Real such that
D4: ( 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 DE0, NDIFF_1:26;
set dd = min d0,d1;
take min d0,d1 ; :: thesis: S₃[k, min d0,d1]
for z being Point of (REAL-NS m) st z <> 0. (REAL-NS m) & ||.z.|| < min d0,d1 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.|| < min d0,d1 implies (||.z.|| " ) * ||.(((Proj k,n) * R) /. z).|| < ((sqrt n) " ) * r )
assume D6: ( z <> 0. (REAL-NS m) & ||.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 D6, XXREAL_0:2;
then D7: (||.z.|| " ) * ||.(PR /. z).|| < ((sqrt n) " ) * r by D6, D4;
min d0,d1 <= d0 by XXREAL_0:17;
then D8: ||.z.|| < d0 by D6, XXREAL_0:2;
D9: (z + x0) - x0 = z by RLVECT_4:1;
then E0: z + x0 in { y where y is Point of (REAL-NS m) : ||.(y - x0).|| < d0 } by D8;
then z + x0 in Nk by D2;
then E2: z + x0 in dom ((Proj k,n) * g) by D1;
(((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 E0, D2, D3;
then D10: PR /. z = ((((Proj k,n) * g) /. (z + x0)) - (((Proj k,n) * g) /. x0)) - ((diff ((Proj k,n) * g),x0) . z) by D9, RLVECT_4:1;
dom ((Proj k,n) * g) c= dom g by RELAT_1:44;
then E3: ((Proj k,n) * R) . z = ((((Proj k,n) * g) /. (z + x0)) - (((Proj k,n) * g) /. x0)) - (((Proj k,n) * L) . z) by E2, D0, A10;
consider y being Element of REAL n such that
D11: ( L . z = y & ( for i being Element of NAT st i in Seg n holds
y . i = (proj 1,1) . ((diff ((Proj i,n) * g),x0) . z) ) ) by A4;
D12: y . k = (proj 1,1) . ((diff ((Proj k,n) * g),x0) . z) by D11, D0;
(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
D13: (diff ((Proj k,n) * g),x0) . z = <*Dk*> by FINSEQ_2:117;
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:23;
then ((Proj k,n) * L) . z = <*((proj k,n) . y1)*> by D11, PDIFF_1:def 4;
then ((Proj k,n) * L) . z = <*((proj 1,1) . ((diff ((Proj k,n) * g),x0) . z))*> by D12, PDIFF_1:def 1;
hence (||.z.|| " ) * ||.(((Proj k,n) * R) /. z).|| < ((sqrt n) " ) * r by D7, D10, E3, D13, PDIFF_1:1; :: thesis: verum

end;

hence S₃[k, min d0,d1] by D2, D4, XXREAL_0:21; :: thesis: verum

end;

consider dd being FinSequence of REAL such that
DD2: ( 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(DD1);
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 ) )
len dd = n by DD2, FINSEQ_1:def 3;
then PP1: min_p dd in dom dd by RFINSEQ2:def 2;
then DD3: dd /. (min_p dd) > 0 by DD2;
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 G0: ( 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 R0 = n |-> ((||.z.|| * (((sqrt n) " ) * r)) ^2 ) as Element of n -tuples_on REAL by FINSEQ_2:132;
reconsider SRz = sqr Rz as Element of n -tuples_on REAL ;
||.z.|| <> 0 by G0, NORMSP_0:def 5;
then GG4: ||.z.|| > 0 by NORMSP_1:8;
DD4: 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 13;
assume G1: i0 in Seg n ; :: thesis: SRz . i0 < R0 . i0
then i in dom Rz by FINSEQ_2:144;
then (sqr Rz) . i = sqrreal . (Rz . i) by FUNCT_1:23;
then G3: (sqr Rz) . i = (Rz . i) ^2 by RVSUM_1:def 2;
( 1 <= i & i <= n ) by G1, FINSEQ_1:3;
then ( 1 <= i & i <= len dd ) by DD2, FINSEQ_1:def 3;
then min dd <= dd . i by RFINSEQ2:2;
then min dd <= dd /. i by G1, DD2, PARTFUN1:def 8;
then ||.z.|| < dd /. i by G0, XXREAL_0:2;
then (||.z.|| " ) * ||.(((Proj i,n) * R) /. z).|| < ((sqrt n) " ) * r by G0, G1, DD2;
then G5: ||.(((Proj i,n) * R) /. z).|| < (((sqrt n) " ) * r) / (||.z.|| " ) by GG4, XREAL_1:83;
reconsider Rzi = <*(Rz . i)*> as Element of REAL 1 by FINSEQ_2:118;
((Proj i,n) * R) . z = (Proj i,n) . (R . z) by FUNCT_2:21;
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 G5, JORDAN2C:12;
then |.(Rz . i).| ^2 < (||.z.|| * (((sqrt n) " ) * r)) ^2 by COMPLEX1:132, SQUARE_1:78;
then (Rz . i0) ^2 < (||.z.|| * (((sqrt n) " ) * r)) ^2 by COMPLEX1:161;
hence SRz . i0 < R0 . i0 by G1, G3, FINSEQ_2:71; :: thesis: verum

end;

DD8: 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:44;
then (sqr Rz) . i = sqrreal . (Rz . i) by FUNCT_1:23;
then (sqr Rz) . i = (Rz . i) ^2 by RVSUM_1:def 2;
hence 0 <= (sqr Rz) . i by XREAL_1:65; :: thesis: verum

end;

DD9: (||.z.|| * (((sqrt n) " ) * r)) ^2 >= 0 by XREAL_1:65;
DD5: 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 DD4; :: thesis: verum

end;

LP1: sqrt n > 0 by SQUARE_1:93;
for i0 being Nat st i0 in Seg n holds
SRz . i0 <= R0 . i0 by DD4;
then Sum SRz < Sum R0 by DD5, RVSUM_1:113;
then Sum (sqr Rz) < n * ((||.z.|| * (((sqrt n) " ) * r)) ^2 ) by RVSUM_1:110;
then |.Rz.| < sqrt (n * ((||.z.|| * (((sqrt n) " ) * r)) ^2 )) by DD8, RVSUM_1:114, SQUARE_1:95;
then |.Rz.| < (sqrt n) * (sqrt ((||.z.|| * (((sqrt n) " ) * r)) ^2 )) by DD9, SQUARE_1:97;
then |.Rz.| < (sqrt n) * |.(||.z.|| * (((sqrt n) " ) * r)).| by COMPLEX1:158;
then |.Rz.| < (sqrt n) * (||.z.|| * (((sqrt n) " ) * r)) by DD0, B1, GG4, ABSVALUE:def 1;
then |.Rz.| < ((sqrt n) * (((sqrt n) " ) * r)) * ||.z.|| ;
then |.Rz.| / ||.z.|| < (sqrt n) * (((sqrt n) " ) * r) by GG4, XREAL_1:85;
then (||.z.|| " ) * ||.(R /. z).|| < ((sqrt n) * ((sqrt n) " )) * r by REAL_NS1:1;
then (||.z.|| " ) * ||.(R /. z).|| < 1 * r by LP1, 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 DD3, PP1, PARTFUN1:def 8; :: thesis: verum

end;

then reconsider R = R as REST of (REAL-NS m),(REAL-NS n) by NDIFF_1:26;
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 AP2, NFCONT_1:3;

now

let x be set ; :: 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
T2: ( x = y & ||.(y - x0).|| < min d ) ;
1 <= n by NAT_1:14;
then T5: ( 1 in Seg n & 1 in dom d ) by A2;
then T3: { z where z is Point of (REAL-NS m) : ||.(z - x0).|| < d /. 1 } c= dom ((Proj 1,n) * g) by A2;
dom ((Proj 1,n) * g) c= dom g by RELAT_1:44;
then T4: { z where z is Point of (REAL-NS m) : ||.(z - x0).|| < d /. 1 } c= dom g by T3, XBOOLE_1:1;
len d = n by A2, 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 T5, PARTFUN1:def 8;
then ||.(y - x0).|| < d /. 1 by T2, 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 T2, T4; :: thesis: verum

end;

then T1: 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 REST 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 REST 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))
PP1: dom R = the carrier of (REAL-NS m) by PARTFUN1:def 4;
R . (x - x0) = ((g /. ((x - x0) + x0)) - (g /. x0)) - (L . (x - x0)) by A9;
then R . (x - x0) = ((g /. (x - (x0 - x0))) - (g /. x0)) - (L0 . (x - x0)) by RLVECT_1:43;
then R . (x - x0) = ((g /. (x - (x0 + (- x0)))) - (g /. x0)) - (L0 . (x - x0)) by RLVECT_1:def 14;
then R . (x - x0) = ((g /. (x - (0. (REAL-NS m)))) - (g /. x0)) - (L0 . (x - x0)) by RLVECT_1:16;
then R . (x - x0) = ((g /. x) - (g /. x0)) - (L0 . (x - x0)) by RLVECT_1:26;
then R . (x - x0) = ((g /. x) - (g /. x0)) + (- (L0 . (x - x0))) by RLVECT_1:def 14;
then R /. (x - x0) = ((g /. x) - (g /. x0)) + (- (L0 . (x - x0))) by PP1, PARTFUN1:def 8;
then (L0 . (x - x0)) + (R /. (x - x0)) = ((g /. x) - (g /. x0)) + ((- (L0 . (x - x0))) + (L0 . (x - x0))) by RLVECT_1:def 6;
then (L0 . (x - x0)) + (R /. (x - x0)) = ((g /. x) - (g /. x0)) + (0. (REAL-NS n)) by RLVECT_1:16;
hence (g /. x) - (g /. x0) = (L0 . (x - x0)) + (R /. (x - x0)) by RLVECT_1:10; :: thesis: verum

end;

end;

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

end;

hence ( 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 ) by DPREP120; :: thesis: verum