:: PDIFF_8 semantic presentation

begin

theorem Th1: :: PDIFF_8:1
for n, i being Element of NAT
for q being Element of REAL n
for p being Point of (TOP-REAL n) st i in Seg n & q = p holds
abs (p /. i) <= |.q.|
proof
let n, i be Element of NAT ; ::_thesis: for q being Element of REAL n
for p being Point of (TOP-REAL n) st i in Seg n & q = p holds
abs (p /. i) <= |.q.|
let q be Element of REAL n; ::_thesis: for p being Point of (TOP-REAL n) st i in Seg n & q = p holds
abs (p /. i) <= |.q.|
let p be Point of (TOP-REAL n); ::_thesis: ( i in Seg n & q = p implies abs (p /. i) <= |.q.| )
assume that
A1: i in Seg n and
A2: q = p ; ::_thesis: abs (p /. i) <= |.q.|
A3: Sum ((0* n) +* (i,((p /. i) ^2))) = (p /. i) ^2 by A1, JORDAN2B:10;
 len (0* n) = n by CARD_1:def_7;
then  len ((0* n) +* (i,((p /. i) ^2))) = n by FUNCT_7:97;
then reconsider w1 = (0* n) +* (i,((p /. i) ^2)) as Element of n -tuples_on REAL by FINSEQ_2:92;
A4: len w1 = n by CARD_1:def_7;
reconsider w2 = sqr q as Element of n -tuples_on REAL ;
A5: Sum (sqr q) >= 0 by RVSUM_1:86;
A6: len q = n by CARD_1:def_7;
 for j being Nat st j in Seg n holds
w1 . j <= w2 . j
proof
let j be Nat; ::_thesis: ( j in Seg n implies w1 . j <= w2 . j )
assume A7: j in Seg n ; ::_thesis: w1 . j <= w2 . j
set r1 = w1 . j;
set r2 = w2 . j;
percases ( j = i or j <> i ) ;
supposeA8: j = i ; ::_thesis: w1 . j <= w2 . j
then  j in dom q by A1, A6, FINSEQ_1:def_3;
then A9: q /. j = q . j by PARTFUN1:def_6;
A10: dom (0* n) = Seg (len (0* n)) by FINSEQ_1:def_3
.= Seg n by CARD_1:def_7 ;
 i in dom w1 by A1, A4, FINSEQ_1:def_3;
then w1 . j = w1 /. i by A8, PARTFUN1:def_6
.= (q /. i) ^2 by A2, A1, A10, FUNCT_7:36 ;
hence  w1 . j <= w2 . j by A8, A9, VALUED_1:11; ::_thesis: verum
end;
supposeA11: j <> i ; ::_thesis: w1 . j <= w2 . j
A12: dom (0* n) = Seg (len (0* n)) by FINSEQ_1:def_3
.= Seg n by CARD_1:def_7 ;
 dom q = Seg n by A6, FINSEQ_1:def_3;
then  q /. j = q . j by A7, PARTFUN1:def_6;
then A13: w2 . j = (q /. j) ^2 by VALUED_1:11;
 j in dom w1 by A4, A7, FINSEQ_1:def_3;
then w1 . j = w1 /. j by PARTFUN1:def_6
.= (0* n) /. j by A7, A11, A12, FUNCT_7:37
.= (n |-> 0) . j by A7, A12, PARTFUN1:def_6
.= 0 ;
hence  w1 . j <= w2 . j by A13, XREAL_1:63; ::_thesis: verum
end;
end;
end;
then  Sum w1 <= Sum w2 by RVSUM_1:82;
then  ( 0 <= (p /. i) ^2 & (p /. i) ^2 <= (sqrt (Sum (sqr q))) ^2 ) by A5, A3, SQUARE_1:def_2, XREAL_1:63;
then  sqrt ((p /. i) ^2) <= sqrt ((sqrt (Sum (sqr q))) ^2) by SQUARE_1:26;
then  abs (abs (p /. i)) <= sqrt ((sqrt (Sum (sqr q))) ^2) by COMPLEX1:72;
then  ( 0 <= |.q.| & abs (p /. i) <= abs (sqrt (Sum (sqr q))) ) by COMPLEX1:72;
hence  abs (p /. i) <= |.q.| by ABSVALUE:def_1; ::_thesis: verum
end;

theorem Th2: :: PDIFF_8:2
for x being Real
for vx being Element of (REAL-NS 1) st vx = <*x*> holds
||.vx.|| = abs x
proof
let x be Real; ::_thesis: for vx being Element of (REAL-NS 1) st vx = <*x*> holds
||.vx.|| = abs x
let vx be Element of (REAL-NS 1); ::_thesis: ( vx = <*x*> implies ||.vx.|| = abs x )
reconsider xx = vx as Element of REAL 1 by REAL_NS1:def_4;
assume  vx = <*x*> ; ::_thesis: ||.vx.|| = abs x
then  sqrt (Sum (sqr xx)) = sqrt (Sum <*(x ^2)*>) by RVSUM_1:55;
then A1: sqrt (Sum (sqr xx)) = sqrt (x ^2) by RVSUM_1:73;
 ||.vx.|| = |.xx.| by REAL_NS1:1;
hence  ||.vx.|| = abs x by A1, COMPLEX1:72; ::_thesis: verum
end;

theorem Th3: :: PDIFF_8:3
for n being non empty Element of NAT
for x being Point of (REAL-NS n)
for i being Element of NAT st 1 <= i & i <= n holds
||.((Proj (i,n)) . x).|| <= ||.x.||
proof
let n be non empty Element of NAT ; ::_thesis: for x being Point of (REAL-NS n)
for i being Element of NAT st 1 <= i & i <= n holds
||.((Proj (i,n)) . x).|| <= ||.x.||
let x be Point of (REAL-NS n); ::_thesis: for i being Element of NAT st 1 <= i & i <= n holds
||.((Proj (i,n)) . x).|| <= ||.x.||
let i be Element of NAT ; ::_thesis: ( 1 <= i & i <= n implies ||.((Proj (i,n)) . x).|| <= ||.x.|| )
assume A1: ( 1 <= i & i <= n ) ; ::_thesis: ||.((Proj (i,n)) . x).|| <= ||.x.||
reconsider y = x as Element of REAL n by REAL_NS1:def_4;
A2: ||.x.|| = |.y.| by REAL_NS1:1;
(Proj (i,n)) . x = <*((proj (i,n)) . x)*> by PDIFF_1:def_4
.= <*(y . i)*> by PDIFF_1:def_1 ;
then A3: ||.((Proj (i,n)) . x).|| = abs (y . i) by Th2;
reconsider p = y as Element of (TOP-REAL n) by EUCLID:22;
A4: i in Seg n by A1;
then A5: abs (p /. i) <= |.y.| by Th1;
 i in dom y by A4, FINSEQ_1:89;
hence  ||.((Proj (i,n)) . x).|| <= ||.x.|| by A2, A3, A5, PARTFUN1:def_6; ::_thesis: verum
end;

theorem Th4: :: PDIFF_8:4
for n being non empty Element of NAT
for x being Element of (REAL-NS n)
for i being Element of NAT holds ||.((Proj (i,n)) . x).|| = |.((proj (i,n)) . x).|
proof
let n be non empty Element of NAT ; ::_thesis: for x being Element of (REAL-NS n)
for i being Element of NAT holds ||.((Proj (i,n)) . x).|| = |.((proj (i,n)) . x).|
let x be Element of (REAL-NS n); ::_thesis: for i being Element of NAT holds ||.((Proj (i,n)) . x).|| = |.((proj (i,n)) . x).|
let i be Element of NAT ; ::_thesis: ||.((Proj (i,n)) . x).|| = |.((proj (i,n)) . x).|
reconsider y = x as Element of REAL n by REAL_NS1:def_4;
(Proj (i,n)) . x = <*((proj (i,n)) . x)*> by PDIFF_1:def_4
.= <*(y . i)*> by PDIFF_1:def_1 ;
then  ||.((Proj (i,n)) . x).|| = abs (y . i) by Th2;
hence  ||.((Proj (i,n)) . x).|| = |.((proj (i,n)) . x).| by PDIFF_1:def_1; ::_thesis: verum
end;

theorem :: PDIFF_8:5
for n being non empty Element of NAT
for x being Element of REAL n
for i being Element of NAT st 1 <= i & i <= n holds
|.((proj (i,n)) . x).| <= |.x.|
proof
let n be non empty Element of NAT ; ::_thesis: for x being Element of REAL n
for i being Element of NAT st 1 <= i & i <= n holds
|.((proj (i,n)) . x).| <= |.x.|
let x be Element of REAL n; ::_thesis: for i being Element of NAT st 1 <= i & i <= n holds
|.((proj (i,n)) . x).| <= |.x.|
let i be Element of NAT ; ::_thesis: ( 1 <= i & i <= n implies |.((proj (i,n)) . x).| <= |.x.| )
assume A1: ( 1 <= i & i <= n ) ; ::_thesis: |.((proj (i,n)) . x).| <= |.x.|
reconsider y = x as Element of (REAL-NS n) by REAL_NS1:def_4;
A2: ||.((Proj (i,n)) . y).|| = |.((proj (i,n)) . y).| by Th4;
 ||.((Proj (i,n)) . y).|| <= ||.y.|| by A1, Th3;
hence  |.((proj (i,n)) . x).| <= |.x.| by A2, REAL_NS1:1; ::_thesis: verum
end;

theorem Th6: :: PDIFF_8:6
for m, n being non empty Element of NAT
for s being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))
for i being Element of NAT st 1 <= i & i <= n holds
( Proj (i,n) is Lipschitzian LinearOperator of (REAL-NS n),(REAL-NS 1) & (BoundedLinearOperatorsNorm ((REAL-NS n),(REAL-NS 1))) . (Proj (i,n)) <= 1 )
proof
let m, n be non empty Element of NAT ; ::_thesis: for s being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))
for i being Element of NAT st 1 <= i & i <= n holds
( Proj (i,n) is Lipschitzian LinearOperator of (REAL-NS n),(REAL-NS 1) & (BoundedLinearOperatorsNorm ((REAL-NS n),(REAL-NS 1))) . (Proj (i,n)) <= 1 )
let s be Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))); ::_thesis: for i being Element of NAT st 1 <= i & i <= n holds
( Proj (i,n) is Lipschitzian LinearOperator of (REAL-NS n),(REAL-NS 1) & (BoundedLinearOperatorsNorm ((REAL-NS n),(REAL-NS 1))) . (Proj (i,n)) <= 1 )
let i be Element of NAT ; ::_thesis: ( 1 <= i & i <= n implies ( Proj (i,n) is Lipschitzian LinearOperator of (REAL-NS n),(REAL-NS 1) & (BoundedLinearOperatorsNorm ((REAL-NS n),(REAL-NS 1))) . (Proj (i,n)) <= 1 ) )
assume A1: ( 1 <= i & i <= n ) ; ::_thesis: ( Proj (i,n) is Lipschitzian LinearOperator of (REAL-NS n),(REAL-NS 1) & (BoundedLinearOperatorsNorm ((REAL-NS n),(REAL-NS 1))) . (Proj (i,n)) <= 1 )
A2: for y being Point of (REAL-NS n)
for r being Real holds (Proj (i,n)) . (r * y) = r * ((Proj (i,n)) . y) by PDIFF_6:27;
 for y1, y2 being Point of (REAL-NS n) holds (Proj (i,n)) . (y1 + y2) = ((Proj (i,n)) . y1) + ((Proj (i,n)) . y2) by PDIFF_6:26;
hence A3: Proj (i,n) is Lipschitzian LinearOperator of (REAL-NS n),(REAL-NS 1) by A2, VECTSP_1:def_20, LOPBAN_1:def_5; ::_thesis: (BoundedLinearOperatorsNorm ((REAL-NS n),(REAL-NS 1))) . (Proj (i,n)) <= 1
deffunc H1( Element of NAT , Element of NAT ) ->  Element of K10(K11((BoundedLinearOperators ((REAL-NS $1),(REAL-NS $2))),REAL)) = BoundedLinearOperatorsNorm ((REAL-NS $1),(REAL-NS $2));
A4: Proj (i,n) in BoundedLinearOperators ((REAL-NS n),(REAL-NS 1)) by A3, LOPBAN_1:def_9;
set s0 = modetrans ((Proj (i,n)),(REAL-NS n),(REAL-NS 1));
 upper_bound (PreNorms (modetrans ((Proj (i,n)),(REAL-NS n),(REAL-NS 1)))) <= 1
