let m be non zero Nat; :: thesis: for f being PartFunc of (REAL-NS m),(REAL-NS 1)
for X being Subset of (REAL-NS m) st X is open holds
( ( for i being Nat st 1 <= i & i <= m holds
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) ) iff ( f is_differentiable_on X & f `| X is_continuous_on X ) )
let f be PartFunc of (REAL-NS m),(REAL-NS 1); :: thesis: for X being Subset of (REAL-NS m) st X is open holds
( ( for i being Nat st 1 <= i & i <= m holds
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) ) iff ( f is_differentiable_on X & f `| X is_continuous_on X ) )
let X be Subset of (REAL-NS m); :: thesis: ( X is open implies ( ( for i being Nat st 1 <= i & i <= m holds
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) ) iff ( f is_differentiable_on X & f `| X is_continuous_on X ) ) )
assume A1: X is open ; :: thesis: ( ( for i being Nat st 1 <= i & i <= m holds
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) ) iff ( f is_differentiable_on X & f `| X is_continuous_on X ) )
hereby :: thesis: ( f is_differentiable_on X & f `| X is_continuous_on X implies for i being Nat st 1 <= i & i <= m holds
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) )
assume A2: for i being Nat st 1 <= i & i <= m holds
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) ; :: thesis: ( f is_differentiable_on X & f `| X is_continuous_on X )
A3: now :: thesis: for i being Nat st 1 <= i & i <= m holds
( X c= dom (f `partial| (X,i)) & ( for y0 being Point of (REAL-NS m)
for r being Real st y0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for y1 being Point of (REAL-NS m) st y1 in X & ||.(y1 - y0).|| < s holds
||.(((f `partial| (X,i)) /. y1) - ((f `partial| (X,i)) /. y0)).|| < r ) ) ) )
let i be Nat; :: thesis: ( 1 <= i & i <= m implies ( X c= dom (f `partial| (X,i)) & ( for y0 being Point of (REAL-NS m)
for r being Real st y0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for y1 being Point of (REAL-NS m) st y1 in X & ||.(y1 - y0).|| < s holds
||.(((f `partial| (X,i)) /. y1) - ((f `partial| (X,i)) /. y0)).|| < r ) ) ) ) )
assume ( 1 <= i & i <= m ) ; :: thesis: ( X c= dom (f `partial| (X,i)) & ( for y0 being Point of (REAL-NS m)
for r being Real st y0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for y1 being Point of (REAL-NS m) st y1 in X & ||.(y1 - y0).|| < s holds
||.(((f `partial| (X,i)) /. y1) - ((f `partial| (X,i)) /. y0)).|| < r ) ) ) )
then f `partial| (X,i) is_continuous_on X by A2;
hence ( X c= dom (f `partial| (X,i)) & ( for y0 being Point of (REAL-NS m)
for r being Real st y0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for y1 being Point of (REAL-NS m) st y1 in X & ||.(y1 - y0).|| < s holds
||.(((f `partial| (X,i)) /. y1) - ((f `partial| (X,i)) /. y0)).|| < r ) ) ) ) by NFCONT_1:19; :: thesis: verum
end;
1 <= m by NAT_1:14;
then f is_partial_differentiable_on X,m by A2;
then A4: X c= dom f ;
for x being Point of (REAL-NS m) st x in X holds
f is_differentiable_in x by A1, A2, Th48;
hence A5: f is_differentiable_on X by A1, A4, NDIFF_1:31; :: thesis: f `| X is_continuous_on X
then A6: dom (f `| X) = X by NDIFF_1:def 9;
for y0 being Point of (REAL-NS m)
for r being Real st y0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for y1 being Point of (REAL-NS m) st y1 in X & ||.(y1 - y0).|| < s holds
||.(((f `| X) /. y1) - ((f `| X) /. y0)).|| < r ) )
proof
let y0 be Point of (REAL-NS m); :: thesis: for r being Real st y0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for y1 being Point of (REAL-NS m) st y1 in X & ||.(y1 - y0).|| < s holds
||.(((f `| X) /. y1) - ((f `| X) /. y0)).|| < r ) )
let r be Real; :: thesis: ( y0 in X & 0 < r implies ex s being Real st
( 0 < s & ( for y1 being Point of (REAL-NS m) st y1 in X & ||.(y1 - y0).|| < s holds
||.(((f `| X) /. y1) - ((f `| X) /. y0)).|| < r ) ) )
assume A7: ( y0 in X & 0 < r ) ; :: thesis: ex s being Real st
( 0 < s & ( for y1 being Point of (REAL-NS m) st y1 in X & ||.(y1 - y0).|| < s holds
||.(((f `| X) /. y1) - ((f `| X) /. y0)).|| < r ) )
defpred S1[ Nat, Real] means for i being Nat st i = $1 holds
( 0 < $2 & ( for y1 being Point of (REAL-NS m) st y1 in X & ||.(y1 - y0).|| < $2 holds
||.(((f `partial| (X,i)) /. y1) - ((f `partial| (X,i)) /. y0)).|| < r / (2 * m) ) );
A8: now :: thesis: for i being Nat st i in Seg m holds
ex s being Element of REAL st S1[i,s]
let i be Nat; :: thesis: ( i in Seg m implies ex s being Element of REAL st S1[i,s] )
reconsider j = i as Nat ;
assume i in Seg m ; :: thesis: ex s being Element of REAL st S1[i,s]
then ( 1 <= j & j <= m ) by FINSEQ_1:1;
then consider s being Real such that
A9: ( 0 < s & ( for y1 being Point of (REAL-NS m) st y1 in X & ||.(y1 - y0).|| < s holds
||.(((f `partial| (X,j)) /. y1) - ((f `partial| (X,j)) /. y0)).|| < r / (2 * m) ) ) by A7, A3;
reconsider s = s as Element of REAL by XREAL_0:def 1;
take s = s; :: thesis: S1[i,s]
thus S1[i,s] by A9; :: thesis: verum
end;
consider S being FinSequence of REAL such that
A10: ( dom S = Seg m & ( for i being Nat st i in Seg m holds
S1[i,S . i] ) ) from FINSEQ_1:sch 5(A8);
 take s = min S; :: thesis: ( 0 < s & ( for y1 being Point of (REAL-NS m) st y1 in X & ||.(y1 - y0).|| < s holds
||.(((f `| X) /. y1) - ((f `| X) /. y0)).|| < r ) )
reconsider mm = m as Element of NAT by ORDINAL1:def 12;
A11: len S = mm by A10, FINSEQ_1:def 3;
then ( s = S . (min_p S) & min_p S in dom S ) by RFINSEQ2:def 2, RFINSEQ2:def 4;
hence s > 0 by A10; :: thesis: for y1 being Point of (REAL-NS m) st y1 in X & ||.(y1 - y0).|| < s holds
||.(((f `| X) /. y1) - ((f `| X) /. y0)).|| < r
let y1 be Point of (REAL-NS m); :: thesis: ( y1 in X & ||.(y1 - y0).|| < s implies ||.(((f `| X) /. y1) - ((f `| X) /. y0)).|| < r )
assume A12: ( y1 in X & ||.(y1 - y0).|| < s ) ; :: thesis: ||.(((f `| X) /. y1) - ((f `| X) /. y0)).|| < r
reconsider DD = (diff (f,y1)) - (diff (f,y0)) as Lipschitzian LinearOperator of (REAL-NS m),(REAL-NS 1) by LOPBAN_1:def 9;
A13: upper_bound (PreNorms DD) = ||.((diff (f,y1)) - (diff (f,y0))).|| by LOPBAN_1:30;
now :: thesis: for mt being Real st mt in PreNorms DD holds
mt <= r / 2
let mt be Real; :: thesis: ( mt in PreNorms DD implies mt <= r / 2 )
assume mt in PreNorms DD ; :: thesis: mt <= r / 2
then consider t being VECTOR of (REAL-NS m) such that
A14: ( mt = ||.(DD . t).|| & ||.t.|| <= 1 ) ;
reconsider tt = t as Element of REAL m by REAL_NS1:def 4;
consider w0 being FinSequence of REAL 1 such that
A15: ( dom w0 = Seg m & ( for i being Nat st i in Seg m holds
w0 . i = (partdiff (f,y0,i)) . <*((proj (i,m)) . t)*> ) & (diff (f,y0)) . t = Sum w0 ) by A1, A2, Th48, A7;
reconsider Sw0 = Sum w0 as Point of (REAL-NS 1) by A15;
consider w1 being FinSequence of REAL 1 such that
A16: ( dom w1 = Seg m & ( for i being Nat st i in Seg m holds
w1 . i = (partdiff (f,y1,i)) . <*((proj (i,m)) . t)*> ) & (diff (f,y1)) . t = Sum w1 ) by A1, A2, Th48, A12;
reconsider Sw1 = Sum w1 as Point of (REAL-NS 1) by A16;
deffunc H1( set ) -> Element of REAL 1 = (w1 /. $1) - (w0 /. $1);
consider w2 being FinSequence of REAL 1 such that
A17: ( len w2 = m & ( for i being Nat st i in dom w2 holds
w2 . i = H1(i) ) ) from FINSEQ_2:sch 1();
reconsider mm = m as Element of NAT by ORDINAL1:def 12;
A18: ( len w1 = mm & len w0 = mm ) by A15, A16, FINSEQ_1:def 3;
now :: thesis: for i being Nat st i in dom w2 holds
w2 /. i = H1(i)
let i be Nat; :: thesis: ( i in dom w2 implies w2 /. i = H1(i) )
assume A19: i in dom w2 ; :: thesis: w2 /. i = H1(i)
then w2 . i = H1(i) by A17;
hence w2 /. i = H1(i) by A19, PARTFUN1:def 6; :: thesis: verum
end;
then A20: Sum w2 = (Sum w1) - (Sum w0) by A17, Th27, A18;
DD . t = Sw1 - Sw0 by A16, A15, LOPBAN_1:40
.= Sum w2 by A20, REAL_NS1:5 ;
then A21: mt = |.(Sum w2).| by A14, REAL_NS1:1;
deffunc H2( Nat) -> Element of REAL = In (|.(w2 /. $1).|,REAL);
consider ys being FinSequence of REAL such that
A22: ( len ys = m & ( for j being Nat st j in dom ys holds
ys . j = H2(j) ) ) from FINSEQ_2:sch 1();
A23: now :: thesis: for i being Nat st i in dom w2 holds
ex v being Element of REAL 1 st
( v = w2 . i & ys . i = |.v.| )
let i be Nat; :: thesis: ( i in dom w2 implies ex v being Element of REAL 1 st
( v = w2 . i & ys . i = |.v.| ) )
assume A24: i in dom w2 ; :: thesis: ex v being Element of REAL 1 st
( v = w2 . i & ys . i = |.v.| )
reconsider v = w2 /. i as Element of REAL 1 ;
take v = v; :: thesis: ( v = w2 . i & ys . i = |.v.| )
thus v = w2 . i by A24, PARTFUN1:def 6; :: thesis: ys . i = |.v.|
i in Seg m by A17, A24, FINSEQ_1:def 3;
then i in dom ys by A22, FINSEQ_1:def 3;
then ys . i = H2(i) by A22;
hence ys . i = |.v.| ; :: thesis: verum
end;
then A25: |.(Sum w2).| <= Sum ys by A17, A22, PDIFF_6:17;
reconsider rm = r / (2 * m) as Element of REAL by XREAL_0:def 1;
deffunc H3( Nat) -> Element of REAL = rm;
consider rs being FinSequence of REAL such that
A26: ( len rs = m & ( for j being Nat st j in dom rs holds
rs . j = H3(j) ) ) from FINSEQ_2:sch 1();
A27: dom rs = Seg m by A26, FINSEQ_1:def 3;
rng rs = {rm}
proof
thus rng rs c= {rm} :: according to XBOOLE_0:def 10 :: thesis: {rm} c= rng rs
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in rng rs or a in {rm} )
assume a in rng rs ; :: thesis: a in {rm}
then consider b being object such that
A28: ( b in dom rs & a = rs . b ) by FUNCT_1:def 3;
reconsider b = b as Nat by A28;
rs . b = rm by A28, A26;
hence a in {rm} by A28, TARSKI:def 1; :: thesis: verum
end;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in {rm} or a in rng rs )
assume a in {rm} ; :: thesis: a in rng rs
then A29: a = rm by TARSKI:def 1;
1 <= m by NAT_1:14;
then A30: 1 in dom rs by A27;
then a = rs . 1 by A29, A26;
hence a in rng rs by A30, FUNCT_1:3; :: thesis: verum
end;
then rs = m |-> (r / (2 * m)) by A27, FUNCOP_1:9;
then A31: Sum rs = m * (r / (2 * m)) by RVSUM_1:80
.= m * ((r / 2) / m) by XCMPLX_1:78
.= r / 2 by XCMPLX_1:87 ;
now :: thesis: for i being Element of NAT st i in dom ys holds
ys . i <= rs . i
let i be Element of NAT ; :: thesis: ( i in dom ys implies ys . i <= rs . i )
assume i in dom ys ; :: thesis: ys . i <= rs . i
then A32: i in Seg m by A22, FINSEQ_1:def 3;
then A33: ( i in dom w2 & i in dom w1 & i in dom w0 ) by A15, A16, A17, FINSEQ_1:def 3;
then consider v being Element of REAL 1 such that
A34: ( v = w2 . i & ys . i = |.v.| ) by A23;
A35: i in dom rs by A26, A32, FINSEQ_1:def 3;
reconsider p1 = partdiff (f,y1,i), p0 = partdiff (f,y0,i) as Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS 1) by LOPBAN_1:def 9;
A36: ( dom p1 = the carrier of (REAL-NS 1) & rng p1 c= the carrier of (REAL-NS 1) ) by FUNCT_2:def 1;
(proj (i,m)) . t in REAL by XREAL_0:def 1;
then <*((proj (i,m)) . t)*> in REAL 1 by FINSEQ_2:98;
then <*((proj (i,m)) . t)*> in the carrier of (REAL-NS 1) by REAL_NS1:def 4;
then p1 . <*((proj (i,m)) . t)*> in rng p1 by A36, FUNCT_1:3;
then reconsider P1 = p1 . <*((proj (i,m)) . t)*> as VECTOR of (REAL-NS 1) ;
A37: ( dom p0 = the carrier of (REAL-NS 1) & rng p0 c= the carrier of (REAL-NS 1) ) by FUNCT_2:def 1;
(proj (i,m)) . t in REAL by XREAL_0:def 1;
then <*((proj (i,m)) . t)*> in REAL 1 by FINSEQ_2:98;
then <*((proj (i,m)) . t)*> in the carrier of (REAL-NS 1) by REAL_NS1:def 4;
then p0 . <*((proj (i,m)) . t)*> in rng p0 by A37, FUNCT_1:3;
then reconsider P0 = p0 . <*((proj (i,m)) . t)*> as VECTOR of (REAL-NS 1) ;
A38: w1 /. i = w1 . i by A32, A16, PARTFUN1:def 6
.= P1 by A16, A32 ;
A39: w0 /. i = w0 . i by A32, A15, PARTFUN1:def 6
.= P0 by A15, A32 ;
A40: w2 . i = (w1 /. i) - (w0 /. i) by A33, A17
.= P1 - P0 by A39, A38, REAL_NS1:5 ;
( 1 <= i & i <= len S ) by A11, A32, FINSEQ_1:1;
then A41: ( s <= S . i & f is_partial_differentiable_on X,i ) by A11, A2, RFINSEQ2:2;
then ||.(y1 - y0).|| < S . i by A12, XXREAL_0:2;
then ||.(((f `partial| (X,i)) /. y1) - ((f `partial| (X,i)) /. y0)).|| < r / (2 * m) by A10, A32, A12;
then ||.((partdiff (f,y1,i)) - ((f `partial| (X,i)) /. y0)).|| < r / (2 * m) by A12, A41, PDIFF_1:def 20;
then A42: ||.((partdiff (f,y1,i)) - (partdiff (f,y0,i))).|| < r / (2 * m) by A7, A41, PDIFF_1:def 20;
reconsider PP = (partdiff (f,y1,i)) - (partdiff (f,y0,i)) as Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS 1) by LOPBAN_1:def 9;
A43: upper_bound (PreNorms PP) = ||.((partdiff (f,y1,i)) - (partdiff (f,y0,i))).|| by LOPBAN_1:30;
(proj (i,m)) . t in REAL by XREAL_0:def 1;
then <*((proj (i,m)) . t)*> in REAL 1 by FINSEQ_2:98;
then reconsider pt = <*((proj (i,m)) . t)*> as VECTOR of (REAL-NS 1) by REAL_NS1:def 4;
A44: PP . pt = P1 - P0 by LOPBAN_1:40;
(proj (i,m)) . t in REAL by XREAL_0:def 1;
then reconsider pt1 = <*((proj (i,m)) . t)*> as Element of REAL 1 by FINSEQ_2:98;
reconsider p2 = ((proj (i,m)) . t) ^2 as Real ;
A45: ||.pt.|| = |.pt1.| by REAL_NS1:1
.= sqrt (Sum <*p2*>) by RVSUM_1:55
.= sqrt (((proj (i,m)) . t) ^2) by RVSUM_1:73 ;
A46: ((proj (i,m)) . t) ^2 >= 0
proof
per cases ( (proj (i,m)) . t = 0 or (proj (i,m)) . t <> 0 ) ;
suppose (proj (i,m)) . t = 0 ; :: thesis: ((proj (i,m)) . t) ^2 >= 0
hence ((proj (i,m)) . t) ^2 >= 0 ; :: thesis: verum
end;
suppose (proj (i,m)) . t <> 0 ; :: thesis: ((proj (i,m)) . t) ^2 >= 0
hence ((proj (i,m)) . t) ^2 >= 0 by SQUARE_1:12; :: thesis: verum
end;
end;
end;
now :: thesis: not ||.pt.|| > 1
assume ||.pt.|| > 1 ; :: thesis: contradiction
then ((proj (i,m)) . t) ^2 > 1 by A45, A46, SQUARE_1:18, SQUARE_1:26;
then A47: (tt . i) ^2 > 1 by PDIFF_1:def 1;
|.tt.| <= 1 by A14, REAL_NS1:1;
then A48: Sum (sqr tt) <= 1 by SQUARE_1:18, SQUARE_1:27;
len tt = m by CARD_1:def 7;
then i in dom tt by A32, FINSEQ_1:def 3;
then A49: i in dom (sqr tt) by RVSUM_1:143;
now :: thesis: for k being Element of NAT st k in dom (sqr tt) holds
(sqr tt) . k >= 0
let k be Element of NAT ; :: thesis: ( k in dom (sqr tt) implies (sqr tt) . b1 >= 0 )
assume k in dom (sqr tt) ; :: thesis: (sqr tt) . b1 >= 0
A50: (sqr tt) . k = (tt . k) ^2 by VALUED_1:11;
per cases ( tt . k = 0 or tt . k <> 0 ) ;
suppose tt . k = 0 ; :: thesis: (sqr tt) . b1 >= 0
hence (sqr tt) . k >= 0 by A50; :: thesis: verum
end;
suppose tt . k <> 0 ; :: thesis: (sqr tt) . b1 >= 0
hence (sqr tt) . k >= 0 by A50, SQUARE_1:12; :: thesis: verum
end;
end;
end;
then Sum (sqr tt) >= (sqr tt) . i by A49, POLYNOM5:4;
then Sum (sqr tt) >= (tt . i) ^2 by VALUED_1:11;
hence contradiction by A47, A48, XXREAL_0:2; :: thesis: verum
end;
then ( ||.(PP . pt).|| in PreNorms PP & not PreNorms PP is empty & PreNorms PP is bounded_above ) by LOPBAN_1:27;
then ||.(PP . pt).|| <= upper_bound (PreNorms PP) by SEQ_4:def 1;
then ||.(P1 - P0).|| <= r / (2 * m) by A44, A42, A43, XXREAL_0:2;
then |.v.| <= r / (2 * m) by A34, A40, REAL_NS1:1;
hence ys . i <= rs . i by A34, A26, A35; :: thesis: verum
end;
then Sum ys <= r / 2 by A31, A26, A22, INTEGRA5:3;
hence mt <= r / 2 by A21, A25, XXREAL_0:2; :: thesis: verum
end;
then A51: ( ||.((diff (f,y1)) - (diff (f,y0))).|| <= r / 2 & r / 2 < r ) by A13, A7, SEQ_4:45, XREAL_1:216;
||.(((f `| X) /. y1) - ((f `| X) /. y0)).|| = ||.((diff (f,y1)) - ((f `| X) /. y0)).|| by A5, A12, NDIFF_1:def 9
.= ||.((diff (f,y1)) - (diff (f,y0))).|| by A5, A7, NDIFF_1:def 9 ;
hence ||.(((f `| X) /. y1) - ((f `| X) /. y0)).|| < r by A51, XXREAL_0:2; :: thesis: verum
end;
hence f `| X is_continuous_on X by A6, NFCONT_1:19; :: thesis: verum
end;
assume A52: ( f is_differentiable_on X & f `| X is_continuous_on X ) ; :: thesis: for i being Nat st 1 <= i & i <= m holds
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X )
then A53: ( X c= dom f & ( for x being Point of (REAL-NS m) st x in X holds
f is_differentiable_in x ) ) by A1, NDIFF_1:31;
thus for i being Nat st 1 <= i & i <= m holds
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) :: thesis: verum
proof
let i be Nat; :: thesis: ( 1 <= i & i <= m implies ( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) )
assume A54: ( 1 <= i & i <= m ) ; :: thesis: ( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X )
now :: thesis: for x being Point of (REAL-NS m) st x in X holds
( f is_partial_differentiable_in x,i & partdiff (f,x,i) = (diff (f,x)) * (reproj (i,(0. (REAL-NS m)))) )
let x be Point of (REAL-NS m); :: thesis: ( x in X implies ( f is_partial_differentiable_in x,i & partdiff (f,x,i) = (diff (f,x)) * (reproj (i,(0. (REAL-NS m)))) ) )
assume x in X ; :: thesis: ( f is_partial_differentiable_in x,i & partdiff (f,x,i) = (diff (f,x)) * (reproj (i,(0. (REAL-NS m)))) )
then f is_differentiable_in x by A52, A1, NDIFF_1:31;
hence ( f is_partial_differentiable_in x,i & partdiff (f,x,i) = (diff (f,x)) * (reproj (i,(0. (REAL-NS m)))) ) by A54, Th21; :: thesis: verum
end;
then for x being Point of (REAL-NS m) st x in X holds
f is_partial_differentiable_in x,i ;
hence A55: f is_partial_differentiable_on X,i by A1, A54, Th8, A53; :: thesis: f `partial| (X,i) is_continuous_on X
then A56: dom (f `partial| (X,i)) = X by PDIFF_1:def 20;
for y0 being Point of (REAL-NS m)
for r being Real st y0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for y1 being Point of (REAL-NS m) st y1 in X & ||.(y1 - y0).|| < s holds
||.(((f `partial| (X,i)) /. y1) - ((f `partial| (X,i)) /. y0)).|| < r ) )
proof
let y0 be Point of (REAL-NS m); :: thesis: for r being Real st y0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for y1 being Point of (REAL-NS m) st y1 in X & ||.(y1 - y0).|| < s holds
||.(((f `partial| (X,i)) /. y1) - ((f `partial| (X,i)) /. y0)).|| < r ) )
let r be Real; :: thesis: ( y0 in X & 0 < r implies ex s being Real st
( 0 < s & ( for y1 being Point of (REAL-NS m) st y1 in X & ||.(y1 - y0).|| < s holds
||.(((f `partial| (X,i)) /. y1) - ((f `partial| (X,i)) /. y0)).|| < r ) ) )
assume A57: ( y0 in X & 0 < r ) ; :: thesis: ex s being Real st
( 0 < s & ( for y1 being Point of (REAL-NS m) st y1 in X & ||.(y1 - y0).|| < s holds
||.(((f `partial| (X,i)) /. y1) - ((f `partial| (X,i)) /. y0)).|| < r ) )
then consider s being Real such that
A58: ( 0 < s & ( for y1 being Point of (REAL-NS m) st y1 in X & ||.(y1 - y0).|| < s holds
||.(((f `| X) /. y1) - ((f `| X) /. y0)).|| < r ) ) by A52, NFCONT_1:19;
take s ; :: thesis: ( 0 < s & ( for y1 being Point of (REAL-NS m) st y1 in X & ||.(y1 - y0).|| < s holds
||.(((f `partial| (X,i)) /. y1) - ((f `partial| (X,i)) /. y0)).|| < r ) )
thus 0 < s by A58; :: thesis: for y1 being Point of (REAL-NS m) st y1 in X & ||.(y1 - y0).|| < s holds
||.(((f `partial| (X,i)) /. y1) - ((f `partial| (X,i)) /. y0)).|| < r
let y1 be Point of (REAL-NS m); :: thesis: ( y1 in X & ||.(y1 - y0).|| < s implies ||.(((f `partial| (X,i)) /. y1) - ((f `partial| (X,i)) /. y0)).|| < r )
assume A59: ( y1 in X & ||.(y1 - y0).|| < s ) ; :: thesis: ||.(((f `partial| (X,i)) /. y1) - ((f `partial| (X,i)) /. y0)).|| < r
then ||.(((f `| X) /. y1) - ((f `| X) /. y0)).|| < r by A58;
then ||.((diff (f,y1)) - ((f `| X) /. y0)).|| < r by A59, A52, NDIFF_1:def 9;
then A60: ||.((diff (f,y1)) - (diff (f,y0))).|| < r by A57, A52, NDIFF_1:def 9;
( f is_differentiable_in y1 & f is_differentiable_in y0 ) by A52, A1, A59, A57, NDIFF_1:31;
then A61: ( partdiff (f,y1,i) = (diff (f,y1)) * (reproj (i,(0. (REAL-NS m)))) & partdiff (f,y0,i) = (diff (f,y0)) * (reproj (i,(0. (REAL-NS m)))) ) by Th21, A54;
reconsider PP = (partdiff (f,y1,i)) - (partdiff (f,y0,i)) as Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS 1) by LOPBAN_1:def 9;
reconsider DD = (diff (f,y1)) - (diff (f,y0)) as Lipschitzian LinearOperator of (REAL-NS m),(REAL-NS 1) by LOPBAN_1:def 9;
A62: upper_bound (PreNorms PP) = ||.((partdiff (f,y1,i)) - (partdiff (f,y0,i))).|| by LOPBAN_1:30;
A63: upper_bound (PreNorms DD) = ||.((diff (f,y1)) - (diff (f,y0))).|| by LOPBAN_1:30;
A64: ( PreNorms PP is bounded_above & PreNorms DD is bounded_above ) by LOPBAN_1:28;
PreNorms PP c= PreNorms DD
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in PreNorms PP or a in PreNorms DD )
assume a in PreNorms PP ; :: thesis: a in PreNorms DD
then consider t being VECTOR of (REAL-NS 1) such that
A65: ( a = ||.(PP . t).|| & ||.t.|| <= 1 ) ;
A66: dom (reproj (i,(0. (REAL-NS m)))) = the carrier of (REAL-NS 1) by FUNCT_2:def 1;
set tm = (reproj (i,(0. (REAL-NS m)))) . t;
A67: ||.((reproj (i,(0. (REAL-NS m)))) . t).|| <= 1 by A65, Th5, A54;
A68: (partdiff (f,y1,i)) . t = (diff (f,y1)) . ((reproj (i,(0. (REAL-NS m)))) . t) by A66, A61, FUNCT_1:13;
(partdiff (f,y0,i)) . t = (diff (f,y0)) . ((reproj (i,(0. (REAL-NS m)))) . t) by A66, A61, FUNCT_1:13;
then ||.(PP . t).|| = ||.(((diff (f,y1)) . ((reproj (i,(0. (REAL-NS m)))) . t)) - ((diff (f,y0)) . ((reproj (i,(0. (REAL-NS m)))) . t))).|| by A68, LOPBAN_1:40
.= ||.(DD . ((reproj (i,(0. (REAL-NS m)))) . t)).|| by LOPBAN_1:40 ;
hence a in PreNorms DD by A65, A67; :: thesis: verum
end;
then ||.((partdiff (f,y1,i)) - (partdiff (f,y0,i))).|| <= ||.((diff (f,y1)) - (diff (f,y0))).|| by A64, A62, A63, SEQ_4:48;
then ||.((partdiff (f,y1,i)) - (partdiff (f,y0,i))).|| < r by A60, XXREAL_0:2;
then ||.((partdiff (f,y1,i)) - ((f `partial| (X,i)) /. y0)).|| < r by A57, A55, PDIFF_1:def 20;
hence ||.(((f `partial| (X,i)) /. y1) - ((f `partial| (X,i)) /. y0)).|| < r by A59, A55, PDIFF_1:def 20; :: thesis: verum
end;
hence f `partial| (X,i) is_continuous_on X by A56, NFCONT_1:19; :: thesis: verum
end;