:: Differentiable Functions on Normed Linear Spaces
:: by Yasunari Shidama
::
:: Received June 2, 2011
:: Copyright (c) 2011-2021 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 ) ) )

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.| ) )

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

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

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

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)) )

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

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

proof end;

theorem Th9: :: NDIFF_5:9

for X being non-empty FinSequence
for x being set st x in product X holds
x is FinSequence

proof end;

registration

let G be RealNormSpace-Sequence;

cluster product G -> constituted-FinSeqs ;

coherence
product G is constituted-FinSeqs

proof end;

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_1:def 11;
hence dom (carr G) = Seg (len G) by FINSEQ_1:def 3
.= dom G by FINSEQ_1:def 3 ;
:: thesis: verum

end;

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);

proof end;

end;

theorem Th10: :: NDIFF_5:10

for G being RealNormSpace-Sequence holds the carrier of (product G) = product (carr G)

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)

proof end;

definition

let G be RealNormSpace-Sequence;

attr G is non-trivial means :Def1: :: NDIFF_5:def 1
for j being Element of dom G holds not G . j is trivial ;

end;

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

registration

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

correctness
existence
ex b₁ being RealNormSpace-Sequence st b₁ is non-trivial ;

proof end;

end;

registration

let G be non-trivial RealNormSpace-Sequence;
let i be Element of dom G;

cluster G . i -> non trivial for RealNormSpace;

correctness
coherence
for b₁ being RealNormSpace st b₁ = G . i holds
not b₁ is trivial ;
by Def1;

end;

registration

let G be non-trivial RealNormSpace-Sequence;

cluster product G -> non trivial ;

correctness
coherence
not product G is trivial ;

proof end;

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) )

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) )

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) )

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) )

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)

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;

notation

let S be RealLinearSpace;
let p, q be Point of S;
synonym [.p,q.] for LSeg (p,q);

end;

definition

let S be RealLinearSpace;
let p, q be Point of S;

func ].p,q.[ -> Subset of S equals :: NDIFF_5:def 2
[.p,q.] \ {p,q};

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

end;

:: deftheorem defines ]. NDIFF_5:def 2 :
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 ) }

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 ) ) )

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 ) ) )

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).||

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).||

proof end;

definition

let G be RealNormSpace-Sequence;
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
ex b₁ being Function of (product G),(G . i) st
for x being Element of product (carr G) holds b₁ . x = x . i

proof end;

uniqueness
for b₁, b₂ being Function of (product G),(G . i) st ( for x being Element of product (carr G) holds b₁ . x = x . i ) & ( for x being Element of product (carr G) holds b₂ . x = x . i ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines proj NDIFF_5:def 3 :
for G being RealNormSpace-Sequence
for i being Element of dom G
for b₃ being Function of (product G),(G . i) holds
( b₃ = proj i iff for x being Element of product (carr G) holds b₃ . x = x . i );

definition

let G be RealNormSpace-Sequence;
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
ex b₁ being Function of (G . i),(product G) st
for r being Element of (G . i) holds b₁ . r = x +* (i,r)

proof end;

uniqueness
for b₁, b₂ being Function of (G . i),(product G) st ( for r being Element of (G . i) holds b₁ . r = x +* (i,r) ) & ( for r being Element of (G . i) holds b₂ . r = x +* (i,r) ) holds
b₁ = b₂

proof end;

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₄ being Function of (G . i),(product G) holds
( b₄ = reproj (i,x) iff for r being Element of (G . i) holds b₄ . r = x +* (i,r) );

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);

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;

end;

:: deftheorem NDIFF_5:def 5 :
canceled;

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

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);

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)) is Point of (R_NormSpace_of_BoundedLinearOperators ((G . (In (i,(dom G)))),F)) ;

end;

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

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 ;

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 ) );

end;

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

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.||

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) )

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

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 ) ) )

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;

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 ;

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
ex b₁ being PartFunc of (product G),(R_NormSpace_of_BoundedLinearOperators ((G . (In (i,(dom G)))),S)) st
( dom b₁ = X & ( for x being Point of (product G) st x in X holds
b₁ /. x = partdiff (f,x,i) ) )

proof end;

uniqueness
for b₁, b₂ being PartFunc of (product G),(R_NormSpace_of_BoundedLinearOperators ((G . (In (i,(dom G)))),S)) st dom b₁ = X & ( for x being Point of (product G) st x in X holds
b₁ /. x = partdiff (f,x,i) ) & dom b₂ = X & ( for x being Point of (product G) st x in X holds
b₂ /. x = partdiff (f,x,i) ) holds
b₁ = b₂

proof end;

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<sub>6</sub> being PartFunc of (product G),(R_NormSpace_of_BoundedLinearOperators ((G . (In (i,(dom G)))),S)) holds
( b<sub>6</sub> = f `partial| (X,i) iff ( dom b₆ = X & ( for x being Point of (product G) st x in X holds
b₆ /. x = partdiff (f,x,i) ) ) );

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))) )

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))

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)) )

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)) )

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)) )

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.||

proof end;

registration

let G be RealNormSpace-Sequence;

cluster -> len G -element for Element of the carrier of (product G);

coherence
for b₁ being Point of (product G) holds b₁ is len G -element

proof end;

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 ) ) )

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) ) )

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)

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)

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)

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)

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)

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)

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)

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)))) )

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

proof end;

theorem :: NDIFF_5:43

for G being RealNormSpace-Sequence
for x, y being Element of product (carr G)
for Z being set holds x +* (y | Z) is Element of product (carr G) by CARD_3:79;

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.||

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 )

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

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

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)

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

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)

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).||

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

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

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))

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

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 ) ) )

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 ) )

proof end;