proof
A5: for x being real set st x in PreNorms (modetrans ((Proj (i,n)),(REAL-NS n),(REAL-NS 1))) holds
x <= 1
proof
let x be real set ; ::_thesis: ( x in PreNorms (modetrans ((Proj (i,n)),(REAL-NS n),(REAL-NS 1))) implies x <= 1 )
assume  x in PreNorms (modetrans ((Proj (i,n)),(REAL-NS n),(REAL-NS 1))) ; ::_thesis: x <= 1
then consider y being VECTOR of (REAL-NS n) such that
A6: ( x = ||.((modetrans ((Proj (i,n)),(REAL-NS n),(REAL-NS 1))) . y).|| & ||.y.|| <= 1 ) ;
A7: ||.((Proj (i,n)) . y).|| <= ||.y.|| by A1, Th3;
 Proj (i,n) = modetrans ((Proj (i,n)),(REAL-NS n),(REAL-NS 1)) by A3, LOPBAN_1:29;
hence  x <= 1 by A6, A7, XXREAL_0:2; ::_thesis: verum
end;
A8: PreNorms (modetrans ((Proj (i,n)),(REAL-NS n),(REAL-NS 1))) is bounded_above
proof
 for x being ext-real set st x in PreNorms (modetrans ((Proj (i,n)),(REAL-NS n),(REAL-NS 1))) holds
x <= 1 by A5;
then  1 is UpperBound of PreNorms (modetrans ((Proj (i,n)),(REAL-NS n),(REAL-NS 1))) by XXREAL_2:def_1;
hence  PreNorms (modetrans ((Proj (i,n)),(REAL-NS n),(REAL-NS 1))) is bounded_above by XXREAL_2:def_10; ::_thesis: verum
end;
assume A9: upper_bound (PreNorms (modetrans ((Proj (i,n)),(REAL-NS n),(REAL-NS 1)))) > 1 ; ::_thesis: contradiction
set dif = (upper_bound (PreNorms (modetrans ((Proj (i,n)),(REAL-NS n),(REAL-NS 1))))) - 1;
A10: (upper_bound (PreNorms (modetrans ((Proj (i,n)),(REAL-NS n),(REAL-NS 1))))) - 1 > 0 by A9, XREAL_1:50;
 ex w being real set st
( w in PreNorms (modetrans ((Proj (i,n)),(REAL-NS n),(REAL-NS 1))) & (upper_bound (PreNorms (modetrans ((Proj (i,n)),(REAL-NS n),(REAL-NS 1))))) - ((upper_bound (PreNorms (modetrans ((Proj (i,n)),(REAL-NS n),(REAL-NS 1))))) - 1) < w ) by A10, A8, SEQ_4:def_1;
hence  contradiction by A5; ::_thesis: verum
end;
hence  (BoundedLinearOperatorsNorm ((REAL-NS n),(REAL-NS 1))) . (Proj (i,n)) <= 1 by A4, LOPBAN_1:def_13; ::_thesis: verum
end;

theorem Th7: :: PDIFF_8:7
for m, n being non empty Element of NAT
for s being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))
for i being Element of NAT st 1 <= i & i <= n holds
( (Proj (i,n)) * s is Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))) & (BoundedLinearOperatorsNorm ((REAL-NS m),(REAL-NS 1))) . ((Proj (i,n)) * s) <= ((BoundedLinearOperatorsNorm ((REAL-NS n),(REAL-NS 1))) . (Proj (i,n))) * ((BoundedLinearOperatorsNorm ((REAL-NS m),(REAL-NS n))) . s) )
proof
let m, n be non empty Element of NAT ; ::_thesis: for s being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))
for i being Element of NAT st 1 <= i & i <= n holds
( (Proj (i,n)) * s is Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))) & (BoundedLinearOperatorsNorm ((REAL-NS m),(REAL-NS 1))) . ((Proj (i,n)) * s) <= ((BoundedLinearOperatorsNorm ((REAL-NS n),(REAL-NS 1))) . (Proj (i,n))) * ((BoundedLinearOperatorsNorm ((REAL-NS m),(REAL-NS n))) . s) )
let s be Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))); ::_thesis: for i being Element of NAT st 1 <= i & i <= n holds
( (Proj (i,n)) * s is Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))) & (BoundedLinearOperatorsNorm ((REAL-NS m),(REAL-NS 1))) . ((Proj (i,n)) * s) <= ((BoundedLinearOperatorsNorm ((REAL-NS n),(REAL-NS 1))) . (Proj (i,n))) * ((BoundedLinearOperatorsNorm ((REAL-NS m),(REAL-NS n))) . s) )
let i be Element of NAT ; ::_thesis: ( 1 <= i & i <= n implies ( (Proj (i,n)) * s is Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))) & (BoundedLinearOperatorsNorm ((REAL-NS m),(REAL-NS 1))) . ((Proj (i,n)) * s) <= ((BoundedLinearOperatorsNorm ((REAL-NS n),(REAL-NS 1))) . (Proj (i,n))) * ((BoundedLinearOperatorsNorm ((REAL-NS m),(REAL-NS n))) . s) ) )
deffunc H1( Element of NAT , Element of NAT ) ->  Element of K10(K11((BoundedLinearOperators ((REAL-NS $1),(REAL-NS $2))),REAL)) = BoundedLinearOperatorsNorm ((REAL-NS $1),(REAL-NS $2));
assume  ( 1 <= i & i <= n ) ; ::_thesis: ( (Proj (i,n)) * s is Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))) & (BoundedLinearOperatorsNorm ((REAL-NS m),(REAL-NS 1))) . ((Proj (i,n)) * s) <= ((BoundedLinearOperatorsNorm ((REAL-NS n),(REAL-NS 1))) . (Proj (i,n))) * ((BoundedLinearOperatorsNorm ((REAL-NS m),(REAL-NS n))) . s) )
then A1: Proj (i,n) is Lipschitzian LinearOperator of (REAL-NS n),(REAL-NS 1) by Th6;
 s is Lipschitzian LinearOperator of (REAL-NS m),(REAL-NS n) by LOPBAN_1:def_9;
then  ( (Proj (i,n)) * s is Lipschitzian LinearOperator of (REAL-NS m),(REAL-NS 1) & H1(m,1) . ((Proj (i,n)) * s) <= (H1(n,1) . (Proj (i,n))) * (H1(m,n) . s) ) by A1, LOPBAN_2:2;
hence  ( (Proj (i,n)) * s is Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))) & (BoundedLinearOperatorsNorm ((REAL-NS m),(REAL-NS 1))) . ((Proj (i,n)) * s) <= ((BoundedLinearOperatorsNorm ((REAL-NS n),(REAL-NS 1))) . (Proj (i,n))) * ((BoundedLinearOperatorsNorm ((REAL-NS m),(REAL-NS n))) . s) ) by LOPBAN_1:def_9; ::_thesis: verum
end;

theorem :: PDIFF_8:8
for n being non empty Element of NAT
for i being Element of NAT holds Proj (i,n) is homogeneous
proof
let n be non empty Element of NAT ; ::_thesis: for i being Element of NAT holds Proj (i,n) is homogeneous
let i be Element of NAT ; ::_thesis: Proj (i,n) is homogeneous
thus  for x being Point of (REAL-NS n)
for r being Real holds (Proj (i,n)) . (r * x) = r * ((Proj (i,n)) . x) by PDIFF_6:27; :: according to LOPBAN_1:def_5 ::_thesis: verum
end;

theorem :: PDIFF_8:9
for n being non empty Element of NAT
for x being Element of REAL n
for r being Real
for i being Element of NAT holds (proj (i,n)) . (r * x) = r * ((proj (i,n)) . x)
proof
let n be non empty Element of NAT ; ::_thesis: for x being Element of REAL n
for r being Real
for i being Element of NAT holds (proj (i,n)) . (r * x) = r * ((proj (i,n)) . x)
let x be Element of REAL n; ::_thesis: for r being Real
for i being Element of NAT holds (proj (i,n)) . (r * x) = r * ((proj (i,n)) . x)
let r be Real; ::_thesis: for i being Element of NAT holds (proj (i,n)) . (r * x) = r * ((proj (i,n)) . x)
let i be Element of NAT ; ::_thesis: (proj (i,n)) . (r * x) = r * ((proj (i,n)) . x)
thus (proj (i,n)) . (r * x) = (r * x) . i by PDIFF_1:def_1
.= r * (x . i) by RVSUM_1:44
.= r * ((proj (i,n)) . x) by PDIFF_1:def_1 ; ::_thesis: verum
end;

theorem :: PDIFF_8:10
for n being non empty Element of NAT
for x, y being Element of REAL n
for i being Element of NAT holds (proj (i,n)) . (x + y) = ((proj (i,n)) . x) + ((proj (i,n)) . y)
proof
let n be non empty Element of NAT ; ::_thesis: for x, y being Element of REAL n
for i being Element of NAT holds (proj (i,n)) . (x + y) = ((proj (i,n)) . x) + ((proj (i,n)) . y)
let x, y be Element of REAL n; ::_thesis: for i being Element of NAT holds (proj (i,n)) . (x + y) = ((proj (i,n)) . x) + ((proj (i,n)) . y)
let i be Element of NAT ; ::_thesis: (proj (i,n)) . (x + y) = ((proj (i,n)) . x) + ((proj (i,n)) . y)
thus (proj (i,n)) . (x + y) = (x + y) . i by PDIFF_1:def_1
.= (x . i) + (y . i) by RVSUM_1:11
.= ((proj (i,n)) . x) + (y . i) by PDIFF_1:def_1
.= ((proj (i,n)) . x) + ((proj (i,n)) . y) by PDIFF_1:def_1 ; ::_thesis: verum
end;

theorem Th11: :: PDIFF_8:11
for n being non empty Element of NAT
for x, y being Point of (REAL-NS n)
for i being Element of NAT holds (Proj (i,n)) . (x - y) = ((Proj (i,n)) . x) - ((Proj (i,n)) . y)
proof
let n be non empty Element of NAT ; ::_thesis: for x, y being Point of (REAL-NS n)
for i being Element of NAT holds (Proj (i,n)) . (x - y) = ((Proj (i,n)) . x) - ((Proj (i,n)) . y)
let x, y be Point of (REAL-NS n); ::_thesis: for i being Element of NAT holds (Proj (i,n)) . (x - y) = ((Proj (i,n)) . x) - ((Proj (i,n)) . y)
let i be Element of NAT ; ::_thesis: (Proj (i,n)) . (x - y) = ((Proj (i,n)) . x) - ((Proj (i,n)) . y)
reconsider x1 = x, y1 = y as Element of REAL n by REAL_NS1:def_4;
reconsider rx = x1 . i, ry = y1 . i as Element of REAL ;
 ( (Proj (i,n)) . x = <*((proj (i,n)) . x)*> & (Proj (i,n)) . y = <*((proj (i,n)) . y)*> ) by PDIFF_1:def_4;
then A1: ( (Proj (i,n)) . x = <*rx*> & (Proj (i,n)) . y = <*ry*> ) by PDIFF_1:def_1;
A2: ( <*rx*> is Element of REAL 1 & <*ry*> is Element of REAL 1 ) by FINSEQ_2:98;
(Proj (i,n)) . (x - y) = <*((proj (i,n)) . (x - y))*> by PDIFF_1:def_4
.= <*((proj (i,n)) . (x1 - y1))*> by REAL_NS1:5
.= <*((x1 - y1) . i)*> by PDIFF_1:def_1
.= <*((x1 . i) - (y1 . i))*> by RVSUM_1:27
.= <*rx*> - <*ry*> by RVSUM_1:29 ;
hence  (Proj (i,n)) . (x - y) = ((Proj (i,n)) . x) - ((Proj (i,n)) . y) by A1, A2, REAL_NS1:5; ::_thesis: verum
end;

theorem :: PDIFF_8:12
for n being non empty Element of NAT
for x, y being Element of REAL n
for i being Element of NAT holds (proj (i,n)) . (x - y) = ((proj (i,n)) . x) - ((proj (i,n)) . y)
proof
let n be non empty Element of NAT ; ::_thesis: for x, y being Element of REAL n
for i being Element of NAT holds (proj (i,n)) . (x - y) = ((proj (i,n)) . x) - ((proj (i,n)) . y)
let x, y be Element of REAL n; ::_thesis: for i being Element of NAT holds (proj (i,n)) . (x - y) = ((proj (i,n)) . x) - ((proj (i,n)) . y)
let i be Element of NAT ; ::_thesis: (proj (i,n)) . (x - y) = ((proj (i,n)) . x) - ((proj (i,n)) . y)
thus (proj (i,n)) . (x - y) = (x - y) . i by PDIFF_1:def_1
.= (x . i) - (y . i) by RVSUM_1:27
.= ((proj (i,n)) . x) - (y . i) by PDIFF_1:def_1
.= ((proj (i,n)) . x) - ((proj (i,n)) . y) by PDIFF_1:def_1 ; ::_thesis: verum
end;

