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

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

let h be set ; :: thesis: ( h in [.p,q.] implies h in dom (f * (reproj ((modetrans (G,i)),x))) )
assume A3: 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))) ;
A4: 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, A3;
hence h in dom (f * (reproj ((modetrans (G,i)),x))) by A4, FUNCT_1:11; :: thesis: verum

end;

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

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

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 A7: x0 in [.p,q.] ; :: thesis: f * (reproj ((modetrans (G,i)),x)) is_differentiable_in x0
set y = (reproj ((modetrans (G,i)),x)) . x0;
A8: (proj (modetrans (G,i))) . ((reproj ((modetrans (G,i)),x)) . x0) = x0 by Th46;
f is_partial_differentiable_in (reproj ((modetrans (G,i)),x)) . x0,i by A1, A7;
then f * (reproj ((modetrans (G,i)),((reproj ((modetrans (G,i)),x)) . x0))) is_differentiable_in x0 by A8, Def6;
hence f * (reproj ((modetrans (G,i)),x)) is_differentiable_in x0 by Th48; :: thesis: verum

end;

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

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
A9: ( z = p + (z1 * (q - p)) & 0 < z1 & z1 < 1 ) ;
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 ].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 A6;
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 A6, NDIFF_1:44;

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

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 A13: ||.((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 Th46;
hence ||.((diff ((f * (reproj ((modetrans (G,i)),x))),h)) - L).|| <= M by A13, Th48; :: thesis: verum

end;

A14: ( p in dom (f * (reproj ((modetrans (G,i)),x))) & q in dom (f * (reproj ((modetrans (G,i)),x))) ) by A2, 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 A14, PARTFUN2:3;
hence ||.(((f /. ((reproj ((modetrans (G,i)),x)) . q)) - (f /. ((reproj ((modetrans (G,i)),x)) . p))) - (L . (q - p))).|| <= M * ||.(q - p).|| by A12, Th20, A5, A10, A11; :: thesis: verum