:: by Yasunari Shidama

::

:: Received June 2, 2011

:: Copyright (c) 2011-2018 Association of Mizar Users

theorem Th1: :: NDIFF_5:1

for S being RealNormSpace

for R being Function of REAL,S holds

( R is RestFunc-like iff 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 ) ) )

for R being Function of REAL,S holds

( R is RestFunc-like iff 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 end;

theorem Th2: :: NDIFF_5:2

for S being RealNormSpace

for R being RestFunc of S st R /. 0 = 0. S holds

for e being Real st e > 0 holds

ex d being Real st

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

||.(R /. h).|| <= e * |.h.| ) )

for R being RestFunc of S st R /. 0 = 0. S holds

for e being Real st e > 0 holds

ex d being Real st

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

||.(R /. h).|| <= e * |.h.| ) )

proof end;

theorem Th3: :: NDIFF_5:3

for S, T being RealNormSpace

for R being RestFunc of S

for L being Lipschitzian LinearOperator of S,T holds L * R is RestFunc of T

for R being RestFunc of S

for L being Lipschitzian LinearOperator of S,T holds L * R is RestFunc of T

proof end;

theorem Th4: :: NDIFF_5:4

for S, T being RealNormSpace

for R1 being RestFunc of S st R1 /. 0 = 0. S holds

for R2 being RestFunc of S,T st R2 /. (0. S) = 0. T holds

for L being LinearFunc of S holds R2 * (L + R1) is RestFunc of T

for R1 being RestFunc of S st R1 /. 0 = 0. S holds

for R2 being RestFunc of S,T st R2 /. (0. S) = 0. T holds

for L being LinearFunc of S holds R2 * (L + R1) is RestFunc of T

proof end;

theorem Th5: :: NDIFF_5:5

for S, T being RealNormSpace

for R1 being RestFunc of S st R1 /. 0 = 0. S holds

for R2 being RestFunc of S,T st R2 /. (0. S) = 0. T holds

for L1 being LinearFunc of S

for L2 being Lipschitzian LinearOperator of S,T holds (L2 * R1) + (R2 * (L1 + R1)) is RestFunc of T

for R1 being RestFunc of S st R1 /. 0 = 0. S holds

for R2 being RestFunc of S,T st R2 /. (0. S) = 0. T holds

for L1 being LinearFunc of S

for L2 being Lipschitzian LinearOperator of S,T holds (L2 * R1) + (R2 * (L1 + R1)) is RestFunc of T

proof end;

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

theorem Th6: :: NDIFF_5:6

for S, T being RealNormSpace

for x0 being Real

for g being PartFunc of REAL, the carrier of S st g is_differentiable_in x0 holds

for f being PartFunc of the carrier of S, the carrier of T st f is_differentiable_in g /. x0 holds

( f * g is_differentiable_in x0 & diff ((f * g),x0) = (diff (f,(g /. x0))) . (diff (g,x0)) )

for x0 being Real

for g being PartFunc of REAL, the carrier of S st g is_differentiable_in x0 holds

for f being PartFunc of the carrier of S, the carrier of T st f is_differentiable_in g /. x0 holds

( f * g is_differentiable_in x0 & diff ((f * g),x0) = (diff (f,(g /. x0))) . (diff (g,x0)) )

proof end;

theorem Th7: :: NDIFF_5:7

for S being RealNormSpace

for xseq being FinSequence of S

for yseq being FinSequence of REAL st len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds

yseq . i = ||.(xseq /. i).|| ) holds

||.(Sum xseq).|| <= Sum yseq

for xseq being FinSequence of S

for yseq being FinSequence of REAL st len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds

yseq . i = ||.(xseq /. i).|| ) holds

||.(Sum xseq).|| <= Sum yseq

proof end;

theorem Th8: :: NDIFF_5:8

for S being RealNormSpace

for x being Point of S

for N1, N2 being Neighbourhood of x holds N1 /\ N2 is Neighbourhood of x

for x being Point of S

for N1, N2 being Neighbourhood of x holds N1 /\ N2 is Neighbourhood of x

proof end;

registration
end;

Lm1: now :: thesis: for G being RealLinearSpace-Sequence holds dom (carr G) = dom G

let G be RealLinearSpace-Sequence; :: thesis: dom (carr G) = dom G

len (carr G) = len G by PRVECT_2:def 4;

hence dom (carr G) = Seg (len G) by FINSEQ_1:def 3

.= dom G by FINSEQ_1:def 3 ;

:: thesis: verum

end;
len (carr G) = len G by PRVECT_2:def 4;

hence dom (carr G) = Seg (len G) by FINSEQ_1:def 3

.= dom G by FINSEQ_1:def 3 ;

:: thesis: verum

definition

let G be RealLinearSpace-Sequence;

let z be Element of product (carr G);

let j be Element of dom G;

:: original: .

redefine func z . j -> Element of (G . j);

correctness

coherence

z . j is Element of (G . j);

end;
let z be Element of product (carr G);

let j be Element of dom G;

:: original: .

redefine func z . j -> Element of (G . j);

correctness

coherence

z . j is Element of (G . j);

proof end;

theorem Th11: :: NDIFF_5:11

for G being RealNormSpace-Sequence

for i being Element of dom G

for r being set

for x being Function st r in the carrier of (G . i) & x in product (carr G) holds

x +* (i,r) in the carrier of (product G)

for i being Element of dom G

for r being set

for x being Function st r in the carrier of (G . i) & x in product (carr G) holds

x +* (i,r) in the carrier of (product G)

proof end;

definition

let G be RealNormSpace-Sequence;

end;
attr G is non-trivial means :Def1: :: NDIFF_5:def 1

for j being Element of dom G holds not G . j is trivial ;

for j being Element of dom G holds not G . j is trivial ;

:: deftheorem Def1 defines non-trivial NDIFF_5:def 1 :

for G being RealNormSpace-Sequence holds

( G is non-trivial iff for j being Element of dom G holds not G . j is trivial );

for G being RealNormSpace-Sequence holds

( G is non-trivial iff for j being Element of dom G holds not G . j is trivial );

registration

existence

ex b_{1} being RealNormSpace-Sequence st b_{1} is non-trivial ;

end;

cluster Relation-like NAT -defined non empty Function-like V55() FinSequence-like FinSubsequence-like countable RealLinearSpace-yielding RealNormSpace-yielding non-trivial for RealNormSpace-Sequence;

correctness existence

ex b

proof end;

registration

let G be non-trivial RealNormSpace-Sequence;

let i be Element of dom G;

correctness

coherence