Lm1:  for m, n being non empty Element of NAT
for s, t being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))
for i being Element of NAT
for si, ti being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))) st si = (Proj (i,n)) * s & ti = (Proj (i,n)) * t & 1 <= i & i <= n holds
si - ti = (Proj (i,n)) * (s - t)
proof
let m, n be non empty Element of NAT ; ::_thesis: for s, t being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))
for i being Element of NAT
for si, ti being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))) st si = (Proj (i,n)) * s & ti = (Proj (i,n)) * t & 1 <= i & i <= n holds
si - ti = (Proj (i,n)) * (s - t)
let s, t be Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))); ::_thesis: for i being Element of NAT
for si, ti being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))) st si = (Proj (i,n)) * s & ti = (Proj (i,n)) * t & 1 <= i & i <= n holds
si - ti = (Proj (i,n)) * (s - t)
let i be Element of NAT ; ::_thesis: for si, ti being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))) st si = (Proj (i,n)) * s & ti = (Proj (i,n)) * t & 1 <= i & i <= n holds
si - ti = (Proj (i,n)) * (s - t)
let si, ti be Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))); ::_thesis: ( si = (Proj (i,n)) * s & ti = (Proj (i,n)) * t & 1 <= i & i <= n implies si - ti = (Proj (i,n)) * (s - t) )
assume A1: ( si = (Proj (i,n)) * s & ti = (Proj (i,n)) * t & 1 <= i & i <= n ) ; ::_thesis: si - ti = (Proj (i,n)) * (s - t)
deffunc H1( non empty Element of NAT , non empty Element of NAT ) ->  L16() = R_NormSpace_of_BoundedLinearOperators ((REAL-NS $1),(REAL-NS $2));
A2: the carrier of (REAL-NS m) = REAL m by REAL_NS1:def_4;
A3: Proj (i,n) is Lipschitzian LinearOperator of (REAL-NS n),(REAL-NS 1) by Th6, A1;
A4: dom (si - ti) = REAL m
proof
 si - ti is LinearOperator of (REAL-NS m),(REAL-NS 1) by LOPBAN_1:def_9;
hence  dom (si - ti) = REAL m by A2, FUNCT_2:def_1; ::_thesis: verum
end;
A5: dom (si - ti) = dom ((Proj (i,n)) * (s - t))
proof
 s - t is Lipschitzian LinearOperator of (REAL-NS m),(REAL-NS n) by LOPBAN_1:def_9;
then  (Proj (i,n)) * (s - t) is LinearOperator of (REAL-NS m),(REAL-NS 1) by A3, LOPBAN_2:1;
hence  dom (si - ti) = dom ((Proj (i,n)) * (s - t)) by A4, A2, FUNCT_2:def_1; ::_thesis: verum
end;
A6: dom si = REAL m
proof
 si is LinearOperator of (REAL-NS m),(REAL-NS 1) by LOPBAN_1:def_9;
hence  dom si = REAL m by A2, FUNCT_2:def_1; ::_thesis: verum
end;
A7: dom ti = REAL m
proof
 ti is LinearOperator of (REAL-NS m),(REAL-NS 1) by LOPBAN_1:def_9;
hence  dom ti = REAL m by A2, FUNCT_2:def_1; ::_thesis: verum
end;
A8: for x being Point of (REAL-NS m) holds (si - ti) . x = ((Proj (i,n)) * (s - t)) . x
proof
let x be Point of (REAL-NS m); ::_thesis: (si - ti) . x = ((Proj (i,n)) * (s - t)) . x
reconsider x = x as Element of REAL m by REAL_NS1:def_4;
reconsider y = x as Point of (REAL-NS m) ;
((Proj (i,n)) * (s - t)) . x = (Proj (i,n)) . ((s - t) . x) by A4, A5, FUNCT_1:12
.= (Proj (i,n)) . ((s . y) - (t . y)) by LOPBAN_1:40
.= ((Proj (i,n)) . (s . y)) - ((Proj (i,n)) . (t . y)) by Th11
.= (si . y) - ((Proj (i,n)) . (t . y)) by A1, A6, FUNCT_1:12
.= (si . y) - (ti . y) by A1, A7, FUNCT_1:12
.= (si - ti) . x by LOPBAN_1:40 ;
hence  (si - ti) . x = ((Proj (i,n)) * (s - t)) . x ; ::_thesis: verum
end;
 for x being set st x in dom (si - ti) holds
(si - ti) . x = ((Proj (i,n)) * (s - t)) . x
proof
let x be set ; ::_thesis: ( x in dom (si - ti) implies (si - ti) . x = ((Proj (i,n)) * (s - t)) . x )
assume A9: x in dom (si - ti) ; ::_thesis: (si - ti) . x = ((Proj (i,n)) * (s - t)) . x
reconsider x = x as Point of (REAL-NS m) by A9, A4, REAL_NS1:def_4;
 (si - ti) . x = ((Proj (i,n)) * (s - t)) . x by A8;
hence  (si - ti) . x = ((Proj (i,n)) * (s - t)) . x ; ::_thesis: verum
end;
hence  si - ti = (Proj (i,n)) * (s - t) by A5, FUNCT_1:2; ::_thesis: verum
end;

theorem Th13: :: PDIFF_8:13
for m, n being non empty Element of NAT
for s being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))
for i being Element of NAT
for si being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))) st si = (Proj (i,n)) * s & 1 <= i & i <= n holds
||.si.|| <= ||.s.||
proof
let m, n be non empty Element of NAT ; ::_thesis: for s being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))
for i being Element of NAT
for si being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))) st si = (Proj (i,n)) * s & 1 <= i & i <= n holds
||.si.|| <= ||.s.||
let s be Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))); ::_thesis: for i being Element of NAT
for si being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))) st si = (Proj (i,n)) * s & 1 <= i & i <= n holds
||.si.|| <= ||.s.||
let i be Element of NAT ; ::_thesis: for si being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))) st si = (Proj (i,n)) * s & 1 <= i & i <= n holds
||.si.|| <= ||.s.||
let si be Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))); ::_thesis: ( si = (Proj (i,n)) * s & 1 <= i & i <= n implies ||.si.|| <= ||.s.|| )
assume A1: ( si = (Proj (i,n)) * s & 1 <= i & i <= n ) ; ::_thesis: ||.si.|| <= ||.s.||
deffunc H1( Element of NAT , Element of NAT ) ->  Element of K10(K11((BoundedLinearOperators ((REAL-NS $1),(REAL-NS $2))),REAL)) = BoundedLinearOperatorsNorm ((REAL-NS $1),(REAL-NS $2));
A2: ( Proj (i,n) is Lipschitzian LinearOperator of (REAL-NS n),(REAL-NS 1) & H1(n,1) . (Proj (i,n)) <= 1 ) by Th6, A1;
 s is Lipschitzian LinearOperator of (REAL-NS m),(REAL-NS n) by LOPBAN_1:def_9;
then A3: ||.si.|| <= (H1(n,1) . (Proj (i,n))) * ||.s.|| by A2, A1, LOPBAN_2:2;
 0 <= ||.s.|| by NORMSP_1:4;
then  (H1(n,1) . (Proj (i,n))) * ||.s.|| <= 1 * ||.s.|| by Th6, A1, XREAL_1:64;
hence  ||.si.|| <= ||.s.|| by A3, XXREAL_0:2; ::_thesis: verum
end;

theorem Th14: :: PDIFF_8:14
for m, n being non empty Element of NAT
for s, t being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))
for si, ti being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1)))
for i being Element of NAT st si = (Proj (i,n)) * s & ti = (Proj (i,n)) * t & 1 <= i & i <= n holds
||.(si - ti).|| <= ||.(s - t).||
proof
let m, n be non empty Element of NAT ; ::_thesis: for s, t being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))
for si, ti being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1)))
for i being Element of NAT st si = (Proj (i,n)) * s & ti = (Proj (i,n)) * t & 1 <= i & i <= n holds
||.(si - ti).|| <= ||.(s - t).||
let s, t be Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))); ::_thesis: for si, ti being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1)))
for i being Element of NAT st si = (Proj (i,n)) * s & ti = (Proj (i,n)) * t & 1 <= i & i <= n holds
||.(si - ti).|| <= ||.(s - t).||
let si, ti be Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))); ::_thesis: for i being Element of NAT st si = (Proj (i,n)) * s & ti = (Proj (i,n)) * t & 1 <= i & i <= n holds
||.(si - ti).|| <= ||.(s - t).||
let i be Element of NAT ; ::_thesis: ( si = (Proj (i,n)) * s & ti = (Proj (i,n)) * t & 1 <= i & i <= n implies ||.(si - ti).|| <= ||.(s - t).|| )
deffunc H1( Element of NAT , Element of NAT ) ->  Element of K10(K11((BoundedLinearOperators ((REAL-NS $1),(REAL-NS $2))),REAL)) = BoundedLinearOperatorsNorm ((REAL-NS $1),(REAL-NS $2));
assume A1: ( si = (Proj (i,n)) * s & ti = (Proj (i,n)) * t & 1 <= i & i <= n ) ; ::_thesis: ||.(si - ti).|| <= ||.(s - t).||
 si - ti = (Proj (i,n)) * (s - t) by Lm1, A1;
hence  ||.(si - ti).|| <= ||.(s - t).|| by A1, Th13; ::_thesis: verum
end;

theorem Th15: :: PDIFF_8:15
for K being Real
for n being Element of NAT
for s being Element of REAL n st ( for i being Element of NAT st 1 <= i & i <= n holds
abs (s . i) <= K ) holds
|.s.| <= n * K
proof
let K be Real; ::_thesis: for n being Element of NAT
for s being Element of REAL n st ( for i being Element of NAT st 1 <= i & i <= n holds
abs (s . i) <= K ) holds
|.s.| <= n * K
defpred S1[ Nat] means  for s being Element of REAL $1 st ( for i being Element of NAT st 1 <= i & i <= $1 holds
abs (s . i) <= K ) holds
|.s.| <= $1 * K;
A1: S1[ 0 ]
proof
let s be Element of REAL 0; ::_thesis: ( ( for i being Element of NAT st 1 <= i & i <= 0 holds
abs (s . i) <= K ) implies |.s.| <= 0 * K )
 s = 0* 0 ;
hence  ( ( for i being Element of NAT st 1 <= i & i <= 0 holds
abs (s . i) <= K ) implies |.s.| <= 0 * K ) by EUCLID:7; ::_thesis: verum
end;
A2: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A3: S1[n] ; ::_thesis: S1[n + 1]
let s be Element of REAL (n + 1); ::_thesis: ( ( for i being Element of NAT st 1 <= i & i <= n + 1 holds
abs (s . i) <= K ) implies |.s.| <= (n + 1) * K )
assume A4: for i being Element of NAT st 1 <= i & i <= n + 1 holds
abs (s . i) <= K ; ::_thesis: |.s.| <= (n + 1) * K
set sn = s | n;
 len s = n + 1 by CARD_1:def_7;
then  len (s | n) = n by FINSEQ_3:53;
then reconsider sn = s | n as Element of REAL n by FINSEQ_2:92;
A5: now__::_thesis:_for_i_being_Element_of_NAT_st_1_<=_i_&_i_<=_n_holds_
abs_(sn_._i)_<=_K
let i be Element of NAT ; ::_thesis: ( 1 <= i & i <= n implies abs (sn . i) <= K )
assume A6: ( 1 <= i & i <= n ) ; ::_thesis: abs (sn . i) <= K
 n <= n + 1 by NAT_1:11;
then  ( 1 <= i & i <= n + 1 ) by A6, XXREAL_0:2;
then  abs (s . i) <= K by A4;
hence  abs (sn . i) <= K by A6, FINSEQ_3:112; ::_thesis: verum
end;
 ( 1 <= n + 1 & n + 1 <= n + 1 ) by NAT_1:11;
then A7: abs (s . (n + 1)) <= K by A4;
A8: |.s.| ^2 = (|.sn.| ^2) + ((s . (n + 1)) ^2) by REAL_NS1:10;
A9: K >= 0 by A7, COMPLEX1:46;
A10: |.sn.| ^2 <= (n * K) ^2 by A3, A5, SQUARE_1:15;
A11: (s . (n + 1)) ^2 <= K ^2 by A7, SERIES_3:24;
A12: (((n * K) ^2) + (K ^2)) + ((2 * (n * K)) * K) >= ((n * K) ^2) + (K ^2) by A9, XREAL_1:38;
 (|.sn.| ^2) + ((s . (n + 1)) ^2) <= ((n * K) ^2) + (K ^2) by A10, A11, XREAL_1:7;
then A13: |.s.| ^2 <= ((n + 1) * K) ^2 by A8, A12, XXREAL_0:2;
A14: sqrt (((n + 1) * K) ^2) = |.((n + 1) * K).| by COMPLEX1:72;
 sqrt (|.s.| ^2) <= sqrt (((n + 1) * K) ^2) by A13, SQUARE_1:26;
