let G be RealNormSpace-Sequence; :: thesis: 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
let S be 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 . (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
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 . (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
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 . (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
let x, y, z be Point of (product G); :: thesis: 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
let i0 be set ; :: thesis: for p, q being Point of (G . (In (i0,(dom G))))
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 ((In (i0,(dom G))),y)) . p & q = (proj (In (i0,(dom G)))) . y holds
||.(((f /. z) - (f /. y)) - ((partdiff (f,x,i0)) . (p - q))).|| <= ||.(p - q).|| * r
let p, q be Point of (G . (In (i0,(dom G)))); :: 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 ((In (i0,(dom G))),y)) . p & q = (proj (In (i0,(dom G)))) . 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 ((In (i0,(dom G))),y)) . p & q = (proj (In (i0,(dom G)))) . 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 ((In (i0,(dom G))),y)) . p & q = (proj (In (i0,(dom G)))) . y ) ; :: thesis: ||.(((f /. z) - (f /. y)) - ((partdiff (f,x,i0)) . (p - q))).|| <= ||.(p - q).|| * r
set i = In (i0,(dom G));
A2: y = (reproj ((In (i0,(dom G))),y)) . q by A1, Th47;

A3: now :: thesis: for h being Point of (G . (In (i0,(dom G)))) st h in [.q,p.] holds
(reproj ((In (i0,(dom G))),y)) . h in dom f

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

end;

A4: now :: thesis: for h being Point of (G . (In (i0,(dom G)))) st h in [.q,p.] holds
f is_partial_differentiable_in (reproj ((In (i0,(dom G))),y)) . h,i0

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

end;

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

proof

let h be Point of (G . (In (i0,(dom G)))); :: thesis: ( h in ].q,p.[ implies ||.((partdiff (f,((reproj ((In (i0,(dom G))),y)) . h),i0)) - (partdiff (f,x,i0))).|| <= r )
assume A5: h in ].q,p.[ ; :: thesis: ||.((partdiff (f,((reproj ((In (i0,(dom G))),y)) . h),i0)) - (partdiff (f,x,i0))).|| <= r
].q,p.[ c= [.q,p.] by XBOOLE_1:36;
then ||.(((reproj ((In (i0,(dom G))),y)) . h) - x).|| < d by A1, A5, Th52;
hence ||.((partdiff (f,((reproj ((In (i0,(dom G))),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 A2, A1, Th51, A3, A4; :: thesis: verum