for b_{1} being RealNormSpace st b_{1} = G . i holds

not b_{1} is trivial ;

by Def1;

end;
let i be Element of dom G;

correctness

coherence

for b

not b

by Def1;

registration

let G be non-trivial RealNormSpace-Sequence;

correctness

coherence

not product G is trivial ;

end;
correctness

coherence

not product G is trivial ;

proof end;

theorem Th12: :: NDIFF_5:12

for G being RealNormSpace-Sequence

for p, q being Point of (product G)

for r0, p0, q0 being Element of product (carr G) st p = p0 & q = q0 holds

( p + q = r0 iff for i being Element of dom G holds r0 . i = (p0 . i) + (q0 . i) )

for p, q being Point of (product G)

for r0, p0, q0 being Element of product (carr G) st p = p0 & q = q0 holds

( p + q = r0 iff for i being Element of dom G holds r0 . i = (p0 . i) + (q0 . i) )

proof end;

theorem Th13: :: NDIFF_5:13

for G being RealNormSpace-Sequence

for p being Point of (product G)

for r being Real

for r0, p0 being Element of product (carr G) st p = p0 holds

( r * p = r0 iff for i being Element of dom G holds r0 . i = r * (p0 . i) )

for p being Point of (product G)

for r being Real

for r0, p0 being Element of product (carr G) st p = p0 holds

( r * p = r0 iff for i being Element of dom G holds r0 . i = r * (p0 . i) )

proof end;

theorem Th14: :: NDIFF_5:14

for G being RealNormSpace-Sequence

for p0 being Element of product (carr G) holds

( 0. (product G) = p0 iff for i being Element of dom G holds p0 . i = 0. (G . i) )

for p0 being Element of product (carr G) holds

( 0. (product G) = p0 iff for i being Element of dom G holds p0 . i = 0. (G . i) )

proof end;

theorem Th15: :: NDIFF_5:15

for G being RealNormSpace-Sequence

for p, q being Point of (product G)

for r0, p0, q0 being Element of product (carr G) st p = p0 & q = q0 holds

( p - q = r0 iff for i being Element of dom G holds r0 . i = (p0 . i) - (q0 . i) )

for p, q being Point of (product G)

for r0, p0, q0 being Element of product (carr G) st p = p0 & q = q0 holds

( p - q = r0 iff for i being Element of dom G holds r0 . i = (p0 . i) - (q0 . i) )

proof end;

Lm2: now :: thesis: for S being RealLinearSpace

for p, q being Point of S

for z1 being Real holds p + (z1 * (q - p)) = ((1 - z1) * p) + (z1 * q)

for p, q being Point of S

for z1 being Real holds p + (z1 * (q - p)) = ((1 - z1) * p) + (z1 * q)

let S be RealLinearSpace; :: thesis: for p, q being Point of S

for z1 being Real holds p + (z1 * (q - p)) = ((1 - z1) * p) + (z1 * q)

let p, q be Point of S; :: thesis: for z1 being Real holds p + (z1 * (q - p)) = ((1 - z1) * p) + (z1 * q)

let z1 be Real; :: thesis: p + (z1 * (q - p)) = ((1 - z1) * p) + (z1 * q)

thus p + (z1 * (q - p)) = p + ((z1 * q) + (z1 * (- p))) by RLVECT_1:def 5

.= p + ((z1 * q) + (- (z1 * p))) by RLVECT_1:25

.= (p + (- (z1 * p))) + (z1 * q) by RLVECT_1:def 3

.= ((1 * p) - (z1 * p)) + (z1 * q) by RLVECT_1:def 8

.= ((1 - z1) * p) + (z1 * q) by RLVECT_1:35 ; :: thesis: verum

end;
for z1 being Real holds p + (z1 * (q - p)) = ((1 - z1) * p) + (z1 * q)

let p, q be Point of S; :: thesis: for z1 being Real holds p + (z1 * (q - p)) = ((1 - z1) * p) + (z1 * q)

let z1 be Real; :: thesis: p + (z1 * (q - p)) = ((1 - z1) * p) + (z1 * q)

thus p + (z1 * (q - p)) = p + ((z1 * q) + (z1 * (- p))) by RLVECT_1:def 5

.= p + ((z1 * q) + (- (z1 * p))) by RLVECT_1:25

.= (p + (- (z1 * p))) + (z1 * q) by RLVECT_1:def 3

.= ((1 * p) - (z1 * p)) + (z1 * q) by RLVECT_1:def 8

.= ((1 - z1) * p) + (z1 * q) by RLVECT_1:35 ; :: thesis: verum

definition

let S be RealLinearSpace;

let p, q be Point of S;

correctness

coherence

[.p,q.] \ {p,q} is Subset of S;

;

end;
let p, q be Point of S;

correctness

coherence

[.p,q.] \ {p,q} is Subset of S;

;

:: deftheorem defines ]. NDIFF_5:def 2 :

for S being RealLinearSpace