then  abs (abs |.s.|) <= sqrt (((n + 1) * K) ^2) by COMPLEX1:72;
then  |.s.| <= sqrt (((n + 1) * K) ^2) by ABSVALUE:def_1;
hence  |.s.| <= (n + 1) * K by A9, A14, ABSVALUE:def_1; ::_thesis: verum
end;
thus  for n being Element of NAT holds S1[n] from NAT_1:sch_1(A1, A2); ::_thesis: verum
end;

theorem Th16: :: PDIFF_8:16
for K being Real
for n being non empty Element of NAT
for s being Element of (REAL-NS n) st ( for i being Element of NAT st 1 <= i & i <= n holds
||.((Proj (i,n)) . s).|| <= K ) holds
||.s.|| <= n * K
proof
let K be Real; ::_thesis: for n being non empty Element of NAT
for s being Element of (REAL-NS n) st ( for i being Element of NAT st 1 <= i & i <= n holds
||.((Proj (i,n)) . s).|| <= K ) holds
||.s.|| <= n * K
let n be non empty Element of NAT ; ::_thesis: for s being Element of (REAL-NS n) st ( for i being Element of NAT st 1 <= i & i <= n holds
||.((Proj (i,n)) . s).|| <= K ) holds
||.s.|| <= n * K
let s be Element of (REAL-NS n); ::_thesis: ( ( for i being Element of NAT st 1 <= i & i <= n holds
||.((Proj (i,n)) . s).|| <= K ) implies ||.s.|| <= n * K )
assume A1: for i being Element of NAT st 1 <= i & i <= n holds
||.((Proj (i,n)) . s).|| <= K ; ::_thesis: ||.s.|| <= n * K
consider m being Nat such that
A2: n = m + 1 by NAT_1:6;
reconsider m = m as Element of NAT by ORDINAL1:def_12;
reconsider s0 = s as Element of REAL n by REAL_NS1:def_4;
now__::_thesis:_for_i_being_Element_of_NAT_st_1_<=_i_&_i_<=_m_+_1_holds_
abs_(s0_._i)_<=_K
let i be Element of NAT ; ::_thesis: ( 1 <= i & i <= m + 1 implies abs (s0 . i) <= K )
assume  ( 1 <= i & i <= m + 1 ) ; ::_thesis: abs (s0 . i) <= K
then A3: ||.((Proj (i,n)) . s).|| <= K by A2, A1;
(Proj (i,n)) . s = <*((proj (i,n)) . s0)*> by PDIFF_1:def_4
.= <*(s0 . i)*> by PDIFF_1:def_1 ;
hence  abs (s0 . i) <= K by A3, Th2; ::_thesis: verum
end;
then  |.s0.| <= n * K by A2, Th15;
hence  ||.s.|| <= n * K by REAL_NS1:1; ::_thesis: verum
end;

theorem :: PDIFF_8:17
for K being Real
for n being non empty Element of NAT
for s being Element of REAL n st ( for i being Element of NAT st 1 <= i & i <= n holds
|.((proj (i,n)) . s).| <= K ) holds
|.s.| <= n * K
proof
let K be Real; ::_thesis: for n being non empty Element of NAT
for s being Element of REAL n st ( for i being Element of NAT st 1 <= i & i <= n holds
|.((proj (i,n)) . s).| <= K ) holds
|.s.| <= n * K
let n be non empty Element of NAT ; ::_thesis: for s being Element of REAL n st ( for i being Element of NAT st 1 <= i & i <= n holds
|.((proj (i,n)) . s).| <= K ) holds
|.s.| <= n * K
let s be Element of REAL n; ::_thesis: ( ( for i being Element of NAT st 1 <= i & i <= n holds
|.((proj (i,n)) . s).| <= K ) implies |.s.| <= n * K )
assume A1: for i being Element of NAT st 1 <= i & i <= n holds
|.((proj (i,n)) . s).| <= K ; ::_thesis: |.s.| <= n * K
reconsider t = s as Element of (REAL-NS n) by REAL_NS1:def_4;
 for i being Element of NAT st 1 <= i & i <= n holds
||.((Proj (i,n)) . t).|| <= K
proof
let i be Element of NAT ; ::_thesis: ( 1 <= i & i <= n implies ||.((Proj (i,n)) . t).|| <= K )
assume  ( 1 <= i & i <= n ) ; ::_thesis: ||.((Proj (i,n)) . t).|| <= K
then  |.((proj (i,n)) . t).| <= K by A1;
hence  ||.((Proj (i,n)) . t).|| <= K by Th4; ::_thesis: verum
end;
then  ||.t.|| <= n * K by Th16;
hence  |.s.| <= n * K by REAL_NS1:1; ::_thesis: verum
end;

theorem Th18: :: PDIFF_8:18
for m, n being non empty Element of NAT
for s being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))
for K being Real st ( for i being Element of NAT
for si being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))) st si = (Proj (i,n)) * s & 1 <= i & i <= n holds
||.si.|| <= K ) holds
||.s.|| <= n * K
proof
deffunc H1( non empty Element of NAT , non empty Element of NAT ) ->  L16() = R_NormSpace_of_BoundedLinearOperators ((REAL-NS $1),(REAL-NS $2));
let m, n be non empty Element of NAT ; ::_thesis: for s being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))
for K being Real st ( for i being Element of NAT
for si being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))) st si = (Proj (i,n)) * s & 1 <= i & i <= n holds
||.si.|| <= K ) holds
||.s.|| <= n * K
let s be Point of H1(m,n); ::_thesis: for K being Real st ( for i being Element of NAT
for si being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))) st si = (Proj (i,n)) * s & 1 <= i & i <= n holds
||.si.|| <= K ) holds
||.s.|| <= n * K
let K be Real; ::_thesis: ( ( for i being Element of NAT
for si being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))) st si = (Proj (i,n)) * s & 1 <= i & i <= n holds
||.si.|| <= K ) implies ||.s.|| <= n * K )
assume A1: for i being Element of NAT
for si being Point of H1(m,1) st si = (Proj (i,n)) * s & 1 <= i & i <= n holds
||.si.|| <= K ; ::_thesis: ||.s.|| <= n * K
reconsider s0 = s as Lipschitzian LinearOperator of (REAL-NS m),(REAL-NS n) by LOPBAN_1:def_9;
A2: now__::_thesis:_for_x_being_Point_of_(REAL-NS_m)_st_||.x.||_<=_1_holds_
||.(s0_._x).||_<=_n_*_K
let x be Point of (REAL-NS m); ::_thesis: ( ||.x.|| <= 1 implies ||.(s0 . x).|| <= n * K )
assume A3: ||.x.|| <= 1 ; ::_thesis: ||.(s0 . x).|| <= n * K
now__::_thesis:_for_i_being_Element_of_NAT_st_1_<=_i_&_i_<=_n_holds_
||.((Proj_(i,n))_._(s_._x)).||_<=_K_*_||.x.||
let i be Element of NAT ; ::_thesis: ( 1 <= i & i <= n implies ||.((Proj (i,n)) . (s . x)).|| <= K * ||.x.|| )
assume A4: ( 1 <= i & i <= n ) ; ::_thesis: ||.((Proj (i,n)) . (s . x)).|| <= K * ||.x.||
set si = (Proj (i,n)) * s;
reconsider si = (Proj (i,n)) * s as Point of H1(m,1) by Th7, A4;
reconsider sii = si as Lipschitzian LinearOperator of (REAL-NS m),(REAL-NS 1) by LOPBAN_1:def_9;
A5: ||.(sii . x).|| <= ||.si.|| * ||.x.|| by LOPBAN_1:32;
A6: the carrier of (REAL-NS m) = REAL m by REAL_NS1:def_4;
A7: Proj (i,n) is Lipschitzian LinearOperator of (REAL-NS n),(REAL-NS 1) by A4, Th6;
 s is Lipschitzian LinearOperator of (REAL-NS m),(REAL-NS n) by LOPBAN_1:def_9;
then  (Proj (i,n)) * s is LinearOperator of (REAL-NS m),(REAL-NS 1) by A7, LOPBAN_2:1;
then  dom ((Proj (i,n)) * s) = REAL m by A6, FUNCT_2:def_1;
then A8: sii . x = (Proj (i,n)) . (s . x) by A6, FUNCT_1:12;
A9: 0 <= ||.x.|| by NORMSP_1:4;
 ||.si.|| * ||.x.|| <= K * ||.x.|| by A4, A1, A9, XREAL_1:64;
hence  ||.((Proj (i,n)) . (s . x)).|| <= K * ||.x.|| by A5, A8, XXREAL_0:2; ::_thesis: verum
end;
then A10: ||.(s . x).|| <= n * (K * ||.x.||) by Th16;
A11: ( 1 <= 1 & 1 <= n ) by NAT_1:14;
then reconsider s1 = (Proj (1,n)) * s as Point of H1(m,1) by Th7;
 ||.s1.|| <= K by A11, A1;
then A12: 0 <= K by NORMSP_1:4;
 (n * K) * ||.x.|| <= (n * K) * 1 by A12, A3, XREAL_1:64;
hence  ||.(s0 . x).|| <= n * K by A10, XXREAL_0:2; ::_thesis: verum
end;
set PreNormS = PreNorms (modetrans (s,(REAL-NS m),(REAL-NS n)));
A13: for y being ext-real set st y in PreNorms (modetrans (s,(REAL-NS m),(REAL-NS n))) holds
y <= n * K
proof
let y be ext-real set ; ::_thesis: ( y in PreNorms (modetrans (s,(REAL-NS m),(REAL-NS n))) implies y <= n * K )
assume A14: y in PreNorms (modetrans (s,(REAL-NS m),(REAL-NS n))) ; ::_thesis: y <= n * K
consider x being VECTOR of (REAL-NS m) such that
A15: ( y = ||.((modetrans (s,(REAL-NS m),(REAL-NS n))) . x).|| & ||.x.|| <= 1 ) by A14;
 y = ||.(s0 . x).|| by A15, LOPBAN_1:29;
hence  y <= n * K by A2, A15; ::_thesis: verum
end;
A16: PreNorms (modetrans (s,(REAL-NS m),(REAL-NS n))) is bounded_above
proof
 n * K is UpperBound of PreNorms (modetrans (s,(REAL-NS m),(REAL-NS n))) by A13, XXREAL_2:def_1;
hence  PreNorms (modetrans (s,(REAL-NS m),(REAL-NS n))) is bounded_above by XXREAL_2:def_10; ::_thesis: verum
end;
set UBPreNormS = upper_bound (PreNorms (modetrans (s,(REAL-NS m),(REAL-NS n))));
 not upper_bound (PreNorms (modetrans (s,(REAL-NS m),(REAL-NS n)))) > n * K
proof
assume A17: upper_bound (PreNorms (modetrans (s,(REAL-NS m),(REAL-NS n)))) > n * K ; ::_thesis: contradiction
set dif = (upper_bound (PreNorms (modetrans (s,(REAL-NS m),(REAL-NS n))))) - (n * K);
A18: (upper_bound (PreNorms (modetrans (s,(REAL-NS m),(REAL-NS n))))) - (n * K) > 0 by A17, XREAL_1:50;
consider w being real set  such that
A19: ( w in PreNorms (modetrans (s,(REAL-NS m),(REAL-NS n))) & (upper_bound (PreNorms (modetrans (s,(REAL-NS m),(REAL-NS n))))) - ((upper_bound (PreNorms (modetrans (s,(REAL-NS m),(REAL-NS n))))) - (n * K)) < w ) by A18, A16, SEQ_4:def_1;
thus  contradiction by A19, A13; ::_thesis: verum
end;
then  upper_bound (PreNorms s0) <= n * K by LOPBAN_1:def_11;
hence  ||.s.|| <= n * K by LOPBAN_1:30; ::_thesis: verum
end;

