let G be RealNormSpace-Sequence; :: thesis: for T being RealNormSpace
for i being set
for f being PartFunc of (product G),T
for Z being Subset of (product G) st Z is open holds
( f is_partial_differentiable_on Z,i iff ( Z c= dom f & ( for x being Point of (product G) st x in Z holds
f is_partial_differentiable_in x,i ) ) )
let T be RealNormSpace; :: thesis: for i being set
for f being PartFunc of (product G),T
for Z being Subset of (product G) st Z is open holds
( f is_partial_differentiable_on Z,i iff ( Z c= dom f & ( for x being Point of (product G) st x in Z holds
f is_partial_differentiable_in x,i ) ) )
let i be set ; :: thesis: for f being PartFunc of (product G),T
for Z being Subset of (product G) st Z is open holds
( f is_partial_differentiable_on Z,i iff ( Z c= dom f & ( for x being Point of (product G) st x in Z holds
f is_partial_differentiable_in x,i ) ) )
let f be PartFunc of (product G),T; :: thesis: for Z being Subset of (product G) st Z is open holds
( f is_partial_differentiable_on Z,i iff ( Z c= dom f & ( for x being Point of (product G) st x in Z holds
f is_partial_differentiable_in x,i ) ) )
let Z be Subset of (product G); :: thesis: ( Z is open implies ( f is_partial_differentiable_on Z,i iff ( Z c= dom f & ( for x being Point of (product G) st x in Z holds
f is_partial_differentiable_in x,i ) ) ) )
assume A1: Z is open ; :: thesis: ( f is_partial_differentiable_on Z,i iff ( Z c= dom f & ( for x being Point of (product G) st x in Z holds
f is_partial_differentiable_in x,i ) ) )
set i0 = In (i,(dom G));
set S = G . (In (i,(dom G)));
set RNS = R_NormSpace_of_BoundedLinearOperators ((G . (In (i,(dom G)))),T);
thus ( f is_partial_differentiable_on Z,i implies ( Z c= dom f & ( for x being Point of (product G) st x in Z holds
f is_partial_differentiable_in x,i ) ) ) :: thesis: ( Z c= dom f & ( for x being Point of (product G) st x in Z holds
f is_partial_differentiable_in x,i ) implies f is_partial_differentiable_on Z,i )

proof