for p, q being Point of S holds ].p,q.[ = [.p,q.] \ {p,q};

for S being RealLinearSpace

for p, q being Point of S holds ].p,q.[ = [.p,q.] \ {p,q};

theorem LMOPN: :: NDIFF_5:16

for S being RealLinearSpace

for p, q being Point of S st p <> q holds

].p,q.[ = { (p + (t * (q - p))) where t is Real : ( 0 < t & t < 1 ) }

for p, q being Point of S st p <> q holds

].p,q.[ = { (p + (t * (q - p))) where t is Real : ( 0 < t & t < 1 ) }

proof end;

Lm3: for x being Real st ( for e being Real st 0 < e holds

x <= e ) holds

x <= 0

proof end;

theorem Th17: :: NDIFF_5:17

for T being RealNormSpace

for R being PartFunc of REAL,T st R is total holds

( R is RestFunc-like iff 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

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

for R being PartFunc of REAL,T st R is total holds

( R is RestFunc-like iff 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

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

proof end;

theorem Th18: :: NDIFF_5:18

for R being Function of REAL,REAL holds

( R is RestFunc-like iff 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

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

( R is RestFunc-like iff 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

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

proof end;

reconsider jj = 1 as Real ;

Lm4: for T being RealNormSpace

for f being PartFunc of REAL,T

for g being PartFunc of REAL,REAL st dom f = [.0,1.] & dom g = [.0,1.] & f | [.0,1.] is continuous & g | [.0,1.] is continuous & f is_differentiable_on ].0,1.[ & g is_differentiable_on ].0,1.[ & ( for x being Real st x in ].0,1.[ holds

||.(diff (f,x)).|| <= diff (g,x) ) holds

||.((f /. 1) - (f /. 0)).|| <= (g /. 1) - (g /. 0)

proof end;

theorem Th19: :: NDIFF_5:19

for S, T being RealNormSpace

for f being PartFunc of S,T

for p, q being Point of S

for M being Real st [.p,q.] c= dom f & ( for x being Point of S st x in [.p,q.] holds

f is_continuous_in x ) & ( for x being Point of S st x in ].p,q.[ holds

f is_differentiable_in x ) & ( for x being Point of S st x in ].p,q.[ holds

||.(diff (f,x)).|| <= M ) holds

||.((f /. q) - (f /. p)).|| <= M * ||.(q - p).||

for f being PartFunc of S,T

for p, q being Point of S

for M being Real st [.p,q.] c= dom f & ( for x being Point of S st x in [.p,q.] holds

f is_continuous_in x ) & ( for x being Point of S st x in ].p,q.[ holds

f is_differentiable_in x ) & ( for x being Point of S st x in ].p,q.[ holds

||.(diff (f,x)).|| <= M ) holds

||.((f /. q) - (f /. p)).|| <= M * ||.(q - p).||

proof end;

theorem Th20: :: NDIFF_5:20

for S, T being RealNormSpace

for f being PartFunc of S,T

for p, q being Point of S

for M being Real

for L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) st [.p,q.] c= dom f & ( for x being Point of S st x in [.p,q.] holds

f is_continuous_in x ) & ( for x being Point of S st x in ].p,q.[ holds

f is_differentiable_in x ) & ( for x being Point of S st x in ].p,q.[ holds

||.((diff (f,x)) - L).|| <= M ) holds

||.(((f /. q) - (f /. p)) - (L . (q - p))).|| <= M * ||.(q - p).||

for f being PartFunc of S,T

for p, q being Point of S

for M being Real

for L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) st [.p,q.] c= dom f & ( for x being Point of S st x in [.p,q.] holds

f is_continuous_in x ) & ( for x being Point of S st x in ].p,q.[ holds

f is_differentiable_in x ) & ( for x being Point of S st x in ].p,q.[ holds

||.((diff (f,x)) - L).|| <= M ) holds

||.(((f /. q) - (f /. p)) - (L . (q - p))).|| <= M * ||.(q - p).||

proof end;

definition

let G be RealNormSpace-Sequence;

let i be Element of dom G;

ex b_{1} being Function of (product G),(G . i) st

for x being Element of product (carr G) holds b_{1} . x = x . i

for b_{1}, b_{2} being Function of (product G),(G . i) st ( for x being Element of product (carr G) holds b_{1} . x = x . i ) & ( for x being Element of product (carr G) holds b_{2} . x = x . i ) holds

b_{1} = b_{2}

end;
let i be Element of dom G;

func proj i -> Function of (product G),(G . i) means :Def3: :: NDIFF_5:def 3

for x being Element of product (carr G) holds it . x = x . i;

existence for x being Element of product (carr G) holds it . x = x . i;

ex b

for x being Element of product (carr G) holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def3 defines proj NDIFF_5:def 3 :

for G being RealNormSpace-Sequence

for i being Element of dom G

for b_{3} being Function of (product G),(G . i) holds

( b_{3} = proj i iff for x being Element of product (carr G) holds b_{3} . x = x . i );

for G being RealNormSpace-Sequence

for i being Element of dom G

for b

( b

definition

let G be RealNormSpace-Sequence;

let i be Element of dom G;

let x be Element of (product G);

ex b_{1} being Function of (G . i),(product G) st

for r being Element of (G . i) holds b_{1} . r = x +* (i,r)

for b_{1}, b_{2} being Function of (G . i),(product G) st ( for r being Element of (G . i) holds b_{1} . r = x +* (i,r) ) & ( for r being Element of (G . i) holds b_{2} . r = x +* (i,r) ) holds

b_{1} = b_{2}

end;
let i be Element of dom G;

let x be Element of (product G);

func reproj (i,x) -> Function of (G . i),(product G) means :Def4: :: NDIFF_5:def 4

for r being Element of (G . i) holds it . r = x +* (i,r);

existence for r being Element of (G . i) holds it . r = x +* (i,r);

ex b

for r being Element of (G . i) holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def4 defines reproj NDIFF_5:def 4 :

for G being RealNormSpace-Sequence

for i being Element of dom G

for x being Element of (product G)

for b_{4} being Function of (G . i),(product G) holds

( b_{4} = reproj (i,x) iff for r being Element of (G . i) holds b_{4} . r = x +* (i,r) );

for G being RealNormSpace-Sequence

for i being Element of dom G

for x being Element of (product G)

for b

( b

definition

let G be RealNormSpace-Sequence;

let F be RealNormSpace;

let i be set ;

let f be PartFunc of (product G),F;

let x be Element of (product G);

end;
let F be RealNormSpace;

let i be set ;

let f be PartFunc of (product G),F;

let x be Element of (product G);

pred f is_partial_differentiable_in x,i means :: NDIFF_5:def 6

f * (reproj ((In (i,(dom G))),x)) is_differentiable_in (proj (In (i,(dom G)))) . x;

f * (reproj ((In (i,(dom G))),x)) is_differentiable_in (proj (In (i,(dom G)))) . x;

:: deftheorem defines is_partial_differentiable_in NDIFF_5:def 6 :

for G being RealNormSpace-Sequence

for F being RealNormSpace

for i being set

for f being PartFunc of (product G),F

for x being Element of (product G) holds

( f is_partial_differentiable_in x,i iff f * (reproj ((In (i,(dom G))),x)) is_differentiable_in (proj (In (i,(dom G)))) . x );

for G being RealNormSpace-Sequence

for F being RealNormSpace

for i being set

for f being PartFunc of (product G),F

for x being Element of (product G) holds

( f is_partial_differentiable_in x,i iff f * (reproj ((In (i,(dom G))),x)) is_differentiable_in (proj (In (i,(dom G)))) . x );

definition

let G be RealNormSpace-Sequence;

let F be RealNormSpace;

let i be set ;

let f be PartFunc of (product G),F;

let x be Point of (product G);

diff ((f * (reproj ((In (i,(dom G))),x))),((proj (In (i,(dom G)))) . x)) is Point of (R_NormSpace_of_BoundedLinearOperators ((G . (In (i,(dom G)))),F)) ;

end;
let F be RealNormSpace;

let i be set ;

let f be PartFunc of (product G),F;

let x be Point of (product G);

func partdiff (f,x,i) -> Point of (R_NormSpace_of_BoundedLinearOperators ((G . (In (i,(dom G)))),F)) equals :: NDIFF_5:def 7

diff ((f * (reproj ((In (i,(dom G))),x))),((proj (In (i,(dom G)))) . x));

coherence diff ((f * (reproj ((In (i,(dom G))),x))),((proj (In (i,(dom G)))) . x));

diff ((f * (reproj ((In (i,(dom G))),x))),((proj (In (i,(dom G)))) . x)) is Point of (R_NormSpace_of_BoundedLinearOperators ((G . (In (i,(dom G)))),F)) ;

:: deftheorem defines partdiff NDIFF_5:def 7 :

for G being RealNormSpace-Sequence

for F being RealNormSpace

for i being set

for f being PartFunc of (product G),F

for x being Point of (product G) holds partdiff (f,x,i) = diff ((f * (reproj ((In (i,(dom G))),x))),((proj (In (i,(dom G)))) . x));

for G being RealNormSpace-Sequence

for F being RealNormSpace

for i being set

for f being PartFunc of (product G),F

for x being Point of (product G) holds partdiff (f,x,i) = diff ((f * (reproj ((In (i,(dom G))),x))),((proj (In (i,(dom G)))) . x));

definition

let G be RealNormSpace-Sequence;

let F be RealNormSpace;

let i be set ;

let f be PartFunc of (product G),F;

let X be set ;

end;
let F be RealNormSpace;

let i be set ;

let f be PartFunc of (product G),F;

let X be set ;

pred f is_partial_differentiable_on X,i means :: NDIFF_5:def 8

( X c= dom f & ( for x being Point of (product G) st x in X holds

f | X is_partial_differentiable_in x,i ) );

( X c= dom f & ( for x being Point of (product G) st x in X holds

f | X is_partial_differentiable_in x,i ) );

:: deftheorem defines is_partial_differentiable_on NDIFF_5:def 8 :

for G being RealNormSpace-Sequence

for F being RealNormSpace

for i being set

for f being PartFunc of (product G),F

for X being set holds

( f is_partial_differentiable_on X,i iff ( X c= dom f & ( for x being Point of (product G) st x in X holds

f | X is_partial_differentiable_in x,i ) ) );

for G being RealNormSpace-Sequence

for F being RealNormSpace

for i being set

for f being PartFunc of (product G),F

for X being set holds

( f is_partial_differentiable_on X,i iff ( X c= dom f & ( for x being Point of (product G) st x in X holds

f | X is_partial_differentiable_in x,i ) ) );

theorem Th21: :: NDIFF_5:21

for G being RealNormSpace-Sequence

for i being Element of dom G

for xi being Element of (G . i) holds ||.((reproj (i,(0. (product G)))) . xi).|| = ||.xi.||

for i being Element of dom G

for xi being Element of (G . i) holds ||.((reproj (i,(0. (product G)))) . xi).|| = ||.xi.||

proof end;

theorem Th22: :: NDIFF_5:22

for G being RealNormSpace-Sequence

for i being Element of dom G

for x being Point of (product G)

for r being Point of (G . i) holds

( ((reproj (i,x)) . r) - x = (reproj (i,(0. (product G)))) . (r - ((proj i) . x)) & x - ((reproj (i,x)) . r) = (reproj (i,(0. (product G)))) . (((proj i) . x) - r) )

for i being Element of dom G

for x being Point of (product G)

for r being Point of (G . i) holds

( ((reproj (i,x)) . r) - x = (reproj (i,(0. (product G)))) . (r - ((proj i) . x)) & x - ((reproj (i,x)) . r) = (reproj (i,(0. (product G)))) . (((proj i) . x) - r) )

proof end;

theorem Th23: :: NDIFF_5:23

for G being RealNormSpace-Sequence

for i being Element of dom G

for x being Point of (product G)

for Z being Subset of (product G) st Z is open & x in Z holds

ex N being Neighbourhood of (proj i) . x st

for z being Point of (G . i) st z in N holds

(reproj (i,x)) . z in Z

for i being Element of dom G

for x being Point of (product G)

for Z being Subset of (product G) st Z is open & x in Z holds

ex N being Neighbourhood of (proj i) . x st

for z being Point of (G . i) st z in N holds

(reproj (i,x)) . z in Z

proof end;

theorem Th24: :: NDIFF_5:24

for G being RealNormSpace-Sequence

for T being RealNormSpace

for i being set

for f being PartFunc of (product G),T

for Z being Subset of (product G) st Z is open holds

( f is_partial_differentiable_on Z,i iff ( Z c= dom f & ( for x being Point of (product G) st x in Z holds

f is_partial_differentiable_in x,i ) ) )

for T being RealNormSpace

for i being set

for f being PartFunc of (product G),T

for Z being Subset of (product G) st Z is open holds

( f is_partial_differentiable_on Z,i iff ( Z c= dom f & ( for x being Point of (product G) st x in Z holds

f is_partial_differentiable_in x,i ) ) )

proof end;

theorem :: NDIFF_5:25

for G being RealNormSpace-Sequence

for F being RealNormSpace

for f being PartFunc of (product G),F

for X, i being set st i in dom G & f is_partial_differentiable_on X,i holds

X is Subset of (product G) by XBOOLE_1:1;

for F being RealNormSpace

for f being PartFunc of (product G),F

for X, i being set st i in dom G & f is_partial_differentiable_on X,i holds

X is Subset of (product G) by XBOOLE_1:1;

definition

let G be RealNormSpace-Sequence;

let S be RealNormSpace;

let i be set ;

let f be PartFunc of (product G),S;

let X be set ;

assume A2: f is_partial_differentiable_on X,i ;

ex b_{1} being PartFunc of (product G),(R_NormSpace_of_BoundedLinearOperators ((G . (In (i,(dom G)))),S)) st

( dom b_{1} = X & ( for x being Point of (product G) st x in X holds

b_{1} /. x = partdiff (f,x,i) ) )

for b_{1}, b_{2} being PartFunc of (product G),(R_NormSpace_of_BoundedLinearOperators ((G . (In (i,(dom G)))),S)) st dom b_{1} = X & ( for x being Point of (product G) st x in X holds

b_{1} /. x = partdiff (f,x,i) ) & dom b_{2} = X & ( for x being Point of (product G) st x in X holds

b_{2} /. x = partdiff (f,x,i) ) holds

b_{1} = b_{2}

end;
let S be RealNormSpace;

let i be set ;

let f be PartFunc of (product G),S;

let X be set ;

assume A2: f is_partial_differentiable_on X,i ;

func f `partial| (X,i) -> PartFunc of (product G),(R_NormSpace_of_BoundedLinearOperators ((G . (In (i,(dom G)))),S)) means :Def9: :: NDIFF_5:def 9

( dom it = X & ( for x being Point of (product G) st x in X holds

it /. x = partdiff (f,x,i) ) );

existence ( dom it = X & ( for x being Point of (product G) st x in X holds

it /. x = partdiff (f,x,i) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def9 defines `partial| NDIFF_5:def 9 :

for G being RealNormSpace-Sequence

for S being RealNormSpace

for i being set

for f being PartFunc of (product G),S

for X being set st f is_partial_differentiable_on X,i holds

for b_{6} being PartFunc of (product G),(R_NormSpace_of_BoundedLinearOperators ((G . (In (i,(dom G)))),S)) holds

( b_{6} = f `partial| (X,i) iff ( dom b_{6} = X & ( for x being Point of (product G) st x in X holds

b_{6} /. x = partdiff (f,x,i) ) ) );

for G being RealNormSpace-Sequence

for S being RealNormSpace

for i being set

for f being PartFunc of (product G),S

for X being set st f is_partial_differentiable_on X,i holds

for b

( b

b

theorem Th26: :: NDIFF_5:26

for G being RealNormSpace-Sequence

for F being RealNormSpace

for f1, f2 being PartFunc of (product G),F

for x being Point of (product G)

for i being set st i in dom G holds

( (f1 + f2) * (reproj ((In (i,(dom G))),x)) = (f1 * (reproj ((In (i,(dom G))),x))) + (f2 * (reproj ((In (i,(dom G))),x))) & (f1 - f2) * (reproj ((In (i,(dom G))),x)) = (f1 * (reproj ((In (i,(dom G))),x))) - (f2 * (reproj ((In (i,(dom G))),x))) )

for F being RealNormSpace

for f1, f2 being PartFunc of (product G),F

for x being Point of (product G)

for i being set st i in dom G holds

( (f1 + f2) * (reproj ((In (i,(dom G))),x)) = (f1 * (reproj ((In (i,(dom G))),x))) + (f2 * (reproj ((In (i,(dom G))),x))) & (f1 - f2) * (reproj ((In (i,(dom G))),x)) = (f1 * (reproj ((In (i,(dom G))),x))) - (f2 * (reproj ((In (i,(dom G))),x))) )

proof end;

theorem Th27: :: NDIFF_5:27

for r being Real

for G being RealNormSpace-Sequence

for F being RealNormSpace

for f being PartFunc of (product G),F

for x being Point of (product G)

for i being set st i in dom G holds

r (#) (f * (reproj ((In (i,(dom G))),x))) = (r (#) f) * (reproj ((In (i,(dom G))),x))

for G being RealNormSpace-Sequence

for F being RealNormSpace

for f being PartFunc of (product G),F

for x being Point of (product G)

for i being set st i in dom G holds

r (#) (f * (reproj ((In (i,(dom G))),x))) = (r (#) f) * (reproj ((In (i,(dom G))),x))

proof end;

theorem :: NDIFF_5:28

for G being RealNormSpace-Sequence

for F being RealNormSpace

for f1, f2 being PartFunc of (product G),F

for x being Point of (product G)

for i being set st i in dom G & f1 is_partial_differentiable_in x,i & f2 is_partial_differentiable_in x,i holds

( f1 + f2 is_partial_differentiable_in x,i & partdiff ((f1 + f2),x,i) = (partdiff (f1,x,i)) + (partdiff (f2,x,i)) )

for F being RealNormSpace

for f1, f2 being PartFunc of (product G),F

for x being Point of (product G)

for i being set st i in dom G & f1 is_partial_differentiable_in x,i & f2 is_partial_differentiable_in x,i holds

( f1 + f2 is_partial_differentiable_in x,i & partdiff ((f1 + f2),x,i) = (partdiff (f1,x,i)) + (partdiff (f2,x,i)) )

proof end;

theorem :: NDIFF_5:29

for G being RealNormSpace-Sequence

for F being RealNormSpace

for f1, f2 being PartFunc of (product G),F

for x being Point of (product G)

for i being set st i in dom G & f1 is_partial_differentiable_in x,i & f2 is_partial_differentiable_in x,i holds

( f1 - f2 is_partial_differentiable_in x,i & partdiff ((f1 - f2),x,i) = (partdiff (f1,x,i)) - (partdiff (f2,x,i)) )

for F being RealNormSpace

for f1, f2 being PartFunc of (product G),F

for x being Point of (product G)

for i being set st i in dom G & f1 is_partial_differentiable_in x,i & f2 is_partial_differentiable_in x,i holds

( f1 - f2 is_partial_differentiable_in x,i & partdiff ((f1 - f2),x,i) = (partdiff (f1,x,i)) - (partdiff (f2,x,i)) )

proof end;

theorem :: NDIFF_5:30

for r being Real

for G being RealNormSpace-Sequence

for F being RealNormSpace

for f being PartFunc of (product G),F

for x being Point of (product G)

for i being set st i in dom G & f is_partial_differentiable_in x,i holds

( r (#) f is_partial_differentiable_in x,i & partdiff ((r (#) f),x,i) = r * (partdiff (f,x,i)) )

for G being RealNormSpace-Sequence

for F being RealNormSpace

for f being PartFunc of (product G),F

for x being Point of (product G)

for i being set st i in dom G & f is_partial_differentiable_in x,i holds

( r (#) f is_partial_differentiable_in x,i & partdiff ((r (#) f),x,i) = r * (partdiff (f,x,i)) )

proof end;

theorem Th31: :: NDIFF_5:31

for G being RealNormSpace-Sequence

for i being Element of dom G

for x being Point of (product G) holds ||.((proj i) . x).|| <= ||.x.||

for i being Element of dom G

for x being Point of (product G) holds ||.((proj i) . x).|| <= ||.x.||

proof end;

registration

let G be RealNormSpace-Sequence;

coherence

for b_{1} being Point of (product G) holds b_{1} is len G -element

end;
coherence

for b

proof end;

theorem Th32: :: NDIFF_5:32

for G being RealNormSpace-Sequence

for T being RealNormSpace

for i being set

for Z being Subset of (product G)

for f being PartFunc of (product G),T st Z is open holds

( f is_partial_differentiable_on Z,i iff ( Z c= dom f & ( for x being Point of (product G) st x in Z holds

f is_partial_differentiable_in x,i ) ) )

for T being RealNormSpace

for i being set

for Z being Subset of (product G)

for f being PartFunc of (product G),T st Z is open holds

( f is_partial_differentiable_on Z,i iff ( Z c= dom f & ( for x being Point of (product G) st x in Z holds

f is_partial_differentiable_in x,i ) ) )

proof end;

theorem Th33: :: NDIFF_5:33

for G being RealNormSpace-Sequence

for i, j being Element of dom G

for x being Point of (G . i)

for z being Element of product (carr G) st z = (reproj (i,(0. (product G)))) . x holds

( ( i = j implies z . j = x ) & ( i <> j implies z . j = 0. (G . j) ) )

for i, j being Element of dom G

for x being Point of (G . i)

for z being Element of product (carr G) st z = (reproj (i,(0. (product G)))) . x holds

( ( i = j implies z . j = x ) & ( i <> j implies z . j = 0. (G . j) ) )

proof end;

theorem Th34: :: NDIFF_5:34

for G being RealNormSpace-Sequence

for i being Element of dom G

for x, y being Point of (G . i) holds (reproj (i,(0. (product G)))) . (x + y) = ((reproj (i,(0. (product G)))) . x) + ((reproj (i,(0. (product G)))) . y)

for i being Element of dom G

for x, y being Point of (G . i) holds (reproj (i,(0. (product G)))) . (x + y) = ((reproj (i,(0. (product G)))) . x) + ((reproj (i,(0. (product G)))) . y)

proof end;

theorem Th35: :: NDIFF_5:35

for G being RealNormSpace-Sequence

for i being Element of dom G

for x, y being Point of (product G) holds (proj i) . (x + y) = ((proj i) . x) + ((proj i) . y)

for i being Element of dom G

for x, y being Point of (product G) holds (proj i) . (x + y) = ((proj i) . x) + ((proj i) . y)

proof end;

theorem :: NDIFF_5:36

for G being RealNormSpace-Sequence

for i being Element of dom G

for x, y being Point of (G . i) holds (reproj (i,(0. (product G)))) . (x - y) = ((reproj (i,(0. (product G)))) . x) - ((reproj (i,(0. (product G)))) . y)

for i being Element of dom G

for x, y being Point of (G . i) holds (reproj (i,(0. (product G)))) . (x - y) = ((reproj (i,(0. (product G)))) . x) - ((reproj (i,(0. (product G)))) . y)

proof end;

theorem Th37: :: NDIFF_5:37

for G being RealNormSpace-Sequence

for i being Element of dom G

for x, y being Point of (product G) holds (proj i) . (x - y) = ((proj i) . x) - ((proj i) . y)

for i being Element of dom G

for x, y being Point of (product G) holds (proj i) . (x - y) = ((proj i) . x) - ((proj i) . y)

proof end;

theorem Th38: :: NDIFF_5:38

for G being RealNormSpace-Sequence

for i being Element of dom G

for x being Point of (G . i) st x <> 0. (G . i) holds

(reproj (i,(0. (product G)))) . x <> 0. (product G)

for i being Element of dom G

for x being Point of (G . i) st x <> 0. (G . i) holds

(reproj (i,(0. (product G)))) . x <> 0. (product G)

proof end;

theorem Th39: :: NDIFF_5:39

for G being RealNormSpace-Sequence

for i being Element of dom G

for x being Point of (G . i)

for a being Real holds (reproj (i,(0. (product G)))) . (a * x) = a * ((reproj (i,(0. (product G)))) . x)

for i being Element of dom G

for x being Point of (G . i)

for a being Real holds (reproj (i,(0. (product G)))) . (a * x) = a * ((reproj (i,(0. (product G)))) . x)

proof end;

theorem Th40: :: NDIFF_5:40

for G being RealNormSpace-Sequence

for i being Element of dom G

for x being Point of (product G)

for a being Real holds (proj i) . (a * x) = a * ((proj i) . x)

for i being Element of dom G

for x being Point of (product G)

for a being Real holds (proj i) . (a * x) = a * ((proj i) . x)

proof end;

theorem Th41: :: NDIFF_5:41

for G being RealNormSpace-Sequence

for S being RealNormSpace

for f being PartFunc of (product G),S

for x being Point of (product G)

for i being set st f is_differentiable_in x holds

( f is_partial_differentiable_in x,i & partdiff (f,x,i) = (diff (f,x)) * (reproj ((In (i,(dom G))),(0. (product G)))) )

for S being RealNormSpace

for f being PartFunc of (product G),S

for x being Point of (product G)

for i being set st f is_differentiable_in x holds

( f is_partial_differentiable_in x,i & partdiff (f,x,i) = (diff (f,x)) * (reproj ((In (i,(dom G))),(0. (product G)))) )

proof end;

Lm5: for G being RealNormSpace-Sequence

for S being RealNormSpace

for f being PartFunc of (product G),S

for x being Point of (product G) ex L being Lipschitzian LinearOperator of (product G),S st

for h being Element of (product G) ex w being FinSequence of S st

( dom w = Seg (len G) & ( for i being Element of NAT st i in Seg (len G) holds

w . i = (partdiff (f,x,i)) . ((proj (In (i,(dom G)))) . h) ) & L . h = Sum w )

proof end;

theorem Th42: :: NDIFF_5:42

for S being RealNormSpace

for h, g being FinSequence of S st len h = (len g) + 1 & ( for i being Nat st i in dom g holds

g /. i = (h /. i) - (h /. (i + 1)) ) holds

(h /. 1) - (h /. (len h)) = Sum g

for h, g being FinSequence of S st len h = (len g) + 1 & ( for i being Nat st i in dom g holds

g /. i = (h /. i) - (h /. (i + 1)) ) holds

(h /. 1) - (h /. (len h)) = Sum g

proof end;

theorem :: NDIFF_5:43

theorem Th44: :: NDIFF_5:44

for G being RealNormSpace-Sequence

for x, y being Point of (product G)

for Z, x0 being Element of product (carr G)

for X being set st Z = 0. (product G) & x0 = x & y = Z +* (x0 | X) holds

||.y.|| <= ||.x.||

for x, y being Point of (product G)

for Z, x0 being Element of product (carr G)

for X being set st Z = 0. (product G) & x0 = x & y = Z +* (x0 | X) holds

||.y.|| <= ||.x.||

proof end;

theorem Th45: :: NDIFF_5:45

for G being RealNormSpace-Sequence

for S being RealNormSpace

for f being PartFunc of (product G),S

for x, y being Point of (product G) ex h being FinSequence of (product G) ex g being FinSequence of S ex Z, y0 being Element of product (carr G) st

( y0 = y & Z = 0. (product G) & len h = (len G) + 1 & len g = len G & ( for i being Nat st i in dom h holds

h /. i = Z +* (y0 | (Seg (((len G) + 1) -' i))) ) & ( for i being Nat st i in dom g holds

g /. i = (f /. (x + (h /. i))) - (f /. (x + (h /. (i + 1)))) ) & ( for i being Nat

for hi being Point of (product G) st i in dom h & h /. i = hi holds

||.hi.|| <= ||.y.|| ) & (f /. (x + y)) - (f /. x) = Sum g )

for S being RealNormSpace

for f being PartFunc of (product G),S

for x, y being Point of (product G) ex h being FinSequence of (product G) ex g being FinSequence of S ex Z, y0 being Element of product (carr G) st

( y0 = y & Z = 0. (product G) & len h = (len G) + 1 & len g = len G & ( for i being Nat st i in dom h holds

h /. i = Z +* (y0 | (Seg (((len G) + 1) -' i))) ) & ( for i being Nat st i in dom g holds

g /. i = (f /. (x + (h /. i))) - (f /. (x + (h /. (i + 1)))) ) & ( for i being Nat

for hi being Point of (product G) st i in dom h & h /. i = hi holds

||.hi.|| <= ||.y.|| ) & (f /. (x + y)) - (f /. x) = Sum g )

proof end;

theorem Th46: :: NDIFF_5:46

for G being RealNormSpace-Sequence

for i being Element of dom G

for x, y being Point of (product G)

for xi being Point of (G . i) st y = (reproj (i,x)) . xi holds

(proj i) . y = xi

for i being Element of dom G

for x, y being Point of (product G)

for xi being Point of (G . i) st y = (reproj (i,x)) . xi holds

(proj i) . y = xi

proof end;

theorem Th47: :: NDIFF_5:47

for G being RealNormSpace-Sequence

for i being Element of dom G

for y being Point of (product G)

for q being Point of (G . i) st q = (proj i) . y holds

y = (reproj (i,y)) . q

for i being Element of dom G

for y being Point of (product G)

for q being Point of (G . i) st q = (proj i) . y holds

y = (reproj (i,y)) . q

proof end;

theorem Th48: :: NDIFF_5:48

for G being RealNormSpace-Sequence

for i being Element of dom G

for x, y being Point of (product G)

for xi being Point of (G . i) st y = (reproj (i,x)) . xi holds

reproj (i,x) = reproj (i,y)

for i being Element of dom G

for x, y being Point of (product G)

for xi being Point of (G . i) st y = (reproj (i,x)) . xi holds

reproj (i,x) = reproj (i,y)

proof end;

theorem Th49: :: NDIFF_5:49

for G being RealNormSpace-Sequence

for i, j being Element of dom G

for x, y being Point of (product G)

for xi being Point of (G . i) st y = (reproj (i,x)) . xi & i <> j holds

(proj j) . x = (proj j) . y

for i, j being Element of dom G

for x, y being Point of (product G)

for xi being Point of (G . i) st y = (reproj (i,x)) . xi & i <> j holds

(proj j) . x = (proj j) . y

proof end;

theorem :: NDIFF_5:50

for G being RealNormSpace-Sequence

for F being RealNormSpace

for i being Element of dom G

for x being Point of (product G)

for xi being Point of (G . i)

for f being PartFunc of (product G),F

for g being PartFunc of (G . i),F st (proj i) . x = xi & g = f * (reproj (i,x)) holds

diff (g,xi) = partdiff (f,x,i)

for F being RealNormSpace

for i being Element of dom G

for x being Point of (product G)

for xi being Point of (G . i)

for f being PartFunc of (product G),F

for g being PartFunc of (G . i),F st (proj i) . x = xi & g = f * (reproj (i,x)) holds

diff (g,xi) = partdiff (f,x,i)

proof end;

theorem Th51: :: NDIFF_5:51

for G being RealNormSpace-Sequence

for F being RealNormSpace

for f being PartFunc of (product G),F

for x being Point of (product G)

for i being set

for M being Real

for L being Point of (R_NormSpace_of_BoundedLinearOperators ((G . (In (i,(dom G)))),F))

for p, q being Point of (G . (In (i,(dom G)))) st i in dom G & ( for h being Point of (G . (In (i,(dom G)))) st h in ].p,q.[ holds

||.((partdiff (f,((reproj ((In (i,(dom G))),x)) . h),i)) - L).|| <= M ) & ( for h being Point of (G . (In (i,(dom G)))) st h in [.p,q.] holds

(reproj ((In (i,(dom G))),x)) . h in dom f ) & ( for h being Point of (G . (In (i,(dom G)))) st h in [.p,q.] holds

f is_partial_differentiable_in (reproj ((In (i,(dom G))),x)) . h,i ) holds

||.(((f /. ((reproj ((In (i,(dom G))),x)) . q)) - (f /. ((reproj ((In (i,(dom G))),x)) . p))) - (L . (q - p))).|| <= M * ||.(q - p).||

for F being RealNormSpace

for f being PartFunc of (product G),F

for x being Point of (product G)

for i being set

for M being Real

for L being Point of (R_NormSpace_of_BoundedLinearOperators ((G . (In (i,(dom G)))),F))

for p, q being Point of (G . (In (i,(dom G)))) st i in dom G & ( for h being Point of (G . (In (i,(dom G)))) st h in ].p,q.[ holds

||.((partdiff (f,((reproj ((In (i,(dom G))),x)) . h),i)) - L).|| <= M ) & ( for h being Point of (G . (In (i,(dom G)))) st h in [.p,q.] holds

(reproj ((In (i,(dom G))),x)) . h in dom f ) & ( for h being Point of (G . (In (i,(dom G)))) st h in [.p,q.] holds

f is_partial_differentiable_in (reproj ((In (i,(dom G))),x)) . h,i ) holds

||.(((f /. ((reproj ((In (i,(dom G))),x)) . q)) - (f /. ((reproj ((In (i,(dom G))),x)) . p))) - (L . (q - p))).|| <= M * ||.(q - p).||

proof end;

theorem Th52: :: NDIFF_5:52

for G being RealNormSpace-Sequence

for x, y, z, w being Point of (product G)

for i being Element of dom G

for d being Real

for p, q, r being Point of (G . i) st ||.(y - x).|| < d & ||.(z - x).|| < d & p = (proj i) . y & z = (reproj (i,y)) . q & r in [.p,q.] & w = (reproj (i,y)) . r holds

||.(w - x).|| < d

for x, y, z, w being Point of (product G)

for i being Element of dom G

for d being Real

for p, q, r being Point of (G . i) st ||.(y - x).|| < d & ||.(z - x).|| < d & p = (proj i) . y & z = (reproj (i,y)) . q & r in [.p,q.] & w = (reproj (i,y)) . r holds

||.(w - x).|| < d

proof end;

theorem Th53: :: NDIFF_5:53

for G being RealNormSpace-Sequence

for S being RealNormSpace

for f being PartFunc of (product G),S

for X being Subset of (product G)

for x, y, z being Point of (product G)

for i being set

for p, q being Point of (G . (In (i,(dom G))))

for d, r being Real st i in dom G & X is open & x in X & ||.(y - x).|| < d & ||.(z - x).|| < d & X c= dom f & ( for x being Point of (product G) st x in X holds

f is_partial_differentiable_in x,i ) & ( for z being Point of (product G) st ||.(z - x).|| < d holds

z in X ) & ( for z being Point of (product G) st ||.(z - x).|| < d holds

||.((partdiff (f,z,i)) - (partdiff (f,x,i))).|| <= r ) & z = (reproj ((In (i,(dom G))),y)) . p & q = (proj (In (i,(dom G)))) . y holds

||.(((f /. z) - (f /. y)) - ((partdiff (f,x,i)) . (p - q))).|| <= ||.(p - q).|| * r

for S being RealNormSpace

for f being PartFunc of (product G),S

for X being Subset of (product G)

for x, y, z being Point of (product G)

for i being set

for p, q being Point of (G . (In (i,(dom G))))

for d, r being Real st i in dom G & X is open & x in X & ||.(y - x).|| < d & ||.(z - x).|| < d & X c= dom f & ( for x being Point of (product G) st x in X holds

f is_partial_differentiable_in x,i ) & ( for z being Point of (product G) st ||.(z - x).|| < d holds

z in X ) & ( for z being Point of (product G) st ||.(z - x).|| < d holds

||.((partdiff (f,z,i)) - (partdiff (f,x,i))).|| <= r ) & z = (reproj ((In (i,(dom G))),y)) . p & q = (proj (In (i,(dom G)))) . y holds

||.(((f /. z) - (f /. y)) - ((partdiff (f,x,i)) . (p - q))).|| <= ||.(p - q).|| * r

proof end;

theorem Th54: :: NDIFF_5:54

for G being RealNormSpace-Sequence

for h being FinSequence of (product G)

for y, x being Point of (product G)

for y0, Z being Element of product (carr G)

for j being Element of NAT st y = y0 & Z = 0. (product G) & len h = (len G) + 1 & 1 <= j & j <= len G & ( for i being Nat st i in dom h holds

h /. i = Z +* (y0 | (Seg (((len G) + 1) -' i))) ) holds

x + (h /. j) = (reproj ((In ((((len G) + 1) -' j),(dom G))),(x + (h /. (j + 1))))) . ((proj (In ((((len G) + 1) -' j),(dom G)))) . (x + y))

for h being FinSequence of (product G)

for y, x being Point of (product G)

for y0, Z being Element of product (carr G)

for j being Element of NAT st y = y0 & Z = 0. (product G) & len h = (len G) + 1 & 1 <= j & j <= len G & ( for i being Nat st i in dom h holds

h /. i = Z +* (y0 | (Seg (((len G) + 1) -' i))) ) holds

x + (h /. j) = (reproj ((In ((((len G) + 1) -' j),(dom G))),(x + (h /. (j + 1))))) . ((proj (In ((((len G) + 1) -' j),(dom G)))) . (x + y))

proof end;

theorem Th55: :: NDIFF_5:55

for G being RealNormSpace-Sequence

for h being FinSequence of (product G)

for y, x being Point of (product G)

for y0, Z being Element of product (carr G)

for j being Element of NAT st y = y0 & Z = 0. (product G) & len h = (len G) + 1 & 1 <= j & j <= len G & ( for i being Nat st i in dom h holds

h /. i = Z +* (y0 | (Seg (((len G) + 1) -' i))) ) holds

((proj (In ((((len G) + 1) -' j),(dom G)))) . (x + y)) - ((proj (In ((((len G) + 1) -' j),(dom G)))) . (x + (h /. (j + 1)))) = (proj (In ((((len G) + 1) -' j),(dom G)))) . y

for h being FinSequence of (product G)

for y, x being Point of (product G)

for y0, Z being Element of product (carr G)

for j being Element of NAT st y = y0 & Z = 0. (product G) & len h = (len G) + 1 & 1 <= j & j <= len G & ( for i being Nat st i in dom h holds

h /. i = Z +* (y0 | (Seg (((len G) + 1) -' i))) ) holds

((proj (In ((((len G) + 1) -' j),(dom G)))) . (x + y)) - ((proj (In ((((len G) + 1) -' j),(dom G)))) . (x + (h /. (j + 1)))) = (proj (In ((((len G) + 1) -' j),(dom G)))) . y

proof end;

theorem Th56: :: NDIFF_5:56

for G being RealNormSpace-Sequence

for S being RealNormSpace

for f being PartFunc of (product G),S

for X being Subset of (product G)

for x being Point of (product G) st X is open & x in X & ( for i being set st i in dom G holds

( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) ) holds

( f is_differentiable_in x & ( for h being Point of (product G) ex w being FinSequence of S st

( dom w = dom G & ( for i being set st i in dom G holds

w . i = (partdiff (f,x,i)) . ((proj (In (i,(dom G)))) . h) ) & (diff (f,x)) . h = Sum w ) ) )

for S being RealNormSpace

for f being PartFunc of (product G),S

for X being Subset of (product G)

for x being Point of (product G) st X is open & x in X & ( for i being set st i in dom G holds

( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) ) holds

( f is_differentiable_in x & ( for h being Point of (product G) ex w being FinSequence of S st

( dom w = dom G & ( for i being set st i in dom G holds

w . i = (partdiff (f,x,i)) . ((proj (In (i,(dom G)))) . h) ) & (diff (f,x)) . h = Sum w ) ) )

proof end;

theorem :: NDIFF_5:57

for G being RealNormSpace-Sequence

for F being RealNormSpace

for f being PartFunc of (product G),F

for X being Subset of (product G) st X is open holds

( ( for i being set st i in dom G holds

( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) ) iff ( f is_differentiable_on X & f `| X is_continuous_on X ) )

for F being RealNormSpace

for f being PartFunc of (product G),F

for X being Subset of (product G) st X is open holds

( ( for i being set st i in dom G holds

( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) ) iff ( f is_differentiable_on X & f `| X is_continuous_on X ) )

proof end;