let G be non-trivial RealNormSpace-Sequence; :: thesis: for S being non trivial 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 . (modetrans (G,i)))
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 ((modetrans (G,i)),y)) . p & q = (proj (modetrans (G,i))) . y holds
||.(((f /. z) - (f /. y)) - ((partdiff (f,x,i)) . (p - q))).|| <= ||.(p - q).|| * r
let S be non trivial RealNormSpace; :: thesis: 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 . (modetrans (G,i)))
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 ((modetrans (G,i)),y)) . p & q = (proj (modetrans (G,i))) . y holds
||.(((f /. z) - (f /. y)) - ((partdiff (f,x,i)) . (p - q))).|| <= ||.(p - q).|| * r
let f be PartFunc of (product G),S; :: thesis: 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 . (modetrans (G,i)))
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 ((modetrans (G,i)),y)) . p & q = (proj (modetrans (G,i))) . y holds
||.(((f /. z) - (f /. y)) - ((partdiff (f,x,i)) . (p - q))).|| <= ||.(p - q).|| * r
let X be Subset of (product G); :: thesis: for x, y, z being Point of (product G)
for i being set
for p, q being Point of (G . (modetrans (G,i)))
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 ((modetrans (G,i)),y)) . p & q = (proj (modetrans (G,i))) . y holds
||.(((f /. z) - (f /. y)) - ((partdiff (f,x,i)) . (p - q))).|| <= ||.(p - q).|| * r
let x, y, z be Point of (product G); :: thesis: for i being set
for p, q being Point of (G . (modetrans (G,i)))
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 ((modetrans (G,i)),y)) . p & q = (proj (modetrans (G,i))) . y holds
||.(((f /. z) - (f /. y)) - ((partdiff (f,x,i)) . (p - q))).|| <= ||.(p - q).|| * r
let i0 be set ; :: thesis: for p, q being Point of (G . (modetrans (G,i0)))
for d, r being Real st i0 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,i0 ) & ( 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,i0)) - (partdiff (f,x,i0))).|| <= r ) & z = (reproj ((modetrans (G,i0)),y)) . p & q = (proj (modetrans (G,i0))) . y holds
||.(((f /. z) - (f /. y)) - ((partdiff (f,x,i0)) . (p - q))).|| <= ||.(p - q).|| * r
let p, q be Point of (G . (modetrans (G,i0))); :: thesis: for d, r being Real st i0 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,i0 ) & ( 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,i0)) - (partdiff (f,x,i0))).|| <= r ) & z = (reproj ((modetrans (G,i0)),y)) . p & q = (proj (modetrans (G,i0))) . y holds
||.(((f /. z) - (f /. y)) - ((partdiff (f,x,i0)) . (p - q))).|| <= ||.(p - q).|| * r
let d, r be Real; :: thesis: ( i0 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,i0 ) & ( 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,i0)) - (partdiff (f,x,i0))).|| <= r ) & z = (reproj ((modetrans (G,i0)),y)) . p & q = (proj (modetrans (G,i0))) . y implies ||.(((f /. z) - (f /. y)) - ((partdiff (f,x,i0)) . (p - q))).|| <= ||.(p - q).|| * r )
assume A1: ( i0 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,i0 ) & ( 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,i0)) - (partdiff (f,x,i0))).|| <= r ) & z = (reproj ((modetrans (G,i0)),y)) . p & q = (proj (modetrans (G,i0))) . y ) ; :: thesis: ||.(((f /. z) - (f /. y)) - ((partdiff (f,x,i0)) . (p - q))).|| <= ||.(p - q).|| * r
set i = modetrans (G,i0);
A3: y = (reproj ((modetrans (G,i0)),y)) . q by A1, XTh39A;

A6: now

let h be Point of (G . (modetrans (G,i0))); :: thesis: ( h in [.q,p.] implies (reproj ((modetrans (G,i0)),y)) . h in dom f )
assume h in [.q,p.] ; :: thesis: (reproj ((modetrans (G,i0)),y)) . h in dom f
then ||.(((reproj ((modetrans (G,i0)),y)) . h) - x).|| < d by A1, XTh44;
then (reproj ((modetrans (G,i0)),y)) . h in X by A1;
hence (reproj ((modetrans (G,i0)),y)) . h in dom f by A1; :: thesis: verum

end;

A7: now

let h be Point of (G . (modetrans (G,i0))); :: thesis: ( h in [.q,p.] implies f is_partial_differentiable_in (reproj ((modetrans (G,i0)),y)) . h,i0 )
assume h in [.q,p.] ; :: thesis: f is_partial_differentiable_in (reproj ((modetrans (G,i0)),y)) . h,i0
then ||.(((reproj ((modetrans (G,i0)),y)) . h) - x).|| < d by A1, XTh44;
hence f is_partial_differentiable_in (reproj ((modetrans (G,i0)),y)) . h,i0 by A1; :: thesis: verum

end;

for h being Point of (G . (modetrans (G,i0))) st h in ].q,p.[ holds
||.((partdiff (f,((reproj ((modetrans (G,i0)),y)) . h),i0)) - (partdiff (f,x,i0))).|| <= r

proof

let h be Point of (G . (modetrans (G,i0))); :: thesis: ( h in ].q,p.[ implies ||.((partdiff (f,((reproj ((modetrans (G,i0)),y)) . h),i0)) - (partdiff (f,x,i0))).|| <= r )
assume X1: h in ].q,p.[ ; :: thesis: ||.((partdiff (f,((reproj ((modetrans (G,i0)),y)) . h),i0)) - (partdiff (f,x,i0))).|| <= r
].q,p.[ c= [.q,p.] by LMDefCLS1;
then ||.(((reproj ((modetrans (G,i0)),y)) . h) - x).|| < d by A1, X1, XTh44;
hence ||.((partdiff (f,((reproj ((modetrans (G,i0)),y)) . h),i0)) - (partdiff (f,x,i0))).|| <= r by A1; :: thesis: verum

end;

hence ||.(((f /. z) - (f /. y)) - ((partdiff (f,x,i0)) . (p - q))).|| <= ||.(p - q).|| * r by A3, A1, XTh42, A6, A7; :: thesis: verum