let m be non empty Element of NAT ; :: thesis: for i being Element of NAT
for X being Subset of (REAL m)
for f being PartFunc of (REAL m),REAL st X is open & 1 <= i & i <= m holds
( f is_partial_differentiable_on X,i iff ( X c= dom f & ( for x being Element of REAL m st x in X holds
f is_partial_differentiable_in x,i ) ) )
let i be Element of NAT ; :: thesis: for X being Subset of (REAL m)
for f being PartFunc of (REAL m),REAL st X is open & 1 <= i & i <= m holds
( f is_partial_differentiable_on X,i iff ( X c= dom f & ( for x being Element of REAL m st x in X holds
f is_partial_differentiable_in x,i ) ) )
let X be Subset of (REAL m); :: thesis: for f being PartFunc of (REAL m),REAL st X is open & 1 <= i & i <= m holds
( f is_partial_differentiable_on X,i iff ( X c= dom f & ( for x being Element of REAL m st x in X holds
f is_partial_differentiable_in x,i ) ) )
let f be PartFunc of (REAL m),REAL; :: thesis: ( X is open & 1 <= i & i <= m implies ( f is_partial_differentiable_on X,i iff ( X c= dom f & ( for x being Element of REAL m st x in X holds
f is_partial_differentiable_in x,i ) ) ) )
assume that
A1: X is open and
A2: ( 1 <= i & i <= m ) ; :: thesis: ( f is_partial_differentiable_on X,i iff ( X c= dom f & ( for x being Element of REAL m st x in X holds
f is_partial_differentiable_in x,i ) ) )
thus ( f is_partial_differentiable_on X,i implies ( X c= dom f & ( for x being Element of REAL m st x in X holds
f is_partial_differentiable_in x,i ) ) ) :: thesis: ( X c= dom f & ( for x being Element of REAL m st x in X holds
f is_partial_differentiable_in x,i ) implies f is_partial_differentiable_on X,i )

proof

assume A3: f is_partial_differentiable_on X,i ; :: thesis: ( X c= dom f & ( for x being Element of REAL m st x in X holds
f is_partial_differentiable_in x,i ) )
hence A4: X c= dom f by CWDef19; :: thesis: for x being Element of REAL m st x in X holds
f is_partial_differentiable_in x,i
let nx0 be Element of REAL m; :: thesis: ( nx0 in X implies f is_partial_differentiable_in nx0,i )
reconsider x0 = (proj (i,m)) . nx0 as Element of REAL ;
assume A5: nx0 in X ; :: thesis: f is_partial_differentiable_in nx0,i
then f | X is_partial_differentiable_in nx0,i by A3, CWDef19;
then (f | X) * (reproj (i,nx0)) is_differentiable_in x0 by PDIFF_1:def 11;
then consider N0 being Neighbourhood of x0 such that
A6: N0 c= dom ((f | X) * (reproj (i,nx0))) and
A7: ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N0 holds
(((f | X) * (reproj (i,nx0))) . x) - (((f | X) * (reproj (i,nx0))) . x0) = (L . (x - x0)) + (R . (x - x0)) by FDIFF_1:def 4;
consider L being LinearFunc, R being RestFunc such that
A8: for x being Element of REAL st x in N0 holds
(((f | X) * (reproj (i,nx0))) . x) - (((f | X) * (reproj (i,nx0))) . x0) = (L . (x - x0)) + (R . (x - x0)) by A7;
consider N1 being Neighbourhood of x0 such that
A9: for x being Element of REAL st x in N1 holds
(reproj (i,nx0)) . x in X by A1, A2, A5, Lm5;

A10: now :: thesis: for x being Element of REAL st x in N1 holds
(reproj (i,nx0)) . x in dom (f | X)

let x be Element of REAL ; :: thesis: ( x in N1 implies (reproj (i,nx0)) . x in dom (f | X) )
assume x in N1 ; :: thesis: (reproj (i,nx0)) . x in dom (f | X)
then (reproj (i,nx0)) . x in X by A9;
then (reproj (i,nx0)) . x in (dom f) /\ X by A4, XBOOLE_0:def 4;
hence (reproj (i,nx0)) . x in dom (f | X) by RELAT_1:61; :: thesis: verum

end;