assume A2: f is_partial_differentiable_on Z,i ; :: thesis: ( Z c= dom f & ( for x being Point of (product G) st x in Z holds
f is_partial_differentiable_in x,i ) )
hence Z c= dom f ; :: thesis: for x being Point of (product G) st x in Z holds
f is_partial_differentiable_in x,i
let nx0 be Point of (product G); :: thesis: ( nx0 in Z implies f is_partial_differentiable_in nx0,i )
reconsider x0 = (proj (In (i,(dom G)))) . nx0 as Point of (G . (In (i,(dom G)))) ;
assume A4: nx0 in Z ; :: thesis: f is_partial_differentiable_in nx0,i
then f | Z is_partial_differentiable_in nx0,i by A2;
then consider N0 being Neighbourhood of x0 such that
A5: N0 c= dom ((f | Z) * (reproj ((In (i,(dom G))),nx0))) and
A6: ex L being Point of (R_NormSpace_of_BoundedLinearOperators ((G . (In (i,(dom G)))),T)) ex R being RestFunc of (G . (In (i,(dom G)))),T st
for x being Point of (G . (In (i,(dom G)))) st x in N0 holds
(((f | Z) * (reproj ((In (i,(dom G))),nx0))) /. x) - (((f | Z) * (reproj ((In (i,(dom G))),nx0))) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by NDIFF_1:def 6;
consider L being Point of (R_NormSpace_of_BoundedLinearOperators ((G . (In (i,(dom G)))),T)), R being RestFunc of (G . (In (i,(dom G)))),T such that
A7: for x being Point of (G . (In (i,(dom G)))) st x in N0 holds
(((f | Z) * (reproj ((In (i,(dom G))),nx0))) /. x) - (((f | Z) * (reproj ((In (i,(dom G))),nx0))) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A6;
consider N1 being Neighbourhood of x0 such that
A8: for x being Point of (G . (In (i,(dom G)))) st x in N1 holds
(reproj ((In (i,(dom G))),nx0)) . x in Z by A1, A4, Th23;

A9: now :: thesis: for x being Point of (G . (In (i,(dom G)))) st x in N1 holds
(reproj ((In (i,(dom G))),nx0)) . x in dom (f | Z)

let x be Point of (G . (In (i,(dom G)))); :: thesis: ( x in N1 implies (reproj ((In (i,(dom G))),nx0)) . x in dom (f | Z) )
assume x in N1 ; :: thesis: (reproj ((In (i,(dom G))),nx0)) . x in dom (f | Z)
then (reproj ((In (i,(dom G))),nx0)) . x in Z by A8;
then (reproj ((In (i,(dom G))),nx0)) . x in (dom f) /\ Z by A2, XBOOLE_0:def 4;
hence (reproj ((In (i,(dom G))),nx0)) . x in dom (f | Z) by RELAT_1:61; :: thesis: verum

end;

reconsider N = N0 /\ N1 as Neighbourhood of x0 by Th8;
(f | Z) * (reproj ((In (i,(dom G))),nx0)) c= f * (reproj ((In (i,(dom G))),nx0)) by RELAT_1:29, RELAT_1:59;
then A10: dom ((f | Z) * (reproj ((In (i,(dom G))),nx0))) c= dom (f * (reproj ((In (i,(dom G))),nx0))) by RELAT_1:11;
N c= N0 by XBOOLE_1:17;
then A11: N c= dom (f * (reproj ((In (i,(dom G))),nx0))) by A5, A10;

now :: thesis: for x being Point of (G . (In (i,(dom G)))) st x in N holds
((f * (reproj ((In (i,(dom G))),nx0))) /. x) - ((f * (reproj ((In (i,(dom G))),nx0))) /. x0) = (L . (x - x0)) + (R /. (x - x0))

let x be Point of (G . (In (i,(dom G)))); :: thesis: ( x in N implies ((f * (reproj ((In (i,(dom G))),nx0))) /. x) - ((f * (reproj ((In (i,(dom G))),nx0))) /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
assume A12: x in N ; :: thesis: ((f * (reproj ((In (i,(dom G))),nx0))) /. x) - ((f * (reproj ((In (i,(dom G))),nx0))) /. x0) = (L . (x - x0)) + (R /. (x - x0))
then A13: x in N0 by XBOOLE_0:def 4;
A14: dom (reproj ((In (i,(dom G))),nx0)) = the carrier of (G . (In (i,(dom G)))) by FUNCT_2:def 1;
x in N1 by A12, XBOOLE_0:def 4;
then A15: (reproj ((In (i,(dom G))),nx0)) . x in dom (f | Z) by A9;
then A16: ( (reproj ((In (i,(dom G))),nx0)) . x in dom f & (reproj ((In (i,(dom G))),nx0)) . x in Z ) by RELAT_1:57;
A17: (reproj ((In (i,(dom G))),nx0)) . x0 in dom (f | Z) by A9, NFCONT_1:4;
then A18: ( (reproj ((In (i,(dom G))),nx0)) . x0 in dom f & (reproj ((In (i,(dom G))),nx0)) . x0 in Z ) by RELAT_1:57;
A19: ((f | Z) * (reproj ((In (i,(dom G))),nx0))) /. x = (f | Z) /. ((reproj ((In (i,(dom G))),nx0)) /. x) by A15, A14, PARTFUN2:4
.= f /. ((reproj ((In (i,(dom G))),nx0)) /. x) by A16, PARTFUN2:17
.= (f * (reproj ((In (i,(dom G))),nx0))) /. x by A14, A16, PARTFUN2:4 ;
((f | Z) * (reproj ((In (i,(dom G))),nx0))) /. x0 = (f | Z) /. ((reproj ((In (i,(dom G))),nx0)) /. x0) by A14, A17, PARTFUN2:4
.= f /. ((reproj ((In (i,(dom G))),nx0)) /. x0) by A18, PARTFUN2:17
.= (f * (reproj ((In (i,(dom G))),nx0))) /. x0 by A14, A18, PARTFUN2:4 ;
hence ((f * (reproj ((In (i,(dom G))),nx0))) /. x) - ((f * (reproj ((In (i,(dom G))),nx0))) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A7, A13, A19; :: thesis: verum

end;

hence f is_partial_differentiable_in nx0,i by A11, NDIFF_1:def 6; :: thesis: verum

end;

assume that
A20: Z c= dom f and
A21: for nx being Point of (product G) st nx in Z holds
f is_partial_differentiable_in nx,i ; :: thesis: f is_partial_differentiable_on Z,i

now :: thesis: for nx0 being Point of (product G) st nx0 in Z holds
f | Z is_partial_differentiable_in nx0,i

let nx0 be Point of (product G); :: thesis: ( nx0 in Z implies f | Z is_partial_differentiable_in nx0,i )
assume A22: nx0 in Z ; :: thesis: f | Z is_partial_differentiable_in nx0,i
then A23: f is_partial_differentiable_in nx0,i by A21;
reconsider x0 = (proj (In (i,(dom G)))) . nx0 as Point of (G . (In (i,(dom G)))) ;
consider N0 being Neighbourhood of x0 such that
N0 c= dom (f * (reproj ((In (i,(dom G))),nx0))) and
A24: ex L being Point of (R_NormSpace_of_BoundedLinearOperators ((G . (In (i,(dom G)))),T)) ex R being RestFunc of (G . (In (i,(dom G)))),T st
for x being Point of (G . (In (i,(dom G)))) st x in N0 holds
((f * (reproj ((In (i,(dom G))),nx0))) /. x) - ((f * (reproj ((In (i,(dom G))),nx0))) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A23, NDIFF_1:def 6;
consider N1 being Neighbourhood of x0 such that
A25: for x being Point of (G . (In (i,(dom G)))) st x in N1 holds
(reproj ((In (i,(dom G))),nx0)) . x in Z by A1, A22, Th23;

A26: now :: thesis: for x being Point of (G . (In (i,(dom G)))) st x in N1 holds
(reproj ((In (i,(dom G))),nx0)) . x in dom (f | Z)

let x be Point of (G . (In (i,(dom G)))); :: thesis: ( x in N1 implies (reproj ((In (i,(dom G))),nx0)) . x in dom (f | Z) )
assume x in N1 ; :: thesis: (reproj ((In (i,(dom G))),nx0)) . x in dom (f | Z)
then (reproj ((In (i,(dom G))),nx0)) . x in Z by A25;
then (reproj ((In (i,(dom G))),nx0)) . x in (dom f) /\ Z by A20, XBOOLE_0:def 4;
hence (reproj ((In (i,(dom G))),nx0)) . x in dom (f | Z) by RELAT_1:61; :: thesis: verum

end;

A27: N1 c= dom ((f | Z) * (reproj ((In (i,(dom G))),nx0)))

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in N1 or z in dom ((f | Z) * (reproj ((In (i,(dom G))),nx0))) )
assume A28: z in N1 ; :: thesis: z in dom ((f | Z) * (reproj ((In (i,(dom G))),nx0)))
then A29: z in the carrier of (G . (In (i,(dom G)))) ;
reconsider x = z as Point of (G . (In (i,(dom G)))) by A28;
A30: (reproj ((In (i,(dom G))),nx0)) . x in dom (f | Z) by A28, A26;
z in dom (reproj ((In (i,(dom G))),nx0)) by A29, FUNCT_2:def 1;
hence z in dom ((f | Z) * (reproj ((In (i,(dom G))),nx0))) by A30, FUNCT_1:11; :: thesis: verum

end;

reconsider N = N0 /\ N1 as Neighbourhood of x0 by Th8;
N c= N1 by XBOOLE_1:17;
then A31: N c= dom ((f | Z) * (reproj ((In (i,(dom G))),nx0))) by A27;
consider L being Point of (R_NormSpace_of_BoundedLinearOperators ((G . (In (i,(dom G)))),T)), R being RestFunc of (G . (In (i,(dom G)))),T such that
A32: for x being Point of (G . (In (i,(dom G)))) st x in N0 holds
((f * (reproj ((In (i,(dom G))),nx0))) /. x) - ((f * (reproj ((In (i,(dom G))),nx0))) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A24;

now :: thesis: for x being Point of (G . (In (i,(dom G)))) st x in N holds
(((f | Z) * (reproj ((In (i,(dom G))),nx0))) /. x) - (((f | Z) * (reproj ((In (i,(dom G))),nx0))) /. x0) = (L . (x - x0)) + (R /. (x - x0))

let x be Point of (G . (In (i,(dom G)))); :: thesis: ( x in N implies (((f | Z) * (reproj ((In (i,(dom G))),nx0))) /. x) - (((f | Z) * (reproj ((In (i,(dom G))),nx0))) /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
assume A33: x in N ; :: thesis: (((f | Z) * (reproj ((In (i,(dom G))),nx0))) /. x) - (((f | Z) * (reproj ((In (i,(dom G))),nx0))) /. x0) = (L . (x - x0)) + (R /. (x - x0))
then A34: x in N0 by XBOOLE_0:def 4;
A35: dom (reproj ((In (i,(dom G))),nx0)) = the carrier of (G . (In (i,(dom G)))) by FUNCT_2:def 1;
x in N1 by A33, XBOOLE_0:def 4;
then A36: (reproj ((In (i,(dom G))),nx0)) . x in dom (f | Z) by A26;
then A37: (reproj ((In (i,(dom G))),nx0)) . x in (dom f) /\ Z by RELAT_1:61;
then A38: (reproj ((In (i,(dom G))),nx0)) . x in dom f by XBOOLE_0:def 4;
A39: (reproj ((In (i,(dom G))),nx0)) . x0 in dom (f | Z) by A26, NFCONT_1:4;
then A40: (reproj ((In (i,(dom G))),nx0)) . x0 in (dom f) /\ Z by RELAT_1:61;
then A41: (reproj ((In (i,(dom G))),nx0)) . x0 in dom f by XBOOLE_0:def 4;
A42: ((f | Z) * (reproj ((In (i,(dom G))),nx0))) /. x = (f | Z) /. ((reproj ((In (i,(dom G))),nx0)) /. x) by A36, A35, PARTFUN2:4
.= f /. ((reproj ((In (i,(dom G))),nx0)) /. x) by A37, PARTFUN2:16
.= (f * (reproj ((In (i,(dom G))),nx0))) /. x by A35, A38, PARTFUN2:4 ;
((f | Z) * (reproj ((In (i,(dom G))),nx0))) /. x0 = (f | Z) /. ((reproj ((In (i,(dom G))),nx0)) /. x0) by A35, A39, PARTFUN2:4
.= f /. ((reproj ((In (i,(dom G))),nx0)) /. x0) by A40, PARTFUN2:16
.= (f * (reproj ((In (i,(dom G))),nx0))) /. x0 by A35, A41, PARTFUN2:4 ;
hence (((f | Z) * (reproj ((In (i,(dom G))),nx0))) /. x) - (((f | Z) * (reproj ((In (i,(dom G))),nx0))) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A42, A34, A32; :: thesis: verum

end;

hence f | Z is_partial_differentiable_in nx0,i by A31, NDIFF_1:def 6; :: thesis: verum

end;

hence f is_partial_differentiable_on Z,i by A20; :: thesis: verum