:: 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;