consider N being Neighbourhood of x0 such that
NXX: ( N c= N0 & N c= N1 ) by RCOMP_1:17;
(f | X) * (reproj (i,nx0)) c= f * (reproj (i,nx0)) by RELAT_1:29, RELAT_1:59;
then A11: dom ((f | X) * (reproj (i,nx0))) c= dom (f * (reproj (i,nx0))) by RELAT_1:11;
N c= dom ((f | X) * (reproj (i,nx0))) by A6, NXX, XBOOLE_1:1;
then A12: N c= dom (f * (reproj (i,nx0))) by A11, XBOOLE_1:1;

now :: thesis: for x being Element of REAL st x in N holds
((f * (reproj (i,nx0))) . x) - ((f * (reproj (i,nx0))) . x0) = (L . (x - x0)) + (R . (x - x0))

let x be Element of REAL ; :: thesis: ( x in N implies ((f * (reproj (i,nx0))) . x) - ((f * (reproj (i,nx0))) . x0) = (L . (x - x0)) + (R . (x - x0)) )
assume A13: x in N ; :: thesis: ((f * (reproj (i,nx0))) . x) - ((f * (reproj (i,nx0))) . x0) = (L . (x - x0)) + (R . (x - x0))
then (reproj (i,nx0)) . x in dom (f | X) by A10, NXX;
then A17: ( (reproj (i,nx0)) . x in dom f & (reproj (i,nx0)) . x in X ) by RELAT_1:57;
(reproj (i,nx0)) . x0 in dom (f | X) by A10, RCOMP_1:16;
then A19: ( (reproj (i,nx0)) . x0 in dom f & (reproj (i,nx0)) . x0 in X ) by RELAT_1:57;
A15: dom (reproj (i,nx0)) = REAL by FUNCT_2:def 1;
then A20: ((f | X) * (reproj (i,nx0))) . x = (f | X) . ((reproj (i,nx0)) . x) by FUNCT_1:13
.= f . ((reproj (i,nx0)) . x) by A17, FUNCT_1:49
.= (f * (reproj (i,nx0))) . x by A15, FUNCT_1:13 ;
((f | X) * (reproj (i,nx0))) . x0 = (f | X) . ((reproj (i,nx0)) . x0) by A15, FUNCT_1:13
.= f . ((reproj (i,nx0)) . x0) by A19, FUNCT_1:49
.= (f * (reproj (i,nx0))) . x0 by A15, FUNCT_1:13 ;
hence ((f * (reproj (i,nx0))) . x) - ((f * (reproj (i,nx0))) . x0) = (L . (x - x0)) + (R . (x - x0)) by A8, A13, NXX, A20; :: thesis: verum

end;

then f * (reproj (i,nx0)) is_differentiable_in x0 by A12, FDIFF_1:def 4;
hence f is_partial_differentiable_in nx0,i by PDIFF_1:def 11; :: thesis: verum

end;

assume that
A21: X c= dom f and
A22: for nx being Element of REAL m st nx in X holds
f is_partial_differentiable_in nx,i ; :: thesis: f is_partial_differentiable_on X,i
thus X c= dom f by A21; :: according to PDIFF_9:def 5 :: thesis: for x being Element of REAL m st x in X holds
f | X is_partial_differentiable_in x,i

now :: thesis: for nx0 being Element of REAL m st nx0 in X holds
f | X is_partial_differentiable_in nx0,i

let nx0 be Element of REAL m; :: thesis: ( nx0 in X implies f | X is_partial_differentiable_in nx0,i )
assume A23: nx0 in X ; :: thesis: f | X is_partial_differentiable_in nx0,i
then A24: f is_partial_differentiable_in nx0,i by A22;
reconsider x0 = (proj (i,m)) . nx0 as Element of REAL ;
f * (reproj (i,nx0)) is_differentiable_in x0 by A24, PDIFF_1:def 11;
then consider N0 being Neighbourhood of x0 such that
N0 c= dom (f * (reproj (i,nx0))) and
A25: ex L being LinearFunc ex R being RestFunc st
for x being Element of REAL st x in N0 holds
((f * (reproj (i,nx0))) . x) - ((f * (reproj (i,nx0))) . x0) = (L . (x - x0)) + (R . (x - x0)) by FDIFF_1:def 4;
consider N1 being Neighbourhood of x0 such that
A26: for x being Element of REAL st x in N1 holds
(reproj (i,nx0)) . x in X by A1, A2, A23, Lm5;