theorem Th19: :: PDIFF_8:19
for m, n being non empty Element of NAT
for s, t being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))
for K being Real st ( for i being Element of NAT
for si, ti being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))) st si = (Proj (i,n)) * s & ti = (Proj (i,n)) * t & 1 <= i & i <= n holds
||.(si - ti).|| <= K ) holds
||.(s - t).|| <= n * K
proof
deffunc H1( non empty Element of NAT , non empty Element of NAT ) ->  L16() = R_NormSpace_of_BoundedLinearOperators ((REAL-NS $1),(REAL-NS $2));
let m, n be non empty Element of NAT ; ::_thesis: for s, t being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))
for K being Real st ( for i being Element of NAT
for si, ti being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))) st si = (Proj (i,n)) * s & ti = (Proj (i,n)) * t & 1 <= i & i <= n holds
||.(si - ti).|| <= K ) holds
||.(s - t).|| <= n * K
let s, t be Point of H1(m,n); ::_thesis: for K being Real st ( for i being Element of NAT
for si, ti being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))) st si = (Proj (i,n)) * s & ti = (Proj (i,n)) * t & 1 <= i & i <= n holds
||.(si - ti).|| <= K ) holds
||.(s - t).|| <= n * K
let K be Real; ::_thesis: ( ( for i being Element of NAT
for si, ti being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))) st si = (Proj (i,n)) * s & ti = (Proj (i,n)) * t & 1 <= i & i <= n holds
||.(si - ti).|| <= K ) implies ||.(s - t).|| <= n * K )
assume A1: for i being Element of NAT
for si, ti being Point of H1(m,1) st si = (Proj (i,n)) * s & ti = (Proj (i,n)) * t & 1 <= i & i <= n holds
||.(si - ti).|| <= K ; ::_thesis: ||.(s - t).|| <= n * K
now__::_thesis:_for_i_being_Element_of_NAT_
for_sti_being_Point_of_H1(m,1)_st_sti_=_(Proj_(i,n))_*_(s_-_t)_&_1_<=_i_&_i_<=_n_holds_
||.sti.||_<=_K
let i be Element of NAT ; ::_thesis: for sti being Point of H1(m,1) st sti = (Proj (i,n)) * (s - t) & 1 <= i & i <= n holds
||.sti.|| <= K
let sti be Point of H1(m,1); ::_thesis: ( sti = (Proj (i,n)) * (s - t) & 1 <= i & i <= n implies ||.sti.|| <= K )
assume A2: ( sti = (Proj (i,n)) * (s - t) & 1 <= i & i <= n ) ; ::_thesis: ||.sti.|| <= K
reconsider si = (Proj (i,n)) * s, ti = (Proj (i,n)) * t as Point of H1(m,1) by Th7, A2;
 si - ti = sti by A2, Lm1;
hence  ||.sti.|| <= K by A2, A1; ::_thesis: verum
end;
hence  ||.(s - t).|| <= n * K by Th18; ::_thesis: verum
end;

