let G be RealNormSpace-Sequence; :: thesis: 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).||
let F be RealNormSpace; :: thesis: 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).||
let f be PartFunc of (product G),F; :: thesis: 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).||
let x be Point of (product G); :: thesis: 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).||
let i be set ; :: thesis: 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).||
let M be Real; :: thesis: 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).||
let L be Point of (R_NormSpace_of_BoundedLinearOperators ((G . (In (i,(dom G)))),F)); :: thesis: 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).||
let p, q be Point of (G . (In (i,(dom G)))); :: thesis: ( 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 ) implies ||.(((f /. ((reproj ((In (i,(dom G))),x)) . q)) - (f /. ((reproj ((In (i,(dom G))),x)) . p))) - (L . (q - p))).|| <= M * ||.(q - p).|| )
assume A1: ( 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 ) ) ; :: thesis: ||.(((f /. ((reproj ((In (i,(dom G))),x)) . q)) - (f /. ((reproj ((In (i,(dom G))),x)) . p))) - (L . (q - p))).|| <= M * ||.(q - p).||

per cases ( p = q or p <> q ) ;

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

set S = G . (In (i,(dom G)));
reconsider LL = L as Lipschitzian LinearOperator of (G . (In (i,(dom G)))),F by LOPBAN_1:def 9;
B3: L . (0. (G . (In (i,(dom G))))) = LL . (0 * (0. (G . (In (i,(dom G)))))) by RLVECT_1:10
.= 0 * (LL . (0. (G . (In (i,(dom G)))))) by LOPBAN_1:def 5
.= 0. F by RLVECT_1:10 ;
B4: ||.(((f /. ((reproj ((In (i,(dom G))),x)) . q)) - (f /. ((reproj ((In (i,(dom G))),x)) . p))) - (L . (q - p))).|| = ||.((0. F) - (L . (q - p))).|| by B2, RLVECT_1:15
.= ||.((0. F) - (L . (0. (G . (In (i,(dom G))))))).|| by B2, RLVECT_1:15
.= ||.(0. F).|| by B3, RLVECT_1:13
.= 0 ;
M * ||.(q - p).|| = M * ||.(0. (G . (In (i,(dom G))))).|| by B2, RLVECT_1:15
.= 0 ;
hence ||.(((f /. ((reproj ((In (i,(dom G))),x)) . q)) - (f /. ((reproj ((In (i,(dom G))),x)) . p))) - (L . (q - p))).|| <= M * ||.(q - p).|| by B4; :: thesis: verum

end;

suppose ASM: p <> q ; :: thesis: ||.(((f /. ((reproj ((In (i,(dom G))),x)) . q)) - (f /. ((reproj ((In (i,(dom G))),x)) . p))) - (L . (q - p))).|| <= M * ||.(q - p).||

set m = len G;
set S = G . (In (i,(dom G)));
set g = f * (reproj ((In (i,(dom G))),x));

A2: now :: thesis: for h being object st h in [.p,q.] holds
h in dom (f * (reproj ((In (i,(dom G))),x)))

let h be object ; :: thesis: ( h in [.p,q.] implies h in dom (f * (reproj ((In (i,(dom G))),x))) )
assume A3: h in [.p,q.] ; :: thesis: h in dom (f * (reproj ((In (i,(dom G))),x)))
then reconsider h1 = h as Point of (G . (In (i,(dom G)))) ;
A4: dom (reproj ((In (i,(dom G))),x)) = the carrier of (G . (In (i,(dom G)))) by FUNCT_2:def 1;
(reproj ((In (i,(dom G))),x)) . h1 in dom f by A1, A3;
hence h in dom (f * (reproj ((In (i,(dom G))),x))) by A4, FUNCT_1:11; :: thesis: verum

end;

then A5: [.p,q.] c= dom (f * (reproj ((In (i,(dom G))),x))) ;

A6: now :: thesis: for x0 being Point of (G . (In (i,(dom G)))) st x0 in [.p,q.] holds
f * (reproj ((In (i,(dom G))),x)) is_differentiable_in x0