A27: now :: thesis: for x being Element of REAL st x in N1 holds
(reproj (i,nx0)) . x in dom (f | X)

let x be Element of REAL ; :: thesis: ( x in N1 implies (reproj (i,nx0)) . x in dom (f | X) )
assume x in N1 ; :: thesis: (reproj (i,nx0)) . x in dom (f | X)
then (reproj (i,nx0)) . x in X by A26;
then (reproj (i,nx0)) . x in (dom f) /\ X by A21, XBOOLE_0:def 4;
hence (reproj (i,nx0)) . x in dom (f | X) by RELAT_1:61; :: thesis: verum

end;

A28: N1 c= dom ((f | X) * (reproj (i,nx0)))

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in N1 or z in dom ((f | X) * (reproj (i,nx0))) )
assume A29: z in N1 ; :: thesis: z in dom ((f | X) * (reproj (i,nx0)))
then A30: z in REAL ;
reconsider x = z as Element of REAL by A29;
A31: (reproj (i,nx0)) . x in dom (f | X) by A29, A27;
z in dom (reproj (i,nx0)) by A30, FUNCT_2:def 1;
hence z in dom ((f | X) * (reproj (i,nx0))) by A31, FUNCT_1:11; :: thesis: verum

end;

consider N being Neighbourhood of x0 such that
NXX: ( N c= N0 & N c= N1 ) by RCOMP_1:17;
A32: N c= dom ((f | X) * (reproj (i,nx0))) by NXX, A28, XBOOLE_1:1;
consider L being LinearFunc, R being RestFunc such that
A33: for x being Element of REAL st x in N0 holds
((f * (reproj (i,nx0))) . x) - ((f * (reproj (i,nx0))) . x0) = (L . (x - x0)) + (R . (x - x0)) by A25;

now :: thesis: for x being Element of REAL st x in N holds
(((f | X) * (reproj (i,nx0))) . x) - (((f | X) * (reproj (i,nx0))) . x0) = (L . (x - x0)) + (R . (x - x0))

let x be Element of REAL ; :: thesis: ( x in N implies (((f | X) * (reproj (i,nx0))) . x) - (((f | X) * (reproj (i,nx0))) . x0) = (L . (x - x0)) + (R . (x - x0)) )
assume A34: x in N ; :: thesis: (((f | X) * (reproj (i,nx0))) . x) - (((f | X) * (reproj (i,nx0))) . x0) = (L . (x - x0)) + (R . (x - x0))
A36: dom (reproj (i,nx0)) = REAL by FUNCT_2:def 1;
(reproj (i,nx0)) . x in dom (f | X) by A27, A34, NXX;
then A38: (reproj (i,nx0)) . x in (dom f) /\ X by RELAT_1:61;
(reproj (i,nx0)) . x0 in dom (f | X) by A27, RCOMP_1:16;
then A41: (reproj (i,nx0)) . x0 in (dom f) /\ X by RELAT_1:61;
A43: ((f | X) * (reproj (i,nx0))) . x = (f | X) . ((reproj (i,nx0)) /. x) by A36, FUNCT_1:13
.= f . ((reproj (i,nx0)) . x) by A38, FUNCT_1:48
.= (f * (reproj (i,nx0))) . x by A36, FUNCT_1:13 ;
((f | X) * (reproj (i,nx0))) . x0 = (f | X) . ((reproj (i,nx0)) . x0) by A36, FUNCT_1:13
.= f . ((reproj (i,nx0)) . x0) by A41, FUNCT_1:48
.= (f * (reproj (i,nx0))) . x0 by A36, FUNCT_1:13 ;
hence (((f | X) * (reproj (i,nx0))) . x) - (((f | X) * (reproj (i,nx0))) . x0) = (L . (x - x0)) + (R . (x - x0)) by A43, A34, A33, NXX; :: thesis: verum

end;

then (f | X) * (reproj (i,nx0)) is_differentiable_in x0 by A32, FDIFF_1:def 4;
hence f | X is_partial_differentiable_in nx0,i by PDIFF_1:def 11; :: thesis: verum

end;

hence for x being Element of REAL m st x in X holds
f | X is_partial_differentiable_in x,i ; :: thesis: verum