theorem Th20: :: PDIFF_8:20
for m, n being non empty Element of NAT
for f being PartFunc of (REAL-NS m),(REAL-NS n)
for X being Subset of (REAL-NS m)
for i being Element of NAT st 1 <= i & i <= m & X is open holds
( ( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) iff for j being Element of NAT st 1 <= j & j <= n holds
( (Proj (j,n)) * f is_partial_differentiable_on X,i & ((Proj (j,n)) * f) `partial| (X,i) is_continuous_on X ) )
proof
let m, n be non empty Element of NAT ; ::_thesis: for f being PartFunc of (REAL-NS m),(REAL-NS n)
for X being Subset of (REAL-NS m)
for i being Element of NAT st 1 <= i & i <= m & X is open holds
( ( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) iff for j being Element of NAT st 1 <= j & j <= n holds
( (Proj (j,n)) * f is_partial_differentiable_on X,i & ((Proj (j,n)) * f) `partial| (X,i) is_continuous_on X ) )
let f be PartFunc of (REAL-NS m),(REAL-NS n); ::_thesis: for X being Subset of (REAL-NS m)
for i being Element of NAT st 1 <= i & i <= m & X is open holds
( ( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) iff for j being Element of NAT st 1 <= j & j <= n holds
( (Proj (j,n)) * f is_partial_differentiable_on X,i & ((Proj (j,n)) * f) `partial| (X,i) is_continuous_on X ) )
let X be Subset of (REAL-NS m); ::_thesis: for i being Element of NAT st 1 <= i & i <= m & X is open holds
( ( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) iff for j being Element of NAT st 1 <= j & j <= n holds
( (Proj (j,n)) * f is_partial_differentiable_on X,i & ((Proj (j,n)) * f) `partial| (X,i) is_continuous_on X ) )
let i be Element of NAT ; ::_thesis: ( 1 <= i & i <= m & X is open implies ( ( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) iff for j being Element of NAT st 1 <= j & j <= n holds
( (Proj (j,n)) * f is_partial_differentiable_on X,i & ((Proj (j,n)) * f) `partial| (X,i) is_continuous_on X ) ) )
assume A1: ( 1 <= i & i <= m & X is open ) ; ::_thesis: ( ( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) iff for j being Element of NAT st 1 <= j & j <= n holds
( (Proj (j,n)) * f is_partial_differentiable_on X,i & ((Proj (j,n)) * f) `partial| (X,i) is_continuous_on X ) )
hereby  ::_thesis: ( ( for j being Element of NAT st 1 <= j & j <= n holds
( (Proj (j,n)) * f is_partial_differentiable_on X,i & ((Proj (j,n)) * f) `partial| (X,i) is_continuous_on X ) ) implies ( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) )
assume A2: ( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) ; ::_thesis: for j being Element of NAT st 1 <= j & j <= n holds
( (Proj (j,n)) * f is_partial_differentiable_on X,i & ((Proj (j,n)) * f) `partial| (X,i) is_continuous_on X )
then A3: X c= dom f by A1, PDIFF_7:8;
thus  for j being Element of NAT st 1 <= j & j <= n holds
( (Proj (j,n)) * f is_partial_differentiable_on X,i & ((Proj (j,n)) * f) `partial| (X,i) is_continuous_on X ) ::_thesis: verum
proof
let j be Element of NAT ; ::_thesis: ( 1 <= j & j <= n implies ( (Proj (j,n)) * f is_partial_differentiable_on X,i & ((Proj (j,n)) * f) `partial| (X,i) is_continuous_on X ) )
assume A4: ( 1 <= j & j <= n ) ; ::_thesis: ( (Proj (j,n)) * f is_partial_differentiable_on X,i & ((Proj (j,n)) * f) `partial| (X,i) is_continuous_on X )
A5: dom (Proj (j,n)) = the carrier of (REAL-NS n) by FUNCT_2:def_1;
 rng f c= the carrier of (REAL-NS n) ;
then A6: X c= dom ((Proj (j,n)) * f) by A5, A3, RELAT_1:27;
now__::_thesis:_for_x0_being_Point_of_(REAL-NS_m)_st_x0_in_X_holds_
(Proj_(j,n))_*_f_is_partial_differentiable_in_x0,i
let x0 be Point of (REAL-NS m); ::_thesis: ( x0 in X implies (Proj (j,n)) * f is_partial_differentiable_in x0,i )
assume  x0 in X ; ::_thesis: (Proj (j,n)) * f is_partial_differentiable_in x0,i
then  f is_partial_differentiable_in x0,i by A2, A1, PDIFF_7:8;
then  f * (reproj (i,x0)) is_differentiable_in (Proj (i,m)) . x0 by PDIFF_1:def_9;
then  (Proj (j,n)) * (f * (reproj (i,x0))) is_differentiable_in (Proj (i,m)) . x0 by A4, PDIFF_6:29;
then  ((Proj (j,n)) * f) * (reproj (i,x0)) is_differentiable_in (Proj (i,m)) . x0 by RELAT_1:36;
hence  (Proj (j,n)) * f is_partial_differentiable_in x0,i by PDIFF_1:def_9; ::_thesis: verum
end;
hence A7: (Proj (j,n)) * f is_partial_differentiable_on X,i by A6, A1, PDIFF_7:8; ::_thesis: ((Proj (j,n)) * f) `partial| (X,i) is_continuous_on X
then A8: X c= dom (((Proj (j,n)) * f) `partial| (X,i)) by PDIFF_1:def_20;
A9: for x0 being Point of (REAL-NS m) st x0 in X holds
(((Proj (j,n)) * f) `partial| (X,i)) /. x0 = (Proj (j,n)) * ((f `partial| (X,i)) /. x0)
proof
let x0 be Point of (REAL-NS m); ::_thesis: ( x0 in X implies (((Proj (j,n)) * f) `partial| (X,i)) /. x0 = (Proj (j,n)) * ((f `partial| (X,i)) /. x0) )
assume A10: x0 in X ; ::_thesis: (((Proj (j,n)) * f) `partial| (X,i)) /. x0 = (Proj (j,n)) * ((f `partial| (X,i)) /. x0)
then  f is_partial_differentiable_in x0,i by A2, A1, PDIFF_7:8;
then A11: f * (reproj (i,x0)) is_differentiable_in (Proj (i,m)) . x0 by PDIFF_1:def_9;
thus (((Proj (j,n)) * f) `partial| (X,i)) /. x0 = partdiff (((Proj (j,n)) * f),x0,i) by A7, A10, PDIFF_1:def_20
.= diff ((((Proj (j,n)) * f) * (reproj (i,x0))),((Proj (i,m)) . x0)) by PDIFF_1:def_10
.= diff (((Proj (j,n)) * (f * (reproj (i,x0)))),((Proj (i,m)) . x0)) by RELAT_1:36
.= (Proj (j,n)) * (diff ((f * (reproj (i,x0))),((Proj (i,m)) . x0))) by A11, A4, PDIFF_6:28
.= (Proj (j,n)) * (partdiff (f,x0,i)) by PDIFF_1:def_10
.= (Proj (j,n)) * ((f `partial| (X,i)) /. x0) by A2, A10, PDIFF_1:def_20 ; ::_thesis: verum
end;
 for x0 being Point of (REAL-NS m)
for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of (REAL-NS m) st x1 in X & ||.(x1 - x0).|| < s holds
||.(((((Proj (j,n)) * f) `partial| (X,i)) /. x1) - ((((Proj (j,n)) * f) `partial| (X,i)) /. x0)).|| < r ) )
proof
let x0 be Point of (REAL-NS m); ::_thesis: for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of (REAL-NS m) st x1 in X & ||.(x1 - x0).|| < s holds
||.(((((Proj (j,n)) * f) `partial| (X,i)) /. x1) - ((((Proj (j,n)) * f) `partial| (X,i)) /. x0)).|| < r ) )
let r be Real; ::_thesis: ( x0 in X & 0 < r implies ex s being Real st
( 0 < s & ( for x1 being Point of (REAL-NS m) st x1 in X & ||.(x1 - x0).|| < s holds
||.(((((Proj (j,n)) * f) `partial| (X,i)) /. x1) - ((((Proj (j,n)) * f) `partial| (X,i)) /. x0)).|| < r ) ) )
assume A12: ( x0 in X & 0 < r ) ; ::_thesis: ex s being Real st
( 0 < s & ( for x1 being Point of (REAL-NS m) st x1 in X & ||.(x1 - x0).|| < s holds
||.(((((Proj (j,n)) * f) `partial| (X,i)) /. x1) - ((((Proj (j,n)) * f) `partial| (X,i)) /. x0)).|| < r ) )
then consider s being Real such that
A13: ( 0 < s & ( for x1 being Point of (REAL-NS m) st x1 in X & ||.(x1 - x0).|| < s holds
||.(((f `partial| (X,i)) /. x1) - ((f `partial| (X,i)) /. x0)).|| < r ) ) by A2, NFCONT_1:19;
take  s ; ::_thesis: ( 0 < s & ( for x1 being Point of (REAL-NS m) st x1 in X & ||.(x1 - x0).|| < s holds
||.(((((Proj (j,n)) * f) `partial| (X,i)) /. x1) - ((((Proj (j,n)) * f) `partial| (X,i)) /. x0)).|| < r ) )
thus  0 < s by A13; ::_thesis: for x1 being Point of (REAL-NS m) st x1 in X & ||.(x1 - x0).|| < s holds
||.(((((Proj (j,n)) * f) `partial| (X,i)) /. x1) - ((((Proj (j,n)) * f) `partial| (X,i)) /. x0)).|| < r
let x1 be Point of (REAL-NS m); ::_thesis: ( x1 in X & ||.(x1 - x0).|| < s implies ||.(((((Proj (j,n)) * f) `partial| (X,i)) /. x1) - ((((Proj (j,n)) * f) `partial| (X,i)) /. x0)).|| < r )
assume A14: ( x1 in X & ||.(x1 - x0).|| < s ) ; ::_thesis: ||.(((((Proj (j,n)) * f) `partial| (X,i)) /. x1) - ((((Proj (j,n)) * f) `partial| (X,i)) /. x0)).|| < r
then A15: ||.(((f `partial| (X,i)) /. x1) - ((f `partial| (X,i)) /. x0)).|| < r by A13;
A16: (((Proj (j,n)) * f) `partial| (X,i)) /. x0 = (Proj (j,n)) * ((f `partial| (X,i)) /. x0) by A9, A12;
reconsider p1 = (Proj (j,n)) * ((f `partial| (X,i)) /. x1) as Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))) by Th7, A4;
reconsider p0 = (Proj (j,n)) * ((f `partial| (X,i)) /. x0) as Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))) by Th7, A4;
 ||.(((((Proj (j,n)) * f) `partial| (X,i)) /. x1) - ((((Proj (j,n)) * f) `partial| (X,i)) /. x0)).|| = ||.(p1 - p0).|| by A9, A14, A16;
then  ||.(((((Proj (j,n)) * f) `partial| (X,i)) /. x1) - ((((Proj (j,n)) * f) `partial| (X,i)) /. x0)).|| <= ||.(((f `partial| (X,i)) /. x1) - ((f `partial| (X,i)) /. x0)).|| by Th14, A4;
hence  ||.(((((Proj (j,n)) * f) `partial| (X,i)) /. x1) - ((((Proj (j,n)) * f) `partial| (X,i)) /. x0)).|| < r by A15, XXREAL_0:2; ::_thesis: verum
end;
hence  ((Proj (j,n)) * f) `partial| (X,i) is_continuous_on X by A8, NFCONT_1:19; ::_thesis: verum
end;
end;
assume A17: for j being Element of NAT st 1 <= j & j <= n holds
( (Proj (j,n)) * f is_partial_differentiable_on X,i & ((Proj (j,n)) * f) `partial| (X,i) is_continuous_on X ) ; ::_thesis: ( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X )
 1 <= n by NAT_1:14;
then  (Proj (1,n)) * f is_partial_differentiable_on X,i by A17;
then A18: X c= dom ((Proj (1,n)) * f) by PDIFF_1:def_19;
A19: dom (Proj (1,n)) = the carrier of (REAL-NS n) by FUNCT_2:def_1;
 rng f c= the carrier of (REAL-NS n) ;
then A20: X c= dom f by A18, A19, RELAT_1:27;
A21: now__::_thesis:_for_x0_being_Point_of_(REAL-NS_m)_st_x0_in_X_holds_
f_is_partial_differentiable_in_x0,i
let x0 be Point of (REAL-NS m); ::_thesis: ( x0 in X implies f is_partial_differentiable_in x0,i )
assume A22: x0 in X ; ::_thesis: f is_partial_differentiable_in x0,i
now__::_thesis:_for_j_being_Element_of_NAT_st_1_<=_j_&_j_<=_n_holds_
(Proj_(j,n))_*_(f_*_(reproj_(i,x0)))_is_differentiable_in_(Proj_(i,m))_._x0
let j be Element of NAT ; ::_thesis: ( 1 <= j & j <= n implies (Proj (j,n)) * (f * (reproj (i,x0))) is_differentiable_in (Proj (i,m)) . x0 )
assume  ( 1 <= j & j <= n ) ; ::_thesis: (Proj (j,n)) * (f * (reproj (i,x0))) is_differentiable_in (Proj (i,m)) . x0
then  (Proj (j,n)) * f is_partial_differentiable_on X,i by A17;
then  (Proj (j,n)) * f is_partial_differentiable_in x0,i by A22, A1, PDIFF_7:8;
then  ((Proj (j,n)) * f) * (reproj (i,x0)) is_differentiable_in (Proj (i,m)) . x0 by PDIFF_1:def_9;
hence  (Proj (j,n)) * (f * (reproj (i,x0))) is_differentiable_in (Proj (i,m)) . x0 by RELAT_1:36; ::_thesis: verum
end;
then  f * (reproj (i,x0)) is_differentiable_in (Proj (i,m)) . x0 by PDIFF_6:29;
hence  f is_partial_differentiable_in x0,i by PDIFF_1:def_9; ::_thesis: verum
end;
hence A23: f is_partial_differentiable_on X,i by A1, A20, PDIFF_7:8; ::_thesis: f `partial| (X,i) is_continuous_on X
then A24: X c= dom (f `partial| (X,i)) by PDIFF_1:def_20;
A25: for x0 being Point of (REAL-NS m)
for j being Element of NAT st x0 in X & 1 <= j & j <= n holds
(Proj (j,n)) * ((f `partial| (X,i)) /. x0) = (((Proj (j,n)) * f) `partial| (X,i)) /. x0
proof
let x0 be Point of (REAL-NS m); ::_thesis: for j being Element of NAT st x0 in X & 1 <= j & j <= n holds
(Proj (j,n)) * ((f `partial| (X,i)) /. x0) = (((Proj (j,n)) * f) `partial| (X,i)) /. x0
let j be Element of NAT ; ::_thesis: ( x0 in X & 1 <= j & j <= n implies (Proj (j,n)) * ((f `partial| (X,i)) /. x0) = (((Proj (j,n)) * f) `partial| (X,i)) /. x0 )
assume A26: ( x0 in X & 1 <= j & j <= n ) ; ::_thesis: (Proj (j,n)) * ((f `partial| (X,i)) /. x0) = (((Proj (j,n)) * f) `partial| (X,i)) /. x0
then  f is_partial_differentiable_in x0,i by A21;
then A27: f * (reproj (i,x0)) is_differentiable_in (Proj (i,m)) . x0 by PDIFF_1:def_9;
A28: (Proj (j,n)) * f is_partial_differentiable_on X,i by A17, A26;
thus (Proj (j,n)) * ((f `partial| (X,i)) /. x0) = (Proj (j,n)) * (partdiff (f,x0,i)) by A26, A23, PDIFF_1:def_20
.= (Proj (j,n)) * (diff ((f * (reproj (i,x0))),((Proj (i,m)) . x0))) by PDIFF_1:def_10
.= diff (((Proj (j,n)) * (f * (reproj (i,x0)))),((Proj (i,m)) . x0)) by A27, A26, PDIFF_6:28
.= diff ((((Proj (j,n)) * f) * (reproj (i,x0))),((Proj (i,m)) . x0)) by RELAT_1:36
.= partdiff (((Proj (j,n)) * f),x0,i) by PDIFF_1:def_10
.= (((Proj (j,n)) * f) `partial| (X,i)) /. x0 by A28, A26, PDIFF_1:def_20 ; ::_thesis: verum
end;
 for x0 being Point of (REAL-NS m)
for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of (REAL-NS m) st x1 in X & ||.(x1 - x0).|| < s holds
||.(((f `partial| (X,i)) /. x1) - ((f `partial| (X,i)) /. x0)).|| < r ) )
proof
let x0 be Point of (REAL-NS m); ::_thesis: for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of (REAL-NS m) st x1 in X & ||.(x1 - x0).|| < s holds
||.(((f `partial| (X,i)) /. x1) - ((f `partial| (X,i)) /. x0)).|| < r ) )
let r0 be Real; ::_thesis: ( x0 in X & 0 < r0 implies ex s being Real st
( 0 < s & ( for x1 being Point of (REAL-NS m) st x1 in X & ||.(x1 - x0).|| < s holds
||.(((f `partial| (X,i)) /. x1) - ((f `partial| (X,i)) /. x0)).|| < r0 ) ) )
assume A29: ( x0 in X & 0 < r0 ) ; ::_thesis: ex s being Real st
( 0 < s & ( for x1 being Point of (REAL-NS m) st x1 in X & ||.(x1 - x0).|| < s holds
||.(((f `partial| (X,i)) /. x1) - ((f `partial| (X,i)) /. x0)).|| < r0 ) )
set r = r0 / 2;
defpred S1[ set , set ] means  ex j being Element of NAT ex sj being Real st
( $2 = sj & $1 = j & 0 < sj & ( for x1 being Point of (REAL-NS m) st x1 in X & ||.(x1 - x0).|| < sj holds
||.(((((Proj (j,n)) * f) `partial| (X,i)) /. x1) - ((((Proj (j,n)) * f) `partial| (X,i)) /. x0)).|| < (r0 / 2) / n ) );
A30: for j0 being Nat st j0 in Seg n holds
ex x being Element of REAL st S1[j0,x]
proof
let j0 be Nat; ::_thesis: ( j0 in Seg n implies ex x being Element of REAL st S1[j0,x] )
assume  j0 in Seg n ; ::_thesis: ex x being Element of REAL st S1[j0,x]
then A31: ( 1 <= j0 & j0 <= n ) by FINSEQ_1:1;
reconsider j = j0 as Element of NAT by ORDINAL1:def_12;
 ((Proj (j,n)) * f) `partial| (X,i) is_continuous_on X by A17, A31;
then consider sj being Real such that
A32: ( 0 < sj & ( for x1 being Point of (REAL-NS m) st x1 in X & ||.(x1 - x0).|| < sj holds
||.(((((Proj (j,n)) * f) `partial| (X,i)) /. x1) - ((((Proj (j,n)) * f) `partial| (X,i)) /. x0)).|| < (r0 / 2) / n ) ) by A29, NFCONT_1:19;
thus  ex x being Element of REAL st S1[j0,x] by A32; ::_thesis: verum
end;
consider s0 being FinSequence of REAL  such that
A33: ( dom s0 = Seg n & ( for k being Nat st k in Seg n holds
S1[k,s0 . k] ) ) from FINSEQ_1:sch_5(A30);
A34: rng s0 is finite by A33, FINSET_1:8;
 n in Seg n by FINSEQ_1:3;
then reconsider rs0 = rng s0 as non empty ext-real-membered set by A33, FUNCT_1:3;
reconsider rs0 = rs0 as non empty ext-real-membered left_end right_end set by A34;
A35: min rs0 in rng s0 by XXREAL_2:def_7;
then reconsider s = min rs0 as Real ;
take  s ; ::_thesis: ( 0 < s & ( for x1 being Point of (REAL-NS m) st x1 in X & ||.(x1 - x0).|| < s holds
||.(((f `partial| (X,i)) /. x1) - ((f `partial| (X,i)) /. x0)).|| < r0 ) )
consider i1 being set  such that
A36: ( i1 in dom s0 & s = s0 . i1 ) by A35, FUNCT_1:def_3;
 ex j being Element of NAT ex sj being Real st
( s0 . i1 = sj & i1 = j & 0 < sj & ( for x1 being Point of (REAL-NS m) st x1 in X & ||.(x1 - x0).|| < sj holds
||.(((((Proj (j,n)) * f) `partial| (X,i)) /. x1) - ((((Proj (j,n)) * f) `partial| (X,i)) /. x0)).|| < (r0 / 2) / n ) ) by A33, A36;
hence  0 < s by A36; ::_thesis: for x1 being Point of (REAL-NS m) st x1 in X & ||.(x1 - x0).|| < s holds
||.(((f `partial| (X,i)) /. x1) - ((f `partial| (X,i)) /. x0)).|| < r0
let x1 be Point of (REAL-NS m); ::_thesis: ( x1 in X & ||.(x1 - x0).|| < s implies ||.(((f `partial| (X,i)) /. x1) - ((f `partial| (X,i)) /. x0)).|| < r0 )
assume A37: ( x1 in X & ||.(x1 - x0).|| < s ) ; ::_thesis: ||.(((f `partial| (X,i)) /. x1) - ((f `partial| (X,i)) /. x0)).|| < r0
now__::_thesis:_for_j_being_Element_of_NAT_
for_p1,_p0_being_Point_of_(R_NormSpace_of_BoundedLinearOperators_((REAL-NS_1),(REAL-NS_1)))_st_p1_=_(Proj_(j,n))_*_((f_`partial|_(X,i))_/._x1)_&_p0_=_(Proj_(j,n))_*_((f_`partial|_(X,i))_/._x0)_&_1_<=_j_&_j_<=_n_holds_
||.(p1_-_p0).||_<=_(r0_/_2)_/_n
let j be Element of NAT ; ::_thesis: for p1, p0 being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))) st p1 = (Proj (j,n)) * ((f `partial| (X,i)) /. x1) & p0 = (Proj (j,n)) * ((f `partial| (X,i)) /. x0) & 1 <= j & j <= n holds
||.(p1 - p0).|| <= (r0 / 2) / n
let p1, p0 be Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))); ::_thesis: ( p1 = (Proj (j,n)) * ((f `partial| (X,i)) /. x1) & p0 = (Proj (j,n)) * ((f `partial| (X,i)) /. x0) & 1 <= j & j <= n implies ||.(p1 - p0).|| <= (r0 / 2) / n )
assume A38: ( p1 = (Proj (j,n)) * ((f `partial| (X,i)) /. x1) & p0 = (Proj (j,n)) * ((f `partial| (X,i)) /. x0) & 1 <= j & j <= n ) ; ::_thesis: ||.(p1 - p0).|| <= (r0 / 2) / n
then A39: j in Seg n ;
then consider jj being Element of NAT , sj being Real such that
A40: ( s0 . j = sj & jj = j & 0 < sj & ( for x1 being Point of (REAL-NS m) st x1 in X & ||.(x1 - x0).|| < sj holds
||.(((((Proj (jj,n)) * f) `partial| (X,i)) /. x1) - ((((Proj (jj,n)) * f) `partial| (X,i)) /. x0)).|| < (r0 / 2) / n ) ) by A33;
A41: (Proj (j,n)) * ((f `partial| (X,i)) /. x0) = (((Proj (j,n)) * f) `partial| (X,i)) /. x0 by A25, A29, A38;
A42: (Proj (j,n)) * ((f `partial| (X,i)) /. x1) = (((Proj (j,n)) * f) `partial| (X,i)) /. x1 by A25, A37, A38;
 sj in rng s0 by A39, A40, A33, FUNCT_1:3;
then  s <= sj by XXREAL_2:def_7;
then  ||.(x1 - x0).|| < sj by A37, XXREAL_0:2;
hence  ||.(p1 - p0).|| <= (r0 / 2) / n by A40, A37, A38, A41, A42; ::_thesis: verum
end;
then  ||.(((f `partial| (X,i)) /. x1) - ((f `partial| (X,i)) /. x0)).|| <= n * ((r0 / 2) / n) by Th19;
then A43: ||.(((f `partial| (X,i)) /. x1) - ((f `partial| (X,i)) /. x0)).|| <= r0 / 2 by XCMPLX_1:87;
 r0 / 2 < r0 by A29, XREAL_1:216;
hence  ||.(((f `partial| (X,i)) /. x1) - ((f `partial| (X,i)) /. x0)).|| < r0 by A43, XXREAL_0:2; ::_thesis: verum
end;
hence  f `partial| (X,i) is_continuous_on X by A24, NFCONT_1:19; ::_thesis: verum
end;

theorem Th21: :: PDIFF_8:21
for m, n being non empty Element of NAT
for f being PartFunc of (REAL-NS m),(REAL-NS n)
for X being Subset of (REAL-NS m) st X is open holds
( ( f is_differentiable_on X & f `| X is_continuous_on X ) iff for j being Element of NAT st 1 <= j & j <= n holds
( (Proj (j,n)) * f is_differentiable_on X & ((Proj (j,n)) * f) `| X is_continuous_on X ) )
proof
let m, n be non empty Element of NAT ; ::_thesis: for f being PartFunc of (REAL-NS m),(REAL-NS n)
for X being Subset of (REAL-NS m) st X is open holds
( ( f is_differentiable_on X & f `| X is_continuous_on X ) iff for j being Element of NAT st 1 <= j & j <= n holds
( (Proj (j,n)) * f is_differentiable_on X & ((Proj (j,n)) * f) `| X is_continuous_on X ) )
let f be PartFunc of (REAL-NS m),(REAL-NS n); ::_thesis: for X being Subset of (REAL-NS m) st X is open holds
( ( f is_differentiable_on X & f `| X is_continuous_on X ) iff for j being Element of NAT st 1 <= j & j <= n holds
( (Proj (j,n)) * f is_differentiable_on X & ((Proj (j,n)) * f) `| X is_continuous_on X ) )
let X be Subset of (REAL-NS m); ::_thesis: ( X is open implies ( ( f is_differentiable_on X & f `| X is_continuous_on X ) iff for j being Element of NAT st 1 <= j & j <= n holds
( (Proj (j,n)) * f is_differentiable_on X & ((Proj (j,n)) * f) `| X is_continuous_on X ) ) )
assume A1: X is open ; ::_thesis: ( ( f is_differentiable_on X & f `| X is_continuous_on X ) iff for j being Element of NAT st 1 <= j & j <= n holds
( (Proj (j,n)) * f is_differentiable_on X & ((Proj (j,n)) * f) `| X is_continuous_on X ) )
hereby  ::_thesis: ( ( for j being Element of NAT st 1 <= j & j <= n holds
( (Proj (j,n)) * f is_differentiable_on X & ((Proj (j,n)) * f) `| X is_continuous_on X ) ) implies ( f is_differentiable_on X & f `| X is_continuous_on X ) )
assume A2: ( f is_differentiable_on X & f `| X is_continuous_on X ) ; ::_thesis: for j being Element of NAT st 1 <= j & j <= n holds
( (Proj (j,n)) * f is_differentiable_on X & ((Proj (j,n)) * f) `| X is_continuous_on X )
then A3: X c= dom f by A1, NDIFF_1:31;
thus  for j being Element of NAT st 1 <= j & j <= n holds
( (Proj (j,n)) * f is_differentiable_on X & ((Proj (j,n)) * f) `| X is_continuous_on X ) ::_thesis: verum
proof
let j be Element of NAT ; ::_thesis: ( 1 <= j & j <= n implies ( (Proj (j,n)) * f is_differentiable_on X & ((Proj (j,n)) * f) `| X is_continuous_on X ) )
assume A4: ( 1 <= j & j <= n ) ; ::_thesis: ( (Proj (j,n)) * f is_differentiable_on X & ((Proj (j,n)) * f) `| X is_continuous_on X )
A5: dom (Proj (j,n)) = the carrier of (REAL-NS n) by FUNCT_2:def_1;
 rng f c= the carrier of (REAL-NS n) ;
then A6: X c= dom ((Proj (j,n)) * f) by A3, A5, RELAT_1:27;
now__::_thesis:_for_x0_being_Point_of_(REAL-NS_m)_st_x0_in_X_holds_
(Proj_(j,n))_*_f_is_differentiable_in_x0
let x0 be Point of (REAL-NS m); ::_thesis: ( x0 in X implies (Proj (j,n)) * f is_differentiable_in x0 )
assume  x0 in X ; ::_thesis: (Proj (j,n)) * f is_differentiable_in x0
then  f is_differentiable_in x0 by A2, A1, NDIFF_1:31;
hence  (Proj (j,n)) * f is_differentiable_in x0 by A4, PDIFF_6:29; ::_thesis: verum
end;
hence A7: (Proj (j,n)) * f is_differentiable_on X by A6, A1, NDIFF_1:31; ::_thesis: ((Proj (j,n)) * f) `| X is_continuous_on X
then A8: X c= dom (((Proj (j,n)) * f) `| X) by NDIFF_1:def_9;
A9: for x0 being Point of (REAL-NS m) st x0 in X holds
(((Proj (j,n)) * f) `| X) /. x0 = (Proj (j,n)) * ((f `| X) /. x0)
proof
let x0 be Point of (REAL-NS m); ::_thesis: ( x0 in X implies (((Proj (j,n)) * f) `| X) /. x0 = (Proj (j,n)) * ((f `| X) /. x0) )
assume A10: x0 in X ; ::_thesis: (((Proj (j,n)) * f) `| X) /. x0 = (Proj (j,n)) * ((f `| X) /. x0)
then A11: f is_differentiable_in x0 by A2, A1, NDIFF_1:31;
thus (((Proj (j,n)) * f) `| X) /. x0 = diff (((Proj (j,n)) * f),x0) by A7, A10, NDIFF_1:def_9
.= (Proj (j,n)) * (diff (f,x0)) by A11, A4, PDIFF_6:28
.= (Proj (j,n)) * ((f `| X) /. x0) by A2, A10, NDIFF_1:def_9 ; ::_thesis: verum
end;
 for x0 being Point of (REAL-NS m)