let x0 be Point of (G . (In (i,(dom G)))); :: thesis: ( x0 in [.p,q.] implies f * (reproj ((In (i,(dom G))),x)) is_differentiable_in x0 )
assume A7: x0 in [.p,q.] ; :: thesis: f * (reproj ((In (i,(dom G))),x)) is_differentiable_in x0
set y = (reproj ((In (i,(dom G))),x)) . x0;
A8: (proj (In (i,(dom G)))) . ((reproj ((In (i,(dom G))),x)) . x0) = x0 by Th46;
f is_partial_differentiable_in (reproj ((In (i,(dom G))),x)) . x0,i by A1, A7;
hence f * (reproj ((In (i,(dom G))),x)) is_differentiable_in x0 by A8, Th48; :: thesis: verum

end;

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

now :: thesis: for z being object st z in ].p,q.[ holds
z in [.p,q.]

let z be object ; :: thesis: ( z in ].p,q.[ implies z in [.p,q.] )
assume z in ].p,q.[ ; :: thesis: z in [.p,q.]
then consider z1 being Real such that
A9: ( z = p + (z1 * (q - p)) & 0 < z1 & z1 < 1 ) by X1;
z = ((1 - z1) * p) + (z1 * q) by A9, Lm2;
then z in { (((1 - r1) * p) + (r1 * q)) where r1 is Real : ( 0 <= r1 & r1 <= 1 ) } by A9;
hence z in [.p,q.] by RLTOPSP1:def 2; :: thesis: verum

end;

then A10: for x being Point of (G . (In (i,(dom G)))) st x in ].p,q.[ holds
f * (reproj ((In (i,(dom G))),x)) is_differentiable_in x by A6;
A11: for x being Point of (G . (In (i,(dom G)))) st x in [.p,q.] holds
f * (reproj ((In (i,(dom G))),x)) is_continuous_in x by A6, NDIFF_1:44;

A12: now :: thesis: for h being Point of (G . (In (i,(dom G)))) st h in ].p,q.[ holds
||.((diff ((f * (reproj ((In (i,(dom G))),x))),h)) - L).|| <= M

let h be Point of (G . (In (i,(dom G)))); :: thesis: ( h in ].p,q.[ implies ||.((diff ((f * (reproj ((In (i,(dom G))),x))),h)) - L).|| <= M )
set y = (reproj ((In (i,(dom G))),x)) . h;
assume h in ].p,q.[ ; :: thesis: ||.((diff ((f * (reproj ((In (i,(dom G))),x))),h)) - L).|| <= M
then A13: ||.((partdiff (f,((reproj ((In (i,(dom G))),x)) . h),i)) - L).|| <= M by A1;
(proj (In (i,(dom G)))) . ((reproj ((In (i,(dom G))),x)) . h) = h by Th46;
hence ||.((diff ((f * (reproj ((In (i,(dom G))),x))),h)) - L).|| <= M by A13, Th48; :: thesis: verum

end;

A14: ( p in dom (f * (reproj ((In (i,(dom G))),x))) & q in dom (f * (reproj ((In (i,(dom G))),x))) ) by A2, RLTOPSP1:68;
( f /. ((reproj ((In (i,(dom G))),x)) . p) = f /. ((reproj ((In (i,(dom G))),x)) /. p) & f /. ((reproj ((In (i,(dom G))),x)) . q) = f /. ((reproj ((In (i,(dom G))),x)) /. q) ) ;
then ( f /. ((reproj ((In (i,(dom G))),x)) . p) = (f * (reproj ((In (i,(dom G))),x))) /. p & f /. ((reproj ((In (i,(dom G))),x)) . q) = (f * (reproj ((In (i,(dom G))),x))) /. q ) by A14, PARTFUN2:3;
hence ||.(((f /. ((reproj ((In (i,(dom G))),x)) . q)) - (f /. ((reproj ((In (i,(dom G))),x)) . p))) - (L . (q - p))).|| <= M * ||.(q - p).|| by A12, Th20, A5, A10, A11; :: thesis: verum

end;

end;