let G be non-trivial RealNormSpace-Sequence; :: thesis: for F being non trivial 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 . (modetrans (G,i))),F))
for p, q being Point of (G . (modetrans (G,i))) st i in dom G & ( for h being Point of (G . (modetrans (G,i))) st h in ].p,q.[ holds
||.((partdiff (f,((reproj ((modetrans (G,i)),x)) . h),i)) - L).|| <= M ) & ( for h being Point of (G . (modetrans (G,i))) st h in [.p,q.] holds
(reproj ((modetrans (G,i)),x)) . h in dom f ) & ( for h being Point of (G . (modetrans (G,i))) st h in [.p,q.] holds
f is_partial_differentiable_in (reproj ((modetrans (G,i)),x)) . h,i ) holds
||.(((f /. ((reproj ((modetrans (G,i)),x)) . q)) - (f /. ((reproj ((modetrans (G,i)),x)) . p))) - (L . (q - p))).|| <= M * ||.(q - p).||
let F be non trivial 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 . (modetrans (G,i))),F))
for p, q being Point of (G . (modetrans (G,i))) st i in dom G & ( for h being Point of (G . (modetrans (G,i))) st h in ].p,q.[ holds
||.((partdiff (f,((reproj ((modetrans (G,i)),x)) . h),i)) - L).|| <= M ) & ( for h being Point of (G . (modetrans (G,i))) st h in [.p,q.] holds
(reproj ((modetrans (G,i)),x)) . h in dom f ) & ( for h being Point of (G . (modetrans (G,i))) st h in [.p,q.] holds
f is_partial_differentiable_in (reproj ((modetrans (G,i)),x)) . h,i ) holds
||.(((f /. ((reproj ((modetrans (G,i)),x)) . q)) - (f /. ((reproj ((modetrans (G,i)),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 . (modetrans (G,i))),F))
for p, q being Point of (G . (modetrans (G,i))) st i in dom G & ( for h being Point of (G . (modetrans (G,i))) st h in ].p,q.[ holds
||.((partdiff (f,((reproj ((modetrans (G,i)),x)) . h),i)) - L).|| <= M ) & ( for h being Point of (G . (modetrans (G,i))) st h in [.p,q.] holds
(reproj ((modetrans (G,i)),x)) . h in dom f ) & ( for h being Point of (G . (modetrans (G,i))) st h in [.p,q.] holds
f is_partial_differentiable_in (reproj ((modetrans (G,i)),x)) . h,i ) holds
||.(((f /. ((reproj ((modetrans (G,i)),x)) . q)) - (f /. ((reproj ((modetrans (G,i)),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 . (modetrans (G,i))),F))
for p, q being Point of (G . (modetrans (G,i))) st i in dom G & ( for h being Point of (G . (modetrans (G,i))) st h in ].p,q.[ holds
||.((partdiff (f,((reproj ((modetrans (G,i)),x)) . h),i)) - L).|| <= M ) & ( for h being Point of (G . (modetrans (G,i))) st h in [.p,q.] holds
(reproj ((modetrans (G,i)),x)) . h in dom f ) & ( for h being Point of (G . (modetrans (G,i))) st h in [.p,q.] holds
f is_partial_differentiable_in (reproj ((modetrans (G,i)),x)) . h,i ) holds
||.(((f /. ((reproj ((modetrans (G,i)),x)) . q)) - (f /. ((reproj ((modetrans (G,i)),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 . (modetrans (G,i))),F))
for p, q being Point of (G . (modetrans (G,i))) st i in dom G & ( for h being Point of (G . (modetrans (G,i))) st h in ].p,q.[ holds
||.((partdiff (f,((reproj ((modetrans (G,i)),x)) . h),i)) - L).|| <= M ) & ( for h being Point of (G . (modetrans (G,i))) st h in [.p,q.] holds
(reproj ((modetrans (G,i)),x)) . h in dom f ) & ( for h being Point of (G . (modetrans (G,i))) st h in [.p,q.] holds
f is_partial_differentiable_in (reproj ((modetrans (G,i)),x)) . h,i ) holds
||.(((f /. ((reproj ((modetrans (G,i)),x)) . q)) - (f /. ((reproj ((modetrans (G,i)),x)) . p))) - (L . (q - p))).|| <= M * ||.(q - p).||
let M be Real; :: thesis: for L being Point of (R_NormSpace_of_BoundedLinearOperators ((G . (modetrans (G,i))),F))
for p, q being Point of (G . (modetrans (G,i))) st i in dom G & ( for h being Point of (G . (modetrans (G,i))) st h in ].p,q.[ holds
||.((partdiff (f,((reproj ((modetrans (G,i)),x)) . h),i)) - L).|| <= M ) & ( for h being Point of (G . (modetrans (G,i))) st h in [.p,q.] holds
(reproj ((modetrans (G,i)),x)) . h in dom f ) & ( for h being Point of (G . (modetrans (G,i))) st h in [.p,q.] holds
f is_partial_differentiable_in (reproj ((modetrans (G,i)),x)) . h,i ) holds
||.(((f /. ((reproj ((modetrans (G,i)),x)) . q)) - (f /. ((reproj ((modetrans (G,i)),x)) . p))) - (L . (q - p))).|| <= M * ||.(q - p).||
let L be Point of (R_NormSpace_of_BoundedLinearOperators ((G . (modetrans (G,i))),F)); :: thesis: for p, q being Point of (G . (modetrans (G,i))) st i in dom G & ( for h being Point of (G . (modetrans (G,i))) st h in ].p,q.[ holds
||.((partdiff (f,((reproj ((modetrans (G,i)),x)) . h),i)) - L).|| <= M ) & ( for h being Point of (G . (modetrans (G,i))) st h in [.p,q.] holds
(reproj ((modetrans (G,i)),x)) . h in dom f ) & ( for h being Point of (G . (modetrans (G,i))) st h in [.p,q.] holds
f is_partial_differentiable_in (reproj ((modetrans (G,i)),x)) . h,i ) holds
||.(((f /. ((reproj ((modetrans (G,i)),x)) . q)) - (f /. ((reproj ((modetrans (G,i)),x)) . p))) - (L . (q - p))).|| <= M * ||.(q - p).||
let p, q be Point of (G . (modetrans (G,i))); :: thesis: ( i in dom G & ( for h being Point of (G . (modetrans (G,i))) st h in ].p,q.[ holds
||.((partdiff (f,((reproj ((modetrans (G,i)),x)) . h),i)) - L).|| <= M ) & ( for h being Point of (G . (modetrans (G,i))) st h in [.p,q.] holds
(reproj ((modetrans (G,i)),x)) . h in dom f ) & ( for h being Point of (G . (modetrans (G,i))) st h in [.p,q.] holds
f is_partial_differentiable_in (reproj ((modetrans (G,i)),x)) . h,i ) implies ||.(((f /. ((reproj ((modetrans (G,i)),x)) . q)) - (f /. ((reproj ((modetrans (G,i)),x)) . p))) - (L . (q - p))).|| <= M * ||.(q - p).|| )
assume A1: ( i in dom G & ( for h being Point of (G . (modetrans (G,i))) st h in ].p,q.[ holds
||.((partdiff (f,((reproj ((modetrans (G,i)),x)) . h),i)) - L).|| <= M ) & ( for h being Point of (G . (modetrans (G,i))) st h in [.p,q.] holds
(reproj ((modetrans (G,i)),x)) . h in dom f ) & ( for h being Point of (G . (modetrans (G,i))) st h in [.p,q.] holds
f is_partial_differentiable_in (reproj ((modetrans (G,i)),x)) . h,i ) ) ; :: thesis: ||.(((f /. ((reproj ((modetrans (G,i)),x)) . q)) - (f /. ((reproj ((modetrans (G,i)),x)) . p))) - (L . (q - p))).|| <= M * ||.(q - p).||
set m = len G;
set S = G . (modetrans (G,i));
set g = f * (reproj ((modetrans (G,i)),x));

A6: now

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

end;

then A4: [.p,q.] c= dom (f * (reproj ((modetrans (G,i)),x))) by TARSKI:def 3;

A5: now

let x0 be Point of (G . (modetrans (G,i))); :: thesis: ( x0 in [.p,q.] implies f * (reproj ((modetrans (G,i)),x)) is_differentiable_in x0 )
assume A6: x0 in [.p,q.] ; :: thesis: f * (reproj ((modetrans (G,i)),x)) is_differentiable_in x0
set y = (reproj ((modetrans (G,i)),x)) . x0;
A7: (proj (modetrans (G,i))) . ((reproj ((modetrans (G,i)),x)) . x0) = x0 by XTh39;
f is_partial_differentiable_in (reproj ((modetrans (G,i)),x)) . x0,i by A1, A6;
then f * (reproj ((modetrans (G,i)),((reproj ((modetrans (G,i)),x)) . x0))) is_differentiable_in x0 by A7, Def9;
hence f * (reproj ((modetrans (G,i)),x)) is_differentiable_in x0 by XTh40; :: thesis: verum

end;

now

let z be set ; :: 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
AB: ( z = p + (z1 * (q - p)) & 0 < z1 & z1 < 1 ) ;
z = ((1 - z1) * p) + (z1 * q) by AB, LmX;
then z in { (((1 - r1) * p) + (r1 * q)) where r1 is Real : ( 0 <= r1 & r1 <= 1 ) } by AB;
hence z in [.p,q.] by RLTOPSP1:def 2; :: thesis: verum

end;

then ].p,q.[ c= [.p,q.] by TARSKI:def 3;
then A10: for x being Point of (G . (modetrans (G,i))) st x in ].p,q.[ holds
f * (reproj ((modetrans (G,i)),x)) is_differentiable_in x by A5;
A11: for x being Point of (G . (modetrans (G,i))) st x in [.p,q.] holds
f * (reproj ((modetrans (G,i)),x)) is_continuous_in x by A5, NDIFF_1:44;

U0: now

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

end;

U1: ( p in dom (f * (reproj ((modetrans (G,i)),x))) & q in dom (f * (reproj ((modetrans (G,i)),x))) ) by A6, RLTOPSP1:68;
( f /. ((reproj ((modetrans (G,i)),x)) . p) = f /. ((reproj ((modetrans (G,i)),x)) /. p) & f /. ((reproj ((modetrans (G,i)),x)) . q) = f /. ((reproj ((modetrans (G,i)),x)) /. q) ) ;
then ( f /. ((reproj ((modetrans (G,i)),x)) . p) = (f * (reproj ((modetrans (G,i)),x))) /. p & f /. ((reproj ((modetrans (G,i)),x)) . q) = (f * (reproj ((modetrans (G,i)),x))) /. q ) by U1, PARTFUN2:3;
hence ||.(((f /. ((reproj ((modetrans (G,i)),x)) . q)) - (f /. ((reproj ((modetrans (G,i)),x)) . p))) - (L . (q - p))).|| <= M * ||.(q - p).|| by U0, FDAF20, A4, A10, A11; :: thesis: verum