for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of (REAL-NS m) st x1 in X & ||.(x1 - x0).|| < s holds
||.(((((Proj (j,n)) * f) `| X) /. x1) - ((((Proj (j,n)) * f) `| X) /. x0)).|| < r ) )
proof
let x0 be Point of (REAL-NS m); ::_thesis: for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of (REAL-NS m) st x1 in X & ||.(x1 - x0).|| < s holds
||.(((((Proj (j,n)) * f) `| X) /. x1) - ((((Proj (j,n)) * f) `| X) /. x0)).|| < r ) )
let r be Real; ::_thesis: ( x0 in X & 0 < r implies ex s being Real st
( 0 < s & ( for x1 being Point of (REAL-NS m) st x1 in X & ||.(x1 - x0).|| < s holds
||.(((((Proj (j,n)) * f) `| X) /. x1) - ((((Proj (j,n)) * f) `| X) /. x0)).|| < r ) ) )
assume A12: ( x0 in X & 0 < r ) ; ::_thesis: ex s being Real st
( 0 < s & ( for x1 being Point of (REAL-NS m) st x1 in X & ||.(x1 - x0).|| < s holds
||.(((((Proj (j,n)) * f) `| X) /. x1) - ((((Proj (j,n)) * f) `| X) /. x0)).|| < r ) )
then consider s being Real such that
A13: ( 0 < s & ( for x1 being Point of (REAL-NS m) st x1 in X & ||.(x1 - x0).|| < s holds
||.(((f `| X) /. x1) - ((f `| X) /. x0)).|| < r ) ) by A2, NFCONT_1:19;
take  s ; ::_thesis: ( 0 < s & ( for x1 being Point of (REAL-NS m) st x1 in X & ||.(x1 - x0).|| < s holds
||.(((((Proj (j,n)) * f) `| X) /. x1) - ((((Proj (j,n)) * f) `| X) /. x0)).|| < r ) )
thus  0 < s by A13; ::_thesis: for x1 being Point of (REAL-NS m) st x1 in X & ||.(x1 - x0).|| < s holds
||.(((((Proj (j,n)) * f) `| X) /. x1) - ((((Proj (j,n)) * f) `| X) /. x0)).|| < r
let x1 be Point of (REAL-NS m); ::_thesis: ( x1 in X & ||.(x1 - x0).|| < s implies ||.(((((Proj (j,n)) * f) `| X) /. x1) - ((((Proj (j,n)) * f) `| X) /. x0)).|| < r )
assume A14: ( x1 in X & ||.(x1 - x0).|| < s ) ; ::_thesis: ||.(((((Proj (j,n)) * f) `| X) /. x1) - ((((Proj (j,n)) * f) `| X) /. x0)).|| < r
then A15: ||.(((f `| X) /. x1) - ((f `| X) /. x0)).|| < r by A13;
A16: (((Proj (j,n)) * f) `| X) /. x0 = (Proj (j,n)) * ((f `| X) /. x0) by A9, A12;
reconsider p1 = (Proj (j,n)) * ((f `| X) /. x1) as Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))) by Th7, A4;
reconsider p0 = (Proj (j,n)) * ((f `| X) /. x0) as Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))) by Th7, A4;
 ||.(((((Proj (j,n)) * f) `| X) /. x1) - ((((Proj (j,n)) * f) `| X) /. x0)).|| = ||.(p1 - p0).|| by A9, A14, A16;
then  ||.(((((Proj (j,n)) * f) `| X) /. x1) - ((((Proj (j,n)) * f) `| X) /. x0)).|| <= ||.(((f `| X) /. x1) - ((f `| X) /. x0)).|| by Th14, A4;
hence  ||.(((((Proj (j,n)) * f) `| X) /. x1) - ((((Proj (j,n)) * f) `| X) /. x0)).|| < r by A15, XXREAL_0:2; ::_thesis: verum
end;
hence  ((Proj (j,n)) * f) `| X is_continuous_on X by A8, NFCONT_1:19; ::_thesis: verum
end;
end;
assume A17: for j being Element of NAT st 1 <= j & j <= n holds
( (Proj (j,n)) * f is_differentiable_on X & ((Proj (j,n)) * f) `| X is_continuous_on X ) ; ::_thesis: ( f is_differentiable_on X & f `| X is_continuous_on X )
 1 <= n by NAT_1:14;
then  (Proj (1,n)) * f is_differentiable_on X by A17;
then A18: X c= dom ((Proj (1,n)) * f) by A1, NDIFF_1:31;
A19: dom (Proj (1,n)) = the carrier of (REAL-NS n) by FUNCT_2:def_1;
 rng f c= the carrier of (REAL-NS n) ;
then A20: X c= dom f by A18, A19, RELAT_1:27;
A21: now__::_thesis:_for_x0_being_Point_of_(REAL-NS_m)_st_x0_in_X_holds_
f_is_differentiable_in_x0
let x0 be Point of (REAL-NS m); ::_thesis: ( x0 in X implies f is_differentiable_in x0 )
assume A22: x0 in X ; ::_thesis: f is_differentiable_in x0
now__::_thesis:_for_j_being_Element_of_NAT_st_1_<=_j_&_j_<=_n_holds_
(Proj_(j,n))_*_f_is_differentiable_in_x0
let j be Element of NAT ; ::_thesis: ( 1 <= j & j <= n implies (Proj (j,n)) * f is_differentiable_in x0 )
assume  ( 1 <= j & j <= n ) ; ::_thesis: (Proj (j,n)) * f is_differentiable_in x0
then  (Proj (j,n)) * f is_differentiable_on X by A17;
hence  (Proj (j,n)) * f is_differentiable_in x0 by A22, A1, NDIFF_1:31; ::_thesis: verum
end;
hence  f is_differentiable_in x0 by PDIFF_6:29; ::_thesis: verum
end;
hence A23: f is_differentiable_on X by A1, A20, NDIFF_1:31; ::_thesis: f `| X is_continuous_on X
then A24: X c= dom (f `| X) by NDIFF_1:def_9;
A25: for x0 being Point of (REAL-NS m)
for j being Element of NAT st x0 in X & 1 <= j & j <= n holds
(Proj (j,n)) * ((f `| X) /. x0) = (((Proj (j,n)) * f) `| X) /. x0
proof
let x0 be Point of (REAL-NS m); ::_thesis: for j being Element of NAT st x0 in X & 1 <= j & j <= n holds
(Proj (j,n)) * ((f `| X) /. x0) = (((Proj (j,n)) * f) `| X) /. x0
let j be Element of NAT ; ::_thesis: ( x0 in X & 1 <= j & j <= n implies (Proj (j,n)) * ((f `| X) /. x0) = (((Proj (j,n)) * f) `| X) /. x0 )
assume A26: ( x0 in X & 1 <= j & j <= n ) ; ::_thesis: (Proj (j,n)) * ((f `| X) /. x0) = (((Proj (j,n)) * f) `| X) /. x0
then A27: f is_differentiable_in x0 by A21;
A28: (Proj (j,n)) * f is_differentiable_on X by A17, A26;
thus (Proj (j,n)) * ((f `| X) /. x0) = (Proj (j,n)) * (diff (f,x0)) by A26, A23, NDIFF_1:def_9
.= diff (((Proj (j,n)) * f),x0) by A27, A26, PDIFF_6:28
.= (((Proj (j,n)) * f) `| X) /. x0 by A28, A26, NDIFF_1:def_9 ; ::_thesis: verum
end;
 for x0 being Point of (REAL-NS m)
for r0 being Real st x0 in X & 0 < r0 holds
ex s being Real st
( 0 < s & ( for x1 being Point of (REAL-NS m) st x1 in X & ||.(x1 - x0).|| < s holds
||.(((f `| X) /. x1) - ((f `| X) /. x0)).|| < r0 ) )
proof
let x0 be Point of (REAL-NS m); ::_thesis: for r0 being Real st x0 in X & 0 < r0 holds
ex s being Real st
( 0 < s & ( for x1 being Point of (REAL-NS m) st x1 in X & ||.(x1 - x0).|| < s holds
||.(((f `| X) /. x1) - ((f `| X) /. x0)).|| < r0 ) )
let r0 be Real; ::_thesis: ( x0 in X & 0 < r0 implies ex s being Real st
( 0 < s & ( for x1 being Point of (REAL-NS m) st x1 in X & ||.(x1 - x0).|| < s holds
||.(((f `| X) /. x1) - ((f `| X) /. x0)).|| < r0 ) ) )
assume A29: ( x0 in X & 0 < r0 ) ; ::_thesis: ex s being Real st
( 0 < s & ( for x1 being Point of (REAL-NS m) st x1 in X & ||.(x1 - x0).|| < s holds
||.(((f `| X) /. x1) - ((f `| X) /. x0)).|| < r0 ) )
set r = r0 / 2;
defpred S1[ set , set ] means  ex j being Element of NAT ex sj being Real st
( $2 = sj & $1 = j & 0 < sj & ( for x1 being Point of (REAL-NS m) st x1 in X & ||.(x1 - x0).|| < sj holds
||.(((((Proj (j,n)) * f) `| X) /. x1) - ((((Proj (j,n)) * f) `| X) /. x0)).|| < (r0 / 2) / n ) );
A30: for j0 being Nat st j0 in Seg n holds
ex x being Element of REAL st S1[j0,x]
proof
let j0 be Nat; ::_thesis: ( j0 in Seg n implies ex x being Element of REAL st S1[j0,x] )
assume  j0 in Seg n ; ::_thesis: ex x being Element of REAL st S1[j0,x]
then A31: ( 1 <= j0 & j0 <= n ) by FINSEQ_1:1;
reconsider j = j0 as Element of NAT by ORDINAL1:def_12;
 ((Proj (j,n)) * f) `| X is_continuous_on X by A17, A31;
then consider sj being Real such that
A32: ( 0 < sj & ( for x1 being Point of (REAL-NS m) st x1 in X & ||.(x1 - x0).|| < sj holds
||.(((((Proj (j,n)) * f) `| X) /. x1) - ((((Proj (j,n)) * f) `| X) /. x0)).|| < (r0 / 2) / n ) ) by A29, NFCONT_1:19;
thus  ex x being Element of REAL st S1[j0,x] by A32; ::_thesis: verum
end;
consider s0 being FinSequence of REAL  such that
A33: ( dom s0 = Seg n & ( for k being Nat st k in Seg n holds
S1[k,s0 . k] ) ) from FINSEQ_1:sch_5(A30);
A34: rng s0 is finite by A33, FINSET_1:8;
 n in Seg n by FINSEQ_1:3;
then reconsider rs0 = rng s0 as non empty ext-real-membered set by A33, FUNCT_1:3;
reconsider rs0 = rs0 as non empty ext-real-membered left_end right_end set by A34;
A35: min rs0 in rng s0 by XXREAL_2:def_7;
then reconsider s = min rs0 as Real ;
take  s ; ::_thesis: ( 0 < s & ( for x1 being Point of (REAL-NS m) st x1 in X & ||.(x1 - x0).|| < s holds
||.(((f `| X) /. x1) - ((f `| X) /. x0)).|| < r0 ) )
consider i1 being set  such that
A36: ( i1 in dom s0 & s = s0 . i1 ) by A35, FUNCT_1:def_3;
 ex j being Element of NAT ex sj being Real st
( s0 . i1 = sj & i1 = j & 0 < sj & ( for x1 being Point of (REAL-NS m) st x1 in X & ||.(x1 - x0).|| < sj holds
||.(((((Proj (j,n)) * f) `| X) /. x1) - ((((Proj (j,n)) * f) `| X) /. x0)).|| < (r0 / 2) / n ) ) by A33, A36;
hence  0 < s by A36; ::_thesis: for x1 being Point of (REAL-NS m) st x1 in X & ||.(x1 - x0).|| < s holds
||.(((f `| X) /. x1) - ((f `| X) /. x0)).|| < r0
let x1 be Point of (REAL-NS m); ::_thesis: ( x1 in X & ||.(x1 - x0).|| < s implies ||.(((f `| X) /. x1) - ((f `| X) /. x0)).|| < r0 )
assume A37: ( x1 in X & ||.(x1 - x0).|| < s ) ; ::_thesis: ||.(((f `| X) /. x1) - ((f `| X) /. x0)).|| < r0
now__::_thesis:_for_j_being_Element_of_NAT_
for_p1,_p0_being_Point_of_(R_NormSpace_of_BoundedLinearOperators_((REAL-NS_m),(REAL-NS_1)))_st_p1_=_(Proj_(j,n))_*_((f_`|_X)_/._x1)_&_p0_=_(Proj_(j,n))_*_((f_`|_X)_/._x0)_&_1_<=_j_&_j_<=_n_holds_
||.(p1_-_p0).||_<=_(r0_/_2)_/_n
let j be Element of NAT ; ::_thesis: for p1, p0 being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))) st p1 = (Proj (j,n)) * ((f `| X) /. x1) & p0 = (Proj (j,n)) * ((f `| X) /. x0) & 1 <= j & j <= n holds
||.(p1 - p0).|| <= (r0 / 2) / n
let p1, p0 be Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))); ::_thesis: ( p1 = (Proj (j,n)) * ((f `| X) /. x1) & p0 = (Proj (j,n)) * ((f `| X) /. x0) & 1 <= j & j <= n implies ||.(p1 - p0).|| <= (r0 / 2) / n )
assume A38: ( p1 = (Proj (j,n)) * ((f `| X) /. x1) & p0 = (Proj (j,n)) * ((f `| X) /. x0) & 1 <= j & j <= n ) ; ::_thesis: ||.(p1 - p0).|| <= (r0 / 2) / n
then A39: j in Seg n ;
then consider jj being Element of NAT , sj being Real such that
A40: ( s0 . j = sj & jj = j & 0 < sj & ( for x1 being Point of (REAL-NS m) st x1 in X & ||.(x1 - x0).|| < sj holds
||.(((((Proj (jj,n)) * f) `| X) /. x1) - ((((Proj (jj,n)) * f) `| X) /. x0)).|| < (r0 / 2) / n ) ) by A33;
A41: (Proj (j,n)) * ((f `| X) /. x0) = (((Proj (j,n)) * f) `| X) /. x0 by A25, A29, A38;
A42: (Proj (j,n)) * ((f `| X) /. x1) = (((Proj (j,n)) * f) `| X) /. x1 by A25, A37, A38;
 sj in rng s0 by A39, A40, A33, FUNCT_1:3;
then  s <= sj by XXREAL_2:def_7;
then  ||.(x1 - x0).|| < sj by A37, XXREAL_0:2;
hence  ||.(p1 - p0).|| <= (r0 / 2) / n by A40, A37, A38, A41, A42; ::_thesis: verum
end;
then  ||.(((f `| X) /. x1) - ((f `| X) /. x0)).|| <= n * ((r0 / 2) / n) by Th19;
then A43: ||.(((f `| X) /. x1) - ((f `| X) /. x0)).|| <= r0 / 2 by XCMPLX_1:87;
 r0 / 2 < r0 by A29, XREAL_1:216;
hence  ||.(((f `| X) /. x1) - ((f `| X) /. x0)).|| < r0 by A43, XXREAL_0:2; ::_thesis: verum
end;
hence  f `| X is_continuous_on X by A24, NFCONT_1:19; ::_thesis: verum
end;

theorem :: PDIFF_8:22
for m, n being non empty Element of NAT
for f being PartFunc of (REAL-NS m),(REAL-NS n)
for X being Subset of (REAL-NS m) st X is open holds
( ( for i being Element of 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 ) )
proof
let m, n be non empty Element of NAT ; ::_thesis: for f being PartFunc of (REAL-NS m),(REAL-NS n)
for X being Subset of (REAL-NS m) st X is open holds
( ( for i being Element of 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 n); ::_thesis: for X being Subset of (REAL-NS m) st X is open holds
( ( for i being Element of 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 Element of 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 Element of 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 Element of 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 Element of 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 )
now__::_thesis:_for_j_being_Element_of_NAT_st_1_<=_j_&_j_<=_n_holds_
(_(Proj_(j,n))_*_f_is_differentiable_on_X_&_((Proj_(j,n))_*_f)_`|_X_is_continuous_on_X_)
let j be Element of NAT ; ::_thesis: ( 1 <= j & j <= n implies ( (Proj (j,n)) * f is_differentiable_on X & ((Proj (j,n)) * f) `| X is_continuous_on X ) )
assume A3: ( 1 <= j & j <= n ) ; ::_thesis: ( (Proj (j,n)) * f is_differentiable_on X & ((Proj (j,n)) * f) `| X is_continuous_on X )
now__::_thesis:_for_i_being_Element_of_NAT_st_1_<=_i_&_i_<=_m_holds_
(_(Proj_(j,n))_*_f_is_partial_differentiable_on_X,i_&_((Proj_(j,n))_*_f)_`partial|_(X,i)_is_continuous_on_X_)
let i be Element of NAT ; ::_thesis: ( 1 <= i & i <= m implies ( (Proj (j,n)) * f is_partial_differentiable_on X,i & ((Proj (j,n)) * f) `partial| (X,i) is_continuous_on X ) )
assume A4: ( 1 <= i & i <= m ) ; ::_thesis: ( (Proj (j,n)) * f is_partial_differentiable_on X,i & ((Proj (j,n)) * f) `partial| (X,i) is_continuous_on X )
then  ( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) by A2;
hence  ( (Proj (j,n)) * f is_partial_differentiable_on X,i & ((Proj (j,n)) * f) `partial| (X,i) is_continuous_on X ) by Th20, A1, A3, A4; ::_thesis: verum
end;
hence  ( (Proj (j,n)) * f is_differentiable_on X & ((Proj (j,n)) * f) `| X is_continuous_on X ) by A1, PDIFF_7:49; ::_thesis: verum
end;
hence  ( f is_differentiable_on X & f `| X is_continuous_on X ) by A1, Th21; ::_thesis: verum
end;
assume A5: ( f is_differentiable_on X & f `| X is_continuous_on X ) ; ::_thesis: for i being Element of NAT st 1 <= i & i <= m holds
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X )
let i be Element of NAT ; ::_thesis: ( 1 <= i & i <= m implies ( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) )
assume A6: ( 1 <= i & i <= m ) ; ::_thesis: ( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X )
now__::_thesis:_for_j_being_Element_of_NAT_st_1_<=_j_&_j_<=_n_holds_
(_(Proj_(j,n))_*_f_is_partial_differentiable_on_X,i_&_((Proj_(j,n))_*_f)_`partial|_(X,i)_is_continuous_on_X_)
let j be Element of NAT ; ::_thesis: ( 1 <= j & j <= n implies ( (Proj (j,n)) * f is_partial_differentiable_on X,i & ((Proj (j,n)) * f) `partial| (X,i) is_continuous_on X ) )
assume  ( 1 <= j & j <= n ) ; ::_thesis: ( (Proj (j,n)) * f is_partial_differentiable_on X,i & ((Proj (j,n)) * f) `partial| (X,i) is_continuous_on X )
then  ( (Proj (j,n)) * f is_differentiable_on X & ((Proj (j,n)) * f) `| X is_continuous_on X ) by A1, A5, Th21;
hence  ( (Proj (j,n)) * f is_partial_differentiable_on X,i & ((Proj (j,n)) * f) `partial| (X,i) is_continuous_on X ) by A1, A6, PDIFF_7:49; ::_thesis: verum
end;
hence  ( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) by A6, A1, Th20; ::_thesis: verum
end;