:: PDIFF_6 semantic presentation begin theorem Th1: :: PDIFF_6:1 for m, n being Element of NAT for f being set holds ( f is PartFunc of (REAL m),(REAL n) iff f is PartFunc of (REAL-NS m),(REAL-NS n) ) proof let m, n be Element of NAT ; ::_thesis: for f being set holds ( f is PartFunc of (REAL m),(REAL n) iff f is PartFunc of (REAL-NS m),(REAL-NS n) ) let f be set ; ::_thesis: ( f is PartFunc of (REAL m),(REAL n) iff f is PartFunc of (REAL-NS m),(REAL-NS n) ) ( the carrier of (REAL-NS m) = REAL m & the carrier of (REAL-NS n) = REAL n ) by REAL_NS1:def_4; hence ( f is PartFunc of (REAL m),(REAL n) iff f is PartFunc of (REAL-NS m),(REAL-NS n) ) ; ::_thesis: verum end; theorem Th2: :: PDIFF_6:2 for n, m being non empty Element of NAT for f being PartFunc of (REAL m),(REAL n) for g being PartFunc of (REAL-NS m),(REAL-NS n) for x being Element of REAL m for y being Point of (REAL-NS m) st f = g & x = y holds ( f is_differentiable_in x iff g is_differentiable_in y ) proof let n, m be non empty Element of NAT ; ::_thesis: for f being PartFunc of (REAL m),(REAL n) for g being PartFunc of (REAL-NS m),(REAL-NS n) for x being Element of REAL m for y being Point of (REAL-NS m) st f = g & x = y holds ( f is_differentiable_in x iff g is_differentiable_in y ) let f be PartFunc of (REAL m),(REAL n); ::_thesis: for g being PartFunc of (REAL-NS m),(REAL-NS n) for x being Element of REAL m for y being Point of (REAL-NS m) st f = g & x = y holds ( f is_differentiable_in x iff g is_differentiable_in y ) let g be PartFunc of (REAL-NS m),(REAL-NS n); ::_thesis: for x being Element of REAL m for y being Point of (REAL-NS m) st f = g & x = y holds ( f is_differentiable_in x iff g is_differentiable_in y ) let x be Element of REAL m; ::_thesis: for y being Point of (REAL-NS m) st f = g & x = y holds ( f is_differentiable_in x iff g is_differentiable_in y ) let y be Point of (REAL-NS m); ::_thesis: ( f = g & x = y implies ( f is_differentiable_in x iff g is_differentiable_in y ) ) assume A1: ( f = g & x = y ) ; ::_thesis: ( f is_differentiable_in x iff g is_differentiable_in y ) hereby ::_thesis: ( g is_differentiable_in y implies f is_differentiable_in x ) assume f is_differentiable_in x ; ::_thesis: g is_differentiable_in y then ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st ( f = g & x = y & g is_differentiable_in y ) by PDIFF_1:def_7; hence g is_differentiable_in y by A1; ::_thesis: verum end; assume g is_differentiable_in y ; ::_thesis: f is_differentiable_in x hence f is_differentiable_in x by A1, PDIFF_1:def_7; ::_thesis: verum end; theorem Th3: :: PDIFF_6:3 for n, m being non empty Element of NAT for f being PartFunc of (REAL m),(REAL n) for g being PartFunc of (REAL-NS m),(REAL-NS n) for x being Element of REAL m for y being Point of (REAL-NS m) st f = g & x = y & f is_differentiable_in x holds diff (f,x) = diff (g,y) proof let n, m be non empty Element of NAT ; ::_thesis: for f being PartFunc of (REAL m),(REAL n) for g being PartFunc of (REAL-NS m),(REAL-NS n) for x being Element of REAL m for y being Point of (REAL-NS m) st f = g & x = y & f is_differentiable_in x holds diff (f,x) = diff (g,y) let f be PartFunc of (REAL m),(REAL n); ::_thesis: for g being PartFunc of (REAL-NS m),(REAL-NS n) for x being Element of REAL m for y being Point of (REAL-NS m) st f = g & x = y & f is_differentiable_in x holds diff (f,x) = diff (g,y) let g be PartFunc of (REAL-NS m),(REAL-NS n); ::_thesis: for x being Element of REAL m for y being Point of (REAL-NS m) st f = g & x = y & f is_differentiable_in x holds diff (f,x) = diff (g,y) let x be Element of REAL m; ::_thesis: for y being Point of (REAL-NS m) st f = g & x = y & f is_differentiable_in x holds diff (f,x) = diff (g,y) let y be Point of (REAL-NS m); ::_thesis: ( f = g & x = y & f is_differentiable_in x implies diff (f,x) = diff (g,y) ) assume A1: ( f = g & x = y & f is_differentiable_in x ) ; ::_thesis: diff (f,x) = diff (g,y) then ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st ( f = g & x = y & diff (f,x) = diff (g,y) ) by PDIFF_1:def_8; hence diff (f,x) = diff (g,y) by A1; ::_thesis: verum end; theorem Th4: :: PDIFF_6:4 for m, n being Element of NAT for f1, f2 being PartFunc of (REAL m),(REAL n) for g1, g2 being PartFunc of (REAL-NS m),(REAL-NS n) st f1 = g1 & f2 = g2 holds f1 + f2 = g1 + g2 proof let m, n be Element of NAT ; ::_thesis: for f1, f2 being PartFunc of (REAL m),(REAL n) for g1, g2 being PartFunc of (REAL-NS m),(REAL-NS n) st f1 = g1 & f2 = g2 holds f1 + f2 = g1 + g2 let f1, f2 be PartFunc of (REAL m),(REAL n); ::_thesis: for g1, g2 being PartFunc of (REAL-NS m),(REAL-NS n) st f1 = g1 & f2 = g2 holds f1 + f2 = g1 + g2 let g1, g2 be PartFunc of (REAL-NS m),(REAL-NS n); ::_thesis: ( f1 = g1 & f2 = g2 implies f1 + f2 = g1 + g2 ) assume A1: ( f1 = g1 & f2 = g2 ) ; ::_thesis: f1 + f2 = g1 + g2 ( the carrier of (REAL-NS m) = REAL m & the carrier of (REAL-NS n) = REAL n ) by REAL_NS1:def_4; then reconsider g12 = g1 + g2 as PartFunc of (REAL m),(REAL n) ; A2: (dom f1) /\ (dom f2) = dom g12 by A1, VFUNCT_1:def_1; A3: f1 <++> f2 = f1 + f2 by INTEGR15:def_9; for c being set st c in dom g12 holds (g1 + g2) . c = (f1 . c) + (f2 . c) proof let c be set ; ::_thesis: ( c in dom g12 implies (g1 + g2) . c = (f1 . c) + (f2 . c) ) assume A4: c in dom g12 ; ::_thesis: (g1 + g2) . c = (f1 . c) + (f2 . c) then A5: c in dom (g1 + g2) ; ( c in dom f1 & c in dom f2 ) by A2, A4, XBOOLE_0:def_4; then A6: ( f1 /. c = f1 . c & f2 /. c = f2 . c ) by PARTFUN1:def_6; A7: ( f1 /. c = g1 /. c & f2 /. c = g2 /. c ) by A1, REAL_NS1:def_4; g12 . c = (g1 + g2) /. c by A4, PARTFUN1:def_6 .= (g1 /. c) + (g2 /. c) by A5, VFUNCT_1:def_1 ; hence (g1 + g2) . c = (f1 . c) + (f2 . c) by A6, A7, REAL_NS1:2; ::_thesis: verum end; hence f1 + f2 = g1 + g2 by A2, A3, VALUED_2:def_45; ::_thesis: verum end; theorem Th5: :: PDIFF_6:5 for m, n being Element of NAT for f1, f2 being PartFunc of (REAL m),(REAL n) for g1, g2 being PartFunc of (REAL-NS m),(REAL-NS n) st f1 = g1 & f2 = g2 holds f1 - f2 = g1 - g2 proof let m, n be Element of NAT ; ::_thesis: for f1, f2 being PartFunc of (REAL m),(REAL n) for g1, g2 being PartFunc of (REAL-NS m),(REAL-NS n) st f1 = g1 & f2 = g2 holds f1 - f2 = g1 - g2 let f1, f2 be PartFunc of (REAL m),(REAL n); ::_thesis: for g1, g2 being PartFunc of (REAL-NS m),(REAL-NS n) st f1 = g1 & f2 = g2 holds f1 - f2 = g1 - g2 let g1, g2 be PartFunc of (REAL-NS m),(REAL-NS n); ::_thesis: ( f1 = g1 & f2 = g2 implies f1 - f2 = g1 - g2 ) assume A1: ( f1 = g1 & f2 = g2 ) ; ::_thesis: f1 - f2 = g1 - g2 ( the carrier of (REAL-NS m) = REAL m & the carrier of (REAL-NS n) = REAL n ) by REAL_NS1:def_4; then reconsider g12 = g1 - g2 as PartFunc of (REAL m),(REAL n) ; A2: (dom f1) /\ (dom f2) = dom g12 by A1, VFUNCT_1:def_2; A3: f1 <--> f2 = f1 - f2 by INTEGR15:def_10; for c being set st c in dom g12 holds (g1 - g2) . c = (f1 . c) - (f2 . c) proof let c be set ; ::_thesis: ( c in dom g12 implies (g1 - g2) . c = (f1 . c) - (f2 . c) ) assume A4: c in dom g12 ; ::_thesis: (g1 - g2) . c = (f1 . c) - (f2 . c) then A5: c in dom (g1 - g2) ; ( c in dom f1 & c in dom f2 ) by A2, A4, XBOOLE_0:def_4; then A6: ( f1 /. c = f1 . c & f2 /. c = f2 . c ) by PARTFUN1:def_6; A7: ( f1 /. c = g1 /. c & f2 /. c = g2 /. c ) by A1, REAL_NS1:def_4; g12 . c = (g1 - g2) /. c by A4, PARTFUN1:def_6 .= (g1 /. c) - (g2 /. c) by A5, VFUNCT_1:def_2 ; hence (g1 - g2) . c = (f1 . c) - (f2 . c) by A6, A7, REAL_NS1:5; ::_thesis: verum end; hence f1 - f2 = g1 - g2 by A2, A3, VALUED_2:def_46; ::_thesis: verum end; theorem Th6: :: PDIFF_6:6 for m, n being Element of NAT for f being PartFunc of (REAL m),(REAL n) for g being PartFunc of (REAL-NS m),(REAL-NS n) for a being Real st f = g holds a (#) f = a (#) g proof let m, n be Element of NAT ; ::_thesis: for f being PartFunc of (REAL m),(REAL n) for g being PartFunc of (REAL-NS m),(REAL-NS n) for a being Real st f = g holds a (#) f = a (#) g let f be PartFunc of (REAL m),(REAL n); ::_thesis: for g being PartFunc of (REAL-NS m),(REAL-NS n) for a being Real st f = g holds a (#) f = a (#) g let g be PartFunc of (REAL-NS m),(REAL-NS n); ::_thesis: for a being Real st f = g holds a (#) f = a (#) g let a be Real; ::_thesis: ( f = g implies a (#) f = a (#) g ) assume A1: f = g ; ::_thesis: a (#) f = a (#) g ( the carrier of (REAL-NS m) = REAL m & the carrier of (REAL-NS n) = REAL n ) by REAL_NS1:def_4; then reconsider aG = a (#) g as PartFunc of (REAL m),(REAL n) ; A2: dom f = dom aG by A1, VFUNCT_1:def_4; A3: a (#) f = f [#] a by INTEGR15:def_11; for c being set st c in dom aG holds aG . c = a (#) (f . c) proof let c be set ; ::_thesis: ( c in dom aG implies aG . c = a (#) (f . c) ) assume A4: c in dom aG ; ::_thesis: aG . c = a (#) (f . c) then A5: c in dom (a (#) g) ; A6: f /. c = g /. c by A1, REAL_NS1:def_4; A7: f /. c = f . c by A2, A4, PARTFUN1:def_6; aG . c = (a (#) g) /. c by A4, PARTFUN1:def_6 .= a * (g /. c) by A5, VFUNCT_1:def_4 ; hence aG . c = a (#) (f . c) by A6, A7, REAL_NS1:3; ::_thesis: verum end; hence a (#) f = a (#) g by A2, A3, VALUED_2:def_39; ::_thesis: verum end; theorem Th7: :: PDIFF_6:7 for m, n being Element of NAT for f1, f2 being Function of (REAL m),(REAL n) for g1, g2 being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))) st f1 = g1 & f2 = g2 holds f1 + f2 = g1 + g2 proof let m, n be Element of NAT ; ::_thesis: for f1, f2 being Function of (REAL m),(REAL n) for g1, g2 being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))) st f1 = g1 & f2 = g2 holds f1 + f2 = g1 + g2 let f1, f2 be Function of (REAL m),(REAL n); ::_thesis: for g1, g2 being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))) st f1 = g1 & f2 = g2 holds f1 + f2 = g1 + g2 let g1, g2 be Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))); ::_thesis: ( f1 = g1 & f2 = g2 implies f1 + f2 = g1 + g2 ) assume A1: ( f1 = g1 & f2 = g2 ) ; ::_thesis: f1 + f2 = g1 + g2 A2: ( the carrier of (REAL-NS m) = REAL m & the carrier of (REAL-NS n) = REAL n ) by REAL_NS1:def_4; then reconsider g12 = g1 + g2 as Function of (REAL m),(REAL n) by LOPBAN_1:def_9; ( g1 is LinearOperator of (REAL-NS m),(REAL-NS n) & g2 is LinearOperator of (REAL-NS m),(REAL-NS n) ) by LOPBAN_1:def_9; then ( dom g1 = REAL m & dom g2 = REAL m ) by A2, FUNCT_2:def_1; then A3: (dom f1) /\ (dom f2) = dom g12 by A1, FUNCT_2:def_1; A4: f1 <++> f2 = f1 + f2 by INTEGR15:def_9; for c being set st c in dom g12 holds g12 . c = (f1 . c) + (f2 . c) proof let c be set ; ::_thesis: ( c in dom g12 implies g12 . c = (f1 . c) + (f2 . c) ) assume A5: c in dom g12 ; ::_thesis: g12 . c = (f1 . c) + (f2 . c) then reconsider x = c as VECTOR of (REAL-NS m) by REAL_NS1:def_4; reconsider c1 = c as Element of REAL m by A5; g12 . x = (g1 . x) + (g2 . x) by LOPBAN_1:35; hence g12 . c = (f1 /. c1) + (f2 /. c1) by A1, REAL_NS1:2 .= (f1 . c) + (f2 . c) ; ::_thesis: verum end; hence f1 + f2 = g1 + g2 by A3, A4, VALUED_2:def_45; ::_thesis: verum end; theorem Th8: :: PDIFF_6:8 for m, n being Element of NAT for f1, f2 being Function of (REAL m),(REAL n) for g1, g2 being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))) st f1 = g1 & f2 = g2 holds f1 - f2 = g1 - g2 proof let m, n be Element of NAT ; ::_thesis: for f1, f2 being Function of (REAL m),(REAL n) for g1, g2 being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))) st f1 = g1 & f2 = g2 holds f1 - f2 = g1 - g2 let f1, f2 be Function of (REAL m),(REAL n); ::_thesis: for g1, g2 being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))) st f1 = g1 & f2 = g2 holds f1 - f2 = g1 - g2 let g1, g2 be Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))); ::_thesis: ( f1 = g1 & f2 = g2 implies f1 - f2 = g1 - g2 ) assume A1: ( f1 = g1 & f2 = g2 ) ; ::_thesis: f1 - f2 = g1 - g2 A2: ( the carrier of (REAL-NS m) = REAL m & the carrier of (REAL-NS n) = REAL n ) by REAL_NS1:def_4; then reconsider g12 = g1 - g2 as Function of (REAL m),(REAL n) by LOPBAN_1:def_9; ( g1 is LinearOperator of (REAL-NS m),(REAL-NS n) & g2 is LinearOperator of (REAL-NS m),(REAL-NS n) ) by LOPBAN_1:def_9; then ( dom g1 = REAL m & dom g2 = REAL m ) by A2, FUNCT_2:def_1; then A3: (dom f1) /\ (dom f2) = dom g12 by A1, FUNCT_2:def_1; A4: f1 <--> f2 = f1 - f2 by INTEGR15:def_10; for c being set st c in dom g12 holds g12 . c = (f1 . c) - (f2 . c) proof let c be set ; ::_thesis: ( c in dom g12 implies g12 . c = (f1 . c) - (f2 . c) ) assume A5: c in dom g12 ; ::_thesis: g12 . c = (f1 . c) - (f2 . c) then reconsider x = c as VECTOR of (REAL-NS m) by REAL_NS1:def_4; reconsider c1 = c as Element of REAL m by A5; g12 . x = (g1 . x) - (g2 . x) by LOPBAN_1:40; hence g12 . c = (f1 /. c1) - (f2 /. c1) by A1, REAL_NS1:5 .= (f1 . c) - (f2 . c) ; ::_thesis: verum end; hence f1 - f2 = g1 - g2 by A3, A4, VALUED_2:def_46; ::_thesis: verum end; theorem Th9: :: PDIFF_6:9 for m, n being Element of NAT for f being Function of (REAL m),(REAL n) for g being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))) for r being Real st f = g holds r (#) f = r * g proof let m, n be Element of NAT ; ::_thesis: for f being Function of (REAL m),(REAL n) for g being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))) for r being Real st f = g holds r (#) f = r * g let f be Function of (REAL m),(REAL n); ::_thesis: for g being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))) for r being Real st f = g holds r (#) f = r * g let g be Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))); ::_thesis: for r being Real st f = g holds r (#) f = r * g let r be Real; ::_thesis: ( f = g implies r (#) f = r * g ) assume A1: f = g ; ::_thesis: r (#) f = r * g ( the carrier of (REAL-NS m) = REAL m & the carrier of (REAL-NS n) = REAL n ) by REAL_NS1:def_4; then reconsider rG = r * g as Function of (REAL m),(REAL n) by LOPBAN_1:def_9; dom f = REAL m by FUNCT_2:def_1; then A2: dom f = dom rG by FUNCT_2:def_1; A3: r (#) f = f [#] r by INTEGR15:def_11; for c being set st c in dom rG holds rG . c = r (#) (f . c) proof let c be set ; ::_thesis: ( c in dom rG implies rG . c = r (#) (f . c) ) assume A4: c in dom rG ; ::_thesis: rG . c = r (#) (f . c) then reconsider x = c as VECTOR of (REAL-NS m) by REAL_NS1:def_4; reconsider c1 = c as Element of REAL m by A4; rG . x = r * (g . x) by LOPBAN_1:36; hence rG . c = r * (f /. c1) by A1, REAL_NS1:3 .= r (#) (f . c) ; ::_thesis: verum end; hence r (#) f = r * g by A2, A3, VALUED_2:def_39; ::_thesis: verum end; theorem Th10: :: PDIFF_6:10 for m, n being non empty Element of NAT for f being PartFunc of (REAL m),(REAL n) for x being Element of REAL m st f is_differentiable_in x holds diff (f,x) is Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))) proof let m, n be non empty Element of NAT ; ::_thesis: for f being PartFunc of (REAL m),(REAL n) for x being Element of REAL m st f is_differentiable_in x holds diff (f,x) is Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))) let f be PartFunc of (REAL m),(REAL n); ::_thesis: for x being Element of REAL m st f is_differentiable_in x holds diff (f,x) is Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))) let x be Element of REAL m; ::_thesis: ( f is_differentiable_in x implies diff (f,x) is Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))) ) assume f is_differentiable_in x ; ::_thesis: diff (f,x) is Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))) then ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st ( f = g & x = y & diff (f,x) = diff (g,y) ) by PDIFF_1:def_8; hence diff (f,x) is Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))) ; ::_thesis: verum end; definition let n, m be Nat; let IT be Function of (REAL m),(REAL n); attrIT is additive means :Def1: :: PDIFF_6:def 1 for x, y being Element of REAL m holds IT . (x + y) = (IT . x) + (IT . y); attrIT is homogeneous means :Def2: :: PDIFF_6:def 2 for x being Element of REAL m for r being Real holds IT . (r * x) = r * (IT . x); end; :: deftheorem Def1 defines additive PDIFF_6:def_1_:_ for n, m being Nat for IT being Function of (REAL m),(REAL n) holds ( IT is additive iff for x, y being Element of REAL m holds IT . (x + y) = (IT . x) + (IT . y) ); :: deftheorem Def2 defines homogeneous PDIFF_6:def_2_:_ for n, m being Nat for IT being Function of (REAL m),(REAL n) holds ( IT is homogeneous iff for x being Element of REAL m for r being Real holds IT . (r * x) = r * (IT . x) ); theorem Th11: :: PDIFF_6:11 for m, n being Element of NAT for IT being Function of (REAL m),(REAL n) st IT is additive holds IT . (0* m) = 0* n proof let m, n be Element of NAT ; ::_thesis: for IT being Function of (REAL m),(REAL n) st IT is additive holds IT . (0* m) = 0* n let IT be Function of (REAL m),(REAL n); ::_thesis: ( IT is additive implies IT . (0* m) = 0* n ) assume A1: IT is additive ; ::_thesis: IT . (0* m) = 0* n IT . (0* m) = IT . ((0* m) + (0* m)) by RVSUM_1:16; then IT . (0* m) = (IT . (0* m)) + (IT . (0* m)) by A1, Def1; then 0* n = ((IT . (0* m)) + (IT . (0* m))) - (IT . (0* m)) by RVSUM_1:37; hence 0* n = IT . (0* m) by RVSUM_1:42; ::_thesis: verum end; theorem Th12: :: PDIFF_6:12 for m, n being Element of NAT for f being Function of (REAL m),(REAL n) for g being Function of (REAL-NS m),(REAL-NS n) st f = g holds ( f is additive iff g is additive ) proof let m, n be Element of NAT ; ::_thesis: for f being Function of (REAL m),(REAL n) for g being Function of (REAL-NS m),(REAL-NS n) st f = g holds ( f is additive iff g is additive ) let f be Function of (REAL m),(REAL n); ::_thesis: for g being Function of (REAL-NS m),(REAL-NS n) st f = g holds ( f is additive iff g is additive ) let g be Function of (REAL-NS m),(REAL-NS n); ::_thesis: ( f = g implies ( f is additive iff g is additive ) ) assume A1: f = g ; ::_thesis: ( f is additive iff g is additive ) hereby ::_thesis: ( g is additive implies f is additive ) assume A2: f is additive ; ::_thesis: g is additive now__::_thesis:_for_x,_y_being_Point_of_(REAL-NS_m)_holds_g_._(x_+_y)_=_(g_._x)_+_(g_._y) let x, y be Point of (REAL-NS m); ::_thesis: g . (x + y) = (g . x) + (g . y) reconsider x1 = x, y1 = y as Element of REAL m by REAL_NS1:def_4; g . (x + y) = f . (x1 + y1) by A1, REAL_NS1:2 .= (f . x1) + (f . y1) by A2, Def1 ; hence g . (x + y) = (g . x) + (g . y) by A1, REAL_NS1:2; ::_thesis: verum end; hence g is additive by VECTSP_1:def_20; ::_thesis: verum end; assume A3: g is additive ; ::_thesis: f is additive now__::_thesis:_for_x,_y_being_Element_of_REAL_m_holds_f_._(x_+_y)_=_(f_._x)_+_(f_._y) let x, y be Element of REAL m; ::_thesis: f . (x + y) = (f . x) + (f . y) reconsider x1 = x, y1 = y as Point of (REAL-NS m) by REAL_NS1:def_4; f . (x + y) = g . (x1 + y1) by A1, REAL_NS1:2 .= (g . x1) + (g . y1) by A3, VECTSP_1:def_20 ; hence f . (x + y) = (f . x) + (f . y) by A1, REAL_NS1:2; ::_thesis: verum end; hence f is additive by Def1; ::_thesis: verum end; theorem Th13: :: PDIFF_6:13 for m, n being Element of NAT for f being Function of (REAL m),(REAL n) for g being Function of (REAL-NS m),(REAL-NS n) st f = g holds ( f is homogeneous iff g is homogeneous ) proof let m, n be Element of NAT ; ::_thesis: for f being Function of (REAL m),(REAL n) for g being Function of (REAL-NS m),(REAL-NS n) st f = g holds ( f is homogeneous iff g is homogeneous ) let f be Function of (REAL m),(REAL n); ::_thesis: for g being Function of (REAL-NS m),(REAL-NS n) st f = g holds ( f is homogeneous iff g is homogeneous ) let g be Function of (REAL-NS m),(REAL-NS n); ::_thesis: ( f = g implies ( f is homogeneous iff g is homogeneous ) ) assume A1: f = g ; ::_thesis: ( f is homogeneous iff g is homogeneous ) hereby ::_thesis: ( g is homogeneous implies f is homogeneous ) assume A2: f is homogeneous ; ::_thesis: g is homogeneous now__::_thesis:_for_x_being_Point_of_(REAL-NS_m) for_r_being_Real_holds_g_._(r_*_x)_=_r_*_(g_._x) let x be Point of (REAL-NS m); ::_thesis: for r being Real holds g . (r * x) = r * (g . x) let r be Real; ::_thesis: g . (r * x) = r * (g . x) reconsider x1 = x as Element of REAL m by REAL_NS1:def_4; g . (r * x) = f . (r * x1) by A1, REAL_NS1:3 .= r * (f . x1) by A2, Def2 ; hence g . (r * x) = r * (g . x) by A1, REAL_NS1:3; ::_thesis: verum end; hence g is homogeneous by LOPBAN_1:def_5; ::_thesis: verum end; assume A3: g is homogeneous ; ::_thesis: f is homogeneous now__::_thesis:_for_x_being_Element_of_REAL_m for_r_being_Real_holds_f_._(r_*_x)_=_r_*_(f_._x) let x be Element of REAL m; ::_thesis: for r being Real holds f . (r * x) = r * (f . x) let r be Real; ::_thesis: f . (r * x) = r * (f . x) reconsider x1 = x as Point of (REAL-NS m) by REAL_NS1:def_4; f . (r * x) = g . (r * x1) by A1, REAL_NS1:3 .= r * (g . x1) by A3, LOPBAN_1:def_5 ; hence f . (r * x) = r * (f . x) by A1, REAL_NS1:3; ::_thesis: verum end; hence f is homogeneous by Def2; ::_thesis: verum end; registration let n, m be Nat; cluster(REAL m) --> (0* n) -> additive homogeneous for Function of (REAL m),(REAL n); coherence for b1 being Function of (REAL m),(REAL n) st b1 = (REAL m) --> (0* n) holds ( b1 is additive & b1 is homogeneous ) proof let f be Function of (REAL m),(REAL n); ::_thesis: ( f = (REAL m) --> (0* n) implies ( f is additive & f is homogeneous ) ) assume A1: f = (REAL m) --> (0* n) ; ::_thesis: ( f is additive & f is homogeneous ) reconsider n1 = n as Element of NAT by ORDINAL1:def_12; hereby :: according to PDIFF_6:def_1 ::_thesis: f is homogeneous let x, y be Element of REAL m; ::_thesis: f . (x + y) = (f . x) + (f . y) A2: 0. (REAL-NS n1) = 0* n by REAL_NS1:def_4; f . (x + y) = 0* n by A1, FUNCOP_1:7 .= 0. (REAL-NS n1) by REAL_NS1:def_4 .= (0. (REAL-NS n1)) + (0. (REAL-NS n1)) by RLVECT_1:4 .= (0* n) + (0* n) by A2, REAL_NS1:2 .= (f . x) + (0* n) by A1, FUNCOP_1:7 ; hence f . (x + y) = (f . x) + (f . y) by A1, FUNCOP_1:7; ::_thesis: verum end; hereby :: according to PDIFF_6:def_2 ::_thesis: verum let x be Element of REAL m; ::_thesis: for r being Real holds f . (r * x) = r * (f . x) let r be Real; ::_thesis: f . (r * x) = r * (f . x) A3: 0. (REAL-NS n1) = 0* n by REAL_NS1:def_4; f . (r * x) = 0* n by A1, FUNCOP_1:7 .= 0. (REAL-NS n1) by REAL_NS1:def_4 .= r * (0. (REAL-NS n1)) by RLVECT_1:10 .= r * (0* n) by A3, REAL_NS1:3 ; hence f . (r * x) = r * (f . x) by A1, FUNCOP_1:7; ::_thesis: verum end; end; end; registration let n, m be Nat; cluster non empty Relation-like REAL m -defined REAL n -valued Function-like total V30( REAL m, REAL n) complex-functions-valued ext-real-functions-valued real-functions-valued additive homogeneous for Element of K6(K7((REAL m),(REAL n))); existence ex b1 being Function of (REAL m),(REAL n) st ( b1 is additive & b1 is homogeneous ) proof take (REAL m) --> (0* n) ; ::_thesis: ( (REAL m) --> (0* n) is additive & (REAL m) --> (0* n) is homogeneous ) thus ( (REAL m) --> (0* n) is additive & (REAL m) --> (0* n) is homogeneous ) ; ::_thesis: verum end; end; definition let m, n be Nat; mode LinearOperator of m,n is additive homogeneous Function of (REAL m),(REAL n); end; theorem Th14: :: PDIFF_6:14 for m, n being Element of NAT for f being set holds ( f is LinearOperator of m,n iff f is LinearOperator of (REAL-NS m),(REAL-NS n) ) proof let m, n be Element of NAT ; ::_thesis: for f being set holds ( f is LinearOperator of m,n iff f is LinearOperator of (REAL-NS m),(REAL-NS n) ) let f be set ; ::_thesis: ( f is LinearOperator of m,n iff f is LinearOperator of (REAL-NS m),(REAL-NS n) ) ( REAL m = the carrier of (REAL-NS m) & REAL n = the carrier of (REAL-NS n) ) by REAL_NS1:def_4; hence ( f is additive homogeneous Function of (REAL m),(REAL n) iff f is additive homogeneous Function of (REAL-NS m),(REAL-NS n) ) by Th12, Th13; ::_thesis: verum end; definition let m, n be Nat; let IT be Function of (REAL m),(REAL n); let x be Element of REAL m; :: original: . redefine funcIT . x -> Element of REAL n; coherence IT . x is Element of REAL n proof IT . x is Element of REAL n ; hence IT . x is Element of REAL n ; ::_thesis: verum end; end; definition let m, n be Nat; let IT be Function of (REAL m),(REAL n); attrIT is Lipschitzian means :Def3: :: PDIFF_6:def 3 ex K being Real st ( 0 <= K & ( for x being Element of REAL m holds |.(IT . x).| <= K * |.x.| ) ); end; :: deftheorem Def3 defines Lipschitzian PDIFF_6:def_3_:_ for m, n being Nat for IT being Function of (REAL m),(REAL n) holds ( IT is Lipschitzian iff ex K being Real st ( 0 <= K & ( for x being Element of REAL m holds |.(IT . x).| <= K * |.x.| ) ) ); theorem Th15: :: PDIFF_6:15 for m being Element of NAT for xseq, yseq being FinSequence of REAL m st len xseq = (len yseq) + 1 & xseq | (len yseq) = yseq holds ex v being Element of REAL m st ( v = xseq . (len xseq) & Sum xseq = (Sum yseq) + v ) proof let m be Element of NAT ; ::_thesis: for xseq, yseq being FinSequence of REAL m st len xseq = (len yseq) + 1 & xseq | (len yseq) = yseq holds ex v being Element of REAL m st ( v = xseq . (len xseq) & Sum xseq = (Sum yseq) + v ) let xseq, yseq be FinSequence of REAL m; ::_thesis: ( len xseq = (len yseq) + 1 & xseq | (len yseq) = yseq implies ex v being Element of REAL m st ( v = xseq . (len xseq) & Sum xseq = (Sum yseq) + v ) ) assume A1: ( len xseq = (len yseq) + 1 & xseq | (len yseq) = yseq ) ; ::_thesis: ex v being Element of REAL m st ( v = xseq . (len xseq) & Sum xseq = (Sum yseq) + v ) A2: ( len xseq = len (accum xseq) & xseq . 1 = (accum xseq) . 1 & ( for k being Nat st 1 <= k & k < len xseq holds (accum xseq) . (k + 1) = ((accum xseq) /. k) + (xseq /. (k + 1)) ) ) by EUCLID_7:def_10; A3: Sum xseq = (accum xseq) . (len xseq) by A1, EUCLID_7:def_11; set g = accum xseq; set i = len yseq; percases ( len yseq = 0 or len yseq <> 0 ) ; supposeA4: len yseq = 0 ; ::_thesis: ex v being Element of REAL m st ( v = xseq . (len xseq) & Sum xseq = (Sum yseq) + v ) then reconsider v = xseq . (len xseq) as Element of REAL m by A1, A3, EUCLID_7:def_10; take v ; ::_thesis: ( v = xseq . (len xseq) & Sum xseq = (Sum yseq) + v ) Sum yseq = 0* m by A4, EUCLID_7:def_11; hence ( v = xseq . (len xseq) & Sum xseq = (Sum yseq) + v ) by A1, A2, A3, A4, RVSUM_1:16; ::_thesis: verum end; supposeA5: len yseq <> 0 ; ::_thesis: ex v being Element of REAL m st ( v = xseq . (len xseq) & Sum xseq = (Sum yseq) + v ) A6: ( len yseq = len (accum yseq) & yseq . 1 = (accum yseq) . 1 & ( for k being Nat st 1 <= k & k < len yseq holds (accum yseq) . (k + 1) = ((accum yseq) /. k) + (yseq /. (k + 1)) ) ) by EUCLID_7:def_10; A7: Sum yseq = (accum yseq) . (len yseq) by A5, EUCLID_7:def_11; set g0 = accum yseq; A8: len yseq <= len (accum xseq) by A1, A2, NAT_1:11; then A9: len ((accum xseq) | (len yseq)) = len yseq by FINSEQ_1:59; A10: for k being Nat st 1 <= k & k <= len ((accum xseq) | (len yseq)) holds ((accum xseq) | (len yseq)) . k = (accum yseq) . k proof defpred S1[ Nat] means ( 1 <= $1 & $1 <= len ((accum xseq) | (len yseq)) implies ((accum xseq) | (len yseq)) . $1 = (accum yseq) . $1 ); A11: S1[ 0 ] ; A12: now__::_thesis:_for_k_being_Nat_st_S1[k]_holds_ S1[k_+_1] let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A13: S1[k] ; ::_thesis: S1[k + 1] now__::_thesis:_(_1_<=_k_+_1_&_k_+_1_<=_len_((accum_xseq)_|_(len_yseq))_implies_((accum_xseq)_|_(len_yseq))_._(k_+_1)_=_(accum_yseq)_._(k_+_1)_) assume A14: ( 1 <= k + 1 & k + 1 <= len ((accum xseq) | (len yseq)) ) ; ::_thesis: ((accum xseq) | (len yseq)) . (k + 1) = (accum yseq) . (k + 1) then A15: k + 1 <= len yseq by A8, FINSEQ_1:59; then k + 1 in Seg (len yseq) by A14; then A16: ( ((accum xseq) | (len yseq)) . (k + 1) = (accum xseq) . (k + 1) & xseq . (k + 1) = (xseq | (Seg (len yseq))) . (k + 1) ) by FUNCT_1:49; A17: k < len yseq by A15, NAT_1:13; now__::_thesis:_(_k_<>_0_implies_((accum_xseq)_|_(len_yseq))_._(k_+_1)_=_(accum_yseq)_._(k_+_1)_) assume A18: k <> 0 ; ::_thesis: ((accum xseq) | (len yseq)) . (k + 1) = (accum yseq) . (k + 1) then A19: 1 <= k by NAT_1:14; then A20: k in Seg (len yseq) by A17, FINSEQ_1:1; len yseq <= len xseq by A1, NAT_1:12; then A21: k < len xseq by A17, XXREAL_0:2; then (accum xseq) /. k = (accum xseq) . k by A2, A19, FINSEQ_4:15; then (accum xseq) /. k = ((accum xseq) | (len yseq)) . k by A20, FUNCT_1:49; then A22: (accum xseq) /. k = (accum yseq) /. k by A6, A17, A19, A13, A14, FINSEQ_4:15, NAT_1:13; k + 1 <= len xseq by A15, A1, NAT_1:12; then xseq /. (k + 1) = xseq . (k + 1) by A14, FINSEQ_4:15; then xseq /. (k + 1) = yseq /. (k + 1) by A1, A14, A9, A16, FINSEQ_4:15; then ((accum xseq) /. k) + (xseq /. (k + 1)) = (accum yseq) . (k + 1) by A6, A17, A18, A22, NAT_1:14; hence ((accum xseq) | (len yseq)) . (k + 1) = (accum yseq) . (k + 1) by A2, A16, A18, A21, NAT_1:14; ::_thesis: verum end; hence ((accum xseq) | (len yseq)) . (k + 1) = (accum yseq) . (k + 1) by A1, A6, A16, EUCLID_7:def_10; ::_thesis: verum end; hence S1[k + 1] ; ::_thesis: verum end; thus for k being Nat holds S1[k] from NAT_1:sch_2(A11, A12); ::_thesis: verum end; 1 <= len yseq by A5, NAT_1:14; then len yseq in Seg (len yseq) ; then A23: len yseq in dom ((accum xseq) | (len yseq)) by A9, FINSEQ_1:def_3; then len yseq in dom (accum xseq) by RELAT_1:57; then (accum xseq) . (len yseq) = (accum xseq) /. (len yseq) by PARTFUN1:def_6; then ((accum xseq) | (len yseq)) . (len yseq) = (accum xseq) /. (len yseq) by A23, FUNCT_1:47; then A24: (accum yseq) . (len yseq) = (accum xseq) /. (len yseq) by A6, A9, A10, FINSEQ_1:14; dom xseq = Seg ((len yseq) + 1) by A1, FINSEQ_1:def_3; then xseq . (len xseq) in rng xseq by A1, FINSEQ_1:4, FUNCT_1:3; then reconsider v = xseq . (len xseq) as Element of REAL m ; take v ; ::_thesis: ( v = xseq . (len xseq) & Sum xseq = (Sum yseq) + v ) thus v = xseq . (len xseq) ; ::_thesis: Sum xseq = (Sum yseq) + v A25: len yseq < len xseq by A1, NAT_1:13; 1 <= (len yseq) + 1 by NAT_1:11; then ((accum xseq) /. (len yseq)) + (xseq /. ((len yseq) + 1)) = (Sum yseq) + v by A7, A24, A1, FINSEQ_4:15; hence Sum xseq = (Sum yseq) + v by A1, A25, A2, A3, A5, NAT_1:14; ::_thesis: verum end; end; end; theorem Th16: :: PDIFF_6:16 for m, n being Element of NAT for f being LinearOperator of m,n for xseq being FinSequence of REAL m for yseq being FinSequence of REAL n st len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds yseq . i = f . (xseq . i) ) holds Sum yseq = f . (Sum xseq) proof let m, n be Element of NAT ; ::_thesis: for f being LinearOperator of m,n for xseq being FinSequence of REAL m for yseq being FinSequence of REAL n st len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds yseq . i = f . (xseq . i) ) holds Sum yseq = f . (Sum xseq) let f be LinearOperator of m,n; ::_thesis: for xseq being FinSequence of REAL m for yseq being FinSequence of REAL n st len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds yseq . i = f . (xseq . i) ) holds Sum yseq = f . (Sum xseq) defpred S1[ Nat] means for xseq being FinSequence of REAL m for yseq being FinSequence of REAL n st $1 = len xseq & len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds yseq . i = f . (xseq . i) ) holds Sum yseq = f . (Sum xseq); A1: S1[ 0 ] proof let xseq be FinSequence of REAL m; ::_thesis: for yseq being FinSequence of REAL n st 0 = len xseq & len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds yseq . i = f . (xseq . i) ) holds Sum yseq = f . (Sum xseq) let yseq be FinSequence of REAL n; ::_thesis: ( 0 = len xseq & len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds yseq . i = f . (xseq . i) ) implies Sum yseq = f . (Sum xseq) ) assume ( 0 = len xseq & len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds yseq . i = f . (xseq . i) ) ) ; ::_thesis: Sum yseq = f . (Sum xseq) then ( Sum xseq = 0* m & Sum yseq = 0* n ) by EUCLID_7:def_11; hence Sum yseq = f . (Sum xseq) by Th11; ::_thesis: verum end; A2: now__::_thesis:_for_i_being_Element_of_NAT_st_S1[i]_holds_ S1[i_+_1] let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] ) assume A3: S1[i] ; ::_thesis: S1[i + 1] now__::_thesis:_for_xseq_being_FinSequence_of_REAL_m for_yseq_being_FinSequence_of_REAL_n_st_i_+_1_=_len_xseq_&_len_xseq_=_len_yseq_&_(_for_k_being_Element_of_NAT_st_k_in_dom_xseq_holds_ yseq_._k_=_f_._(xseq_._k)_)_holds_ Sum_yseq_=_f_._(Sum_xseq) let xseq be FinSequence of REAL m; ::_thesis: for yseq being FinSequence of REAL n st i + 1 = len xseq & len xseq = len yseq & ( for k being Element of NAT st k in dom xseq holds yseq . k = f . (xseq . k) ) holds Sum yseq = f . (Sum xseq) let yseq be FinSequence of REAL n; ::_thesis: ( i + 1 = len xseq & len xseq = len yseq & ( for k being Element of NAT st k in dom xseq holds yseq . k = f . (xseq . k) ) implies Sum yseq = f . (Sum xseq) ) assume A4: ( i + 1 = len xseq & len xseq = len yseq & ( for k being Element of NAT st k in dom xseq holds yseq . k = f . (xseq . k) ) ) ; ::_thesis: Sum yseq = f . (Sum xseq) set xseq0 = xseq | i; set yseq0 = yseq | i; A5: i = len (xseq | i) by A4, FINSEQ_1:59, NAT_1:11; then A6: len (xseq | i) = len (yseq | i) by A4, FINSEQ_1:59, NAT_1:11; for k being Element of NAT st k in dom (xseq | i) holds (yseq | i) . k = f . ((xseq | i) . k) proof let k be Element of NAT ; ::_thesis: ( k in dom (xseq | i) implies (yseq | i) . k = f . ((xseq | i) . k) ) assume A7: k in dom (xseq | i) ; ::_thesis: (yseq | i) . k = f . ((xseq | i) . k) then A8: k in Seg i by RELAT_1:57; k in dom xseq by A7, RELAT_1:57; then A9: yseq . k = f . (xseq . k) by A4; xseq . k = (xseq | i) . k by A8, FUNCT_1:49; hence (yseq | i) . k = f . ((xseq | i) . k) by A8, A9, FUNCT_1:49; ::_thesis: verum end; then A10: Sum (yseq | i) = f . (Sum (xseq | i)) by A5, A6, A3; consider v being Element of REAL m such that A11: ( v = xseq . (len xseq) & Sum xseq = (Sum (xseq | i)) + v ) by A4, A5, Th15; consider w being Element of REAL n such that A12: ( w = yseq . (len yseq) & Sum yseq = (Sum (yseq | i)) + w ) by A4, A5, A6, Th15; dom xseq = Seg (i + 1) by A4, FINSEQ_1:def_3; then w = f . v by A4, A12, A11, FINSEQ_1:4; hence Sum yseq = f . (Sum xseq) by A10, A11, A12, Def1; ::_thesis: verum end; hence S1[i + 1] ; ::_thesis: verum end; A13: for k being Element of NAT holds S1[k] from NAT_1:sch_1(A1, A2); let xseq be FinSequence of REAL m; ::_thesis: for yseq being FinSequence of REAL n st len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds yseq . i = f . (xseq . i) ) holds Sum yseq = f . (Sum xseq) let yseq be FinSequence of REAL n; ::_thesis: ( len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds yseq . i = f . (xseq . i) ) implies Sum yseq = f . (Sum xseq) ) assume ( len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds yseq . i = f . (xseq . i) ) ) ; ::_thesis: Sum yseq = f . (Sum xseq) hence Sum yseq = f . (Sum xseq) by A13; ::_thesis: verum end; theorem Th17: :: PDIFF_6:17 for m being Element of NAT for xseq being FinSequence of REAL m for yseq being FinSequence of REAL st len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds ex v being Element of REAL m st ( v = xseq . i & yseq . i = |.v.| ) ) holds |.(Sum xseq).| <= Sum yseq proof let m be Element of NAT ; ::_thesis: for xseq being FinSequence of REAL m for yseq being FinSequence of REAL st len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds ex v being Element of REAL m st ( v = xseq . i & yseq . i = |.v.| ) ) holds |.(Sum xseq).| <= Sum yseq defpred S1[ Nat] means for xseq being FinSequence of REAL m for yseq being FinSequence of REAL st $1 = len xseq & len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds ex v being Element of REAL m st ( v = xseq . i & yseq . i = |.v.| ) ) holds |.(Sum xseq).| <= Sum yseq; A1: S1[ 0 ] proof let xseq be FinSequence of REAL m; ::_thesis: for yseq being FinSequence of REAL st 0 = len xseq & len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds ex v being Element of REAL m st ( v = xseq . i & yseq . i = |.v.| ) ) holds |.(Sum xseq).| <= Sum yseq let yseq be FinSequence of REAL ; ::_thesis: ( 0 = len xseq & len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds ex v being Element of REAL m st ( v = xseq . i & yseq . i = |.v.| ) ) implies |.(Sum xseq).| <= Sum yseq ) assume ( 0 = len xseq & len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds ex v being Element of REAL m st ( v = xseq . i & yseq . i = |.v.| ) ) ) ; ::_thesis: |.(Sum xseq).| <= Sum yseq then ( Sum xseq = 0* m & <*> REAL = yseq ) by EUCLID_7:def_11; hence |.(Sum xseq).| <= Sum yseq by EUCLID:7, RVSUM_1:72; ::_thesis: verum end; A2: now__::_thesis:_for_i_being_Element_of_NAT_st_S1[i]_holds_ S1[i_+_1] let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] ) assume A3: S1[i] ; ::_thesis: S1[i + 1] now__::_thesis:_for_xseq_being_FinSequence_of_REAL_m for_yseq_being_FinSequence_of_REAL_st_i_+_1_=_len_xseq_&_len_xseq_=_len_yseq_&_(_for_i_being_Element_of_NAT_st_i_in_dom_xseq_holds_ ex_v_being_Element_of_REAL_m_st_ (_v_=_xseq_._i_&_yseq_._i_=_|.v.|_)_)_holds_ |.(Sum_xseq).|_<=_Sum_yseq let xseq be FinSequence of REAL m; ::_thesis: for yseq being FinSequence of REAL st i + 1 = len xseq & len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds ex v being Element of REAL m st ( v = xseq . i & yseq . i = |.v.| ) ) holds |.(Sum xseq).| <= Sum yseq let yseq be FinSequence of REAL ; ::_thesis: ( i + 1 = len xseq & len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds ex v being Element of REAL m st ( v = xseq . i & yseq . i = |.v.| ) ) implies |.(Sum xseq).| <= Sum yseq ) set xseq0 = xseq | i; set yseq0 = yseq | i; assume A4: ( i + 1 = len xseq & len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds ex v being Element of REAL m st ( v = xseq . i & yseq . i = |.v.| ) ) ) ; ::_thesis: |.(Sum xseq).| <= Sum yseq A5: for k being Element of NAT st k in dom (xseq | i) holds ex v being Element of REAL m st ( v = (xseq | i) . k & (yseq | i) . k = |.v.| ) proof let k be Element of NAT ; ::_thesis: ( k in dom (xseq | i) implies ex v being Element of REAL m st ( v = (xseq | i) . k & (yseq | i) . k = |.v.| ) ) assume k in dom (xseq | i) ; ::_thesis: ex v being Element of REAL m st ( v = (xseq | i) . k & (yseq | i) . k = |.v.| ) then A6: ( k in Seg i & k in dom xseq ) by RELAT_1:57; then consider v being Element of REAL m such that A7: ( v = xseq . k & yseq . k = |.v.| ) by A4; take v ; ::_thesis: ( v = (xseq | i) . k & (yseq | i) . k = |.v.| ) thus ( v = (xseq | i) . k & (yseq | i) . k = |.v.| ) by A6, A7, FUNCT_1:49; ::_thesis: verum end; dom xseq = Seg (i + 1) by A4, FINSEQ_1:def_3; then consider w being Element of REAL m such that A8: ( w = xseq . (i + 1) & yseq . (i + 1) = |.w.| ) by A4, FINSEQ_1:4; A9: ( 1 <= i + 1 & i + 1 <= len yseq ) by A4, NAT_1:11; yseq = (yseq | i) ^ <*(yseq /. (i + 1))*> by A4, FINSEQ_5:21; then yseq = (yseq | i) ^ <*(yseq . (i + 1))*> by A9, FINSEQ_4:15; then A10: Sum yseq = (Sum (yseq | i)) + (yseq . (i + 1)) by RVSUM_1:74; A11: i = len (xseq | i) by A4, FINSEQ_1:59, NAT_1:11; then A12: ex v being Element of REAL m st ( v = xseq . (len xseq) & Sum xseq = (Sum (xseq | i)) + v ) by A4, Th15; A13: |.((Sum (xseq | i)) + w).| <= |.(Sum (xseq | i)).| + |.w.| by EUCLID:12; len (xseq | i) = len (yseq | i) by A4, A11, FINSEQ_1:59, NAT_1:11; then |.(Sum (xseq | i)).| <= Sum (yseq | i) by A3, A5, A11; then |.(Sum (xseq | i)).| + |.w.| <= (Sum (yseq | i)) + (yseq . (i + 1)) by A8, XREAL_1:6; hence |.(Sum xseq).| <= Sum yseq by A4, A8, A10, A12, A13, XXREAL_0:2; ::_thesis: verum end; hence S1[i + 1] ; ::_thesis: verum end; for i being Element of NAT holds S1[i] from NAT_1:sch_1(A1, A2); hence for xseq being FinSequence of REAL m for yseq being FinSequence of REAL st len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds ex v being Element of REAL m st ( v = xseq . i & yseq . i = |.v.| ) ) holds |.(Sum xseq).| <= Sum yseq ; ::_thesis: verum end; registration let m, n be Nat; cluster Function-like V30( REAL m, REAL n) additive homogeneous -> Lipschitzian for Element of K6(K7((REAL m),(REAL n))); coherence for b1 being LinearOperator of m,n holds b1 is Lipschitzian proof let f be LinearOperator of m,n; ::_thesis: f is Lipschitzian A1: ( m in NAT & n in NAT ) by ORDINAL1:def_12; defpred S1[ Nat, set ] means n = |.(f . (Base_FinSeq (m,m))).|; A2: for k0 being Nat st k0 in Seg m holds ex v being Element of REAL st S1[k0,v] ; consider KS being FinSequence of REAL such that A3: ( dom KS = Seg m & ( for i being Nat st i in Seg m holds S1[i,KS . i] ) ) from FINSEQ_1:sch_5(A2); set K = (Sum KS) + 1; now__::_thesis:_for_j_being_Nat_st_j_in_dom_KS_holds_ 0_<=_KS_._j let j be Nat; ::_thesis: ( j in dom KS implies 0 <= KS . j ) assume j in dom KS ; ::_thesis: 0 <= KS . j then KS . j = |.(f . (Base_FinSeq (m,j))).| by A3; hence 0 <= KS . j ; ::_thesis: verum end; then A4: 0 <= Sum KS by RVSUM_1:84; reconsider m0 = m as Nat ; now__::_thesis:_for_x_being_Element_of_REAL_m_holds_|.(f_._x).|_<=_((Sum_KS)_+_1)_*_|.x.| let x be Element of REAL m; ::_thesis: |.(f . x).| <= ((Sum KS) + 1) * |.x.| A5: len (ProjFinSeq x) = m by EUCLID_7:def_12; defpred S2[ set , set ] means n = f . ((ProjFinSeq x) . m); A6: now__::_thesis:_for_k_being_Nat_st_k_in_Seg_m_holds_ ex_x_being_Element_of_REAL_n_st_S2[k,x] let k be Nat; ::_thesis: ( k in Seg m implies ex x being Element of REAL n st S2[k,x] ) assume k in Seg m ; ::_thesis: ex x being Element of REAL n st S2[k,x] then k in dom (ProjFinSeq x) by A5, FINSEQ_1:def_3; then reconsider v = (ProjFinSeq x) . k as Element of REAL m by PARTFUN1:4; f . v is Element of REAL n ; hence ex x being Element of REAL n st S2[k,x] ; ::_thesis: verum end; consider fx being FinSequence of REAL n such that A7: ( dom fx = Seg m & ( for i being Nat st i in Seg m holds S2[i,fx . i] ) ) from FINSEQ_1:sch_5(A6); A8: ( x = Sum (ProjFinSeq x) & len fx = m ) by A1, A7, EUCLID_7:31, FINSEQ_1:def_3; now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_(ProjFinSeq_x)_holds_ fx_._i_=_f_._((ProjFinSeq_x)_._i) let i be Element of NAT ; ::_thesis: ( i in dom (ProjFinSeq x) implies fx . i = f . ((ProjFinSeq x) . i) ) assume i in dom (ProjFinSeq x) ; ::_thesis: fx . i = f . ((ProjFinSeq x) . i) then i in Seg m by A5, FINSEQ_1:def_3; hence fx . i = f . ((ProjFinSeq x) . i) by A7; ::_thesis: verum end; then A9: Sum fx = f . x by A1, A5, A8, Th16; reconsider x0 = x as Element of REAL m ; A10: for i being Nat st 1 <= i & i <= m holds ex v being Element of REAL n st ( v = fx . i & |.v.| <= |.x.| * |.(f . (Base_FinSeq (m,i))).| ) proof let i be Nat; ::_thesis: ( 1 <= i & i <= m implies ex v being Element of REAL n st ( v = fx . i & |.v.| <= |.x.| * |.(f . (Base_FinSeq (m,i))).| ) ) assume A11: ( 1 <= i & i <= m ) ; ::_thesis: ex v being Element of REAL n st ( v = fx . i & |.v.| <= |.x.| * |.(f . (Base_FinSeq (m,i))).| ) then A12: (ProjFinSeq x) . i = |(x,(Base_FinSeq (m,i)))| * (Base_FinSeq (m,i)) by EUCLID_7:def_12; A13: i in Seg m by A11, FINSEQ_1:1; then reconsider v = fx . i as Element of REAL n by A7, PARTFUN1:4; take v ; ::_thesis: ( v = fx . i & |.v.| <= |.x.| * |.(f . (Base_FinSeq (m,i))).| ) v = f . ((ProjFinSeq x) . i) by A7, A13; then v = |(x,(Base_FinSeq (m,i)))| * (f . (Base_FinSeq (m,i))) by A12, Def2; then v = (x0 . i) * (f . (Base_FinSeq (m,i))) by A11, EUCLID_7:30; then |.v.| = |.(x0 . i).| * |.(f . (Base_FinSeq (m,i))).| by EUCLID:11; hence ( v = fx . i & |.v.| <= |.x.| * |.(f . (Base_FinSeq (m,i))).| ) by A13, REAL_NS1:8, XREAL_1:64; ::_thesis: verum end; defpred S3[ set , set ] means ex v being Element of REAL n st ( v = fx . m & n = |.v.| ); A14: now__::_thesis:_for_k_being_Nat_st_k_in_Seg_m_holds_ ex_x_being_Element_of_REAL_st_S3[k,x] let k be Nat; ::_thesis: ( k in Seg m implies ex x being Element of REAL st S3[k,x] ) assume k in Seg m ; ::_thesis: ex x being Element of REAL st S3[k,x] then reconsider v = fx . k as Element of REAL n by A7, PARTFUN1:4; |.v.| in REAL ; hence ex x being Element of REAL st S3[k,x] ; ::_thesis: verum end; consider zfx being FinSequence of REAL such that A15: ( dom zfx = Seg m & ( for i being Nat st i in Seg m holds S3[i,zfx . i] ) ) from FINSEQ_1:sch_5(A14); A16: len zfx = m by A1, A15, FINSEQ_1:def_3; then A17: len fx = len zfx by A7, FINSEQ_1:def_3; for i being Element of NAT st i in dom fx holds ex v being Element of REAL n st ( v = fx . i & zfx . i = |.v.| ) by A7, A15; then A18: |.(f . x).| <= Sum zfx by A1, A9, A17, Th17; A19: now__::_thesis:_for_j_being_Nat_st_j_in_Seg_m_holds_ zfx_._j_<=_(|.x.|_*_KS)_._j let j be Nat; ::_thesis: ( j in Seg m implies zfx . j <= (|.x.| * KS) . j ) assume A20: j in Seg m ; ::_thesis: zfx . j <= (|.x.| * KS) . j then A21: ex v being Element of REAL n st ( v = fx . j & zfx . j = |.v.| ) by A15; ( 1 <= j & j <= m ) by A20, FINSEQ_1:1; then ex v being Element of REAL n st ( v = fx . j & |.v.| <= |.x.| * |.(f . (Base_FinSeq (m,j))).| ) by A10; then zfx . j <= |.x.| * (KS . j) by A3, A20, A21; hence zfx . j <= (|.x.| * KS) . j by VALUED_1:6; ::_thesis: verum end; A22: zfx is Element of m -tuples_on REAL by A16, FINSEQ_2:92; len KS = m by A1, A3, FINSEQ_1:def_3; then reconsider KS0 = KS as Element of REAL m0 by FINSEQ_2:92; |.x.| * KS0 is Element of m0 -tuples_on REAL ; then Sum zfx <= Sum (|.x.| * KS) by A19, A22, RVSUM_1:82; then Sum zfx <= |.x.| * (Sum KS) by RVSUM_1:87; then A23: |.(f . x).| <= |.x.| * (Sum KS) by A18, XXREAL_0:2; 0 + (Sum KS) <= 1 + (Sum KS) by XREAL_1:6; then |.x.| * (Sum KS) <= |.x.| * (1 + (Sum KS)) by XREAL_1:64; hence |.(f . x).| <= ((Sum KS) + 1) * |.x.| by A23, XXREAL_0:2; ::_thesis: verum end; hence f is Lipschitzian by A4, Def3; ::_thesis: verum end; end; registration let m, n be Element of NAT ; cluster Function-like V30( the carrier of (REAL-NS m), the carrier of (REAL-NS n)) additive homogeneous -> Lipschitzian for Element of K6(K7( the carrier of (REAL-NS m), the carrier of (REAL-NS n))); coherence for b1 being LinearOperator of (REAL-NS m),(REAL-NS n) holds b1 is Lipschitzian proof let f be LinearOperator of (REAL-NS m),(REAL-NS n); ::_thesis: f is Lipschitzian reconsider g = f as LinearOperator of m,n by Th14; consider K being Real such that A1: ( 0 <= K & ( for x being Element of REAL m holds |.(g . x).| <= K * |.x.| ) ) by Def3; take K ; :: according to LOPBAN_1:def_8 ::_thesis: ( 0 <= K & ( for b1 being Element of the carrier of (REAL-NS m) holds ||.(f . b1).|| <= K * ||.b1.|| ) ) thus 0 <= K by A1; ::_thesis: for b1 being Element of the carrier of (REAL-NS m) holds ||.(f . b1).|| <= K * ||.b1.|| let x be Point of (REAL-NS m); ::_thesis: ||.(f . x).|| <= K * ||.x.|| reconsider x1 = x as Element of REAL m by REAL_NS1:def_4; reconsider y = g . x1 as Element of REAL n ; ||.(f . x).|| = |.y.| by REAL_NS1:1; then ||.(f . x).|| <= K * |.x1.| by A1; hence ||.(f . x).|| <= K * ||.x.|| by REAL_NS1:1; ::_thesis: verum end; end; theorem Th18: :: PDIFF_6:18 for m, n being non empty Element of NAT for f being PartFunc of (REAL m),(REAL n) for x being Element of REAL m st f is_differentiable_in x holds diff (f,x) is LinearOperator of (REAL-NS m),(REAL-NS n) proof let m, n be non empty Element of NAT ; ::_thesis: for f being PartFunc of (REAL m),(REAL n) for x being Element of REAL m st f is_differentiable_in x holds diff (f,x) is LinearOperator of (REAL-NS m),(REAL-NS n) let f be PartFunc of (REAL m),(REAL n); ::_thesis: for x being Element of REAL m st f is_differentiable_in x holds diff (f,x) is LinearOperator of (REAL-NS m),(REAL-NS n) let x be Element of REAL m; ::_thesis: ( f is_differentiable_in x implies diff (f,x) is LinearOperator of (REAL-NS m),(REAL-NS n) ) assume f is_differentiable_in x ; ::_thesis: diff (f,x) is LinearOperator of (REAL-NS m),(REAL-NS n) then diff (f,x) is Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))) by Th10; hence diff (f,x) is LinearOperator of (REAL-NS m),(REAL-NS n) by LOPBAN_1:def_9; ::_thesis: verum end; theorem :: PDIFF_6:19 for m, n being non empty Element of NAT for f being PartFunc of (REAL m),(REAL n) for x being Element of REAL m st f is_differentiable_in x holds diff (f,x) is LinearOperator of m,n proof let m, n be non empty Element of NAT ; ::_thesis: for f being PartFunc of (REAL m),(REAL n) for x being Element of REAL m st f is_differentiable_in x holds diff (f,x) is LinearOperator of m,n let f be PartFunc of (REAL m),(REAL n); ::_thesis: for x being Element of REAL m st f is_differentiable_in x holds diff (f,x) is LinearOperator of m,n let x be Element of REAL m; ::_thesis: ( f is_differentiable_in x implies diff (f,x) is LinearOperator of m,n ) assume f is_differentiable_in x ; ::_thesis: diff (f,x) is LinearOperator of m,n then diff (f,x) is LinearOperator of (REAL-NS m),(REAL-NS n) by Th18; hence diff (f,x) is LinearOperator of m,n by Th14; ::_thesis: verum end; theorem :: PDIFF_6:20 for n, m being non empty Element of NAT for g1, g2 being PartFunc of (REAL m),(REAL n) for y0 being Element of REAL m st g1 is_differentiable_in y0 & g2 is_differentiable_in y0 holds ( g1 + g2 is_differentiable_in y0 & diff ((g1 + g2),y0) = (diff (g1,y0)) + (diff (g2,y0)) ) proof let n, m be non empty Element of NAT ; ::_thesis: for g1, g2 being PartFunc of (REAL m),(REAL n) for y0 being Element of REAL m st g1 is_differentiable_in y0 & g2 is_differentiable_in y0 holds ( g1 + g2 is_differentiable_in y0 & diff ((g1 + g2),y0) = (diff (g1,y0)) + (diff (g2,y0)) ) let g1, g2 be PartFunc of (REAL m),(REAL n); ::_thesis: for y0 being Element of REAL m st g1 is_differentiable_in y0 & g2 is_differentiable_in y0 holds ( g1 + g2 is_differentiable_in y0 & diff ((g1 + g2),y0) = (diff (g1,y0)) + (diff (g2,y0)) ) let y0 be Element of REAL m; ::_thesis: ( g1 is_differentiable_in y0 & g2 is_differentiable_in y0 implies ( g1 + g2 is_differentiable_in y0 & diff ((g1 + g2),y0) = (diff (g1,y0)) + (diff (g2,y0)) ) ) assume A1: ( g1 is_differentiable_in y0 & g2 is_differentiable_in y0 ) ; ::_thesis: ( g1 + g2 is_differentiable_in y0 & diff ((g1 + g2),y0) = (diff (g1,y0)) + (diff (g2,y0)) ) reconsider f1 = g1 as PartFunc of (REAL-NS m),(REAL-NS n) by Th1; reconsider f2 = g2 as PartFunc of (REAL-NS m),(REAL-NS n) by Th1; reconsider x0 = y0 as Point of (REAL-NS m) by REAL_NS1:def_4; ( f1 is_differentiable_in x0 & f2 is_differentiable_in x0 ) by A1, Th2; then A2: ( f1 + f2 is_differentiable_in x0 & diff ((f1 + f2),x0) = (diff (f1,x0)) + (diff (f2,x0)) ) by NDIFF_1:35; f1 + f2 = g1 + g2 by Th4; hence g1 + g2 is_differentiable_in y0 by A2, Th2; ::_thesis: diff ((g1 + g2),y0) = (diff (g1,y0)) + (diff (g2,y0)) then A3: diff ((g1 + g2),y0) = diff ((f1 + f2),x0) by Th4, Th3; ( diff (f1,x0) = diff (g1,y0) & diff (f2,x0) = diff (g2,y0) ) by Th3, A1; hence diff ((g1 + g2),y0) = (diff (g1,y0)) + (diff (g2,y0)) by A2, A3, Th7; ::_thesis: verum end; theorem :: PDIFF_6:21 for n, m being non empty Element of NAT for g1, g2 being PartFunc of (REAL m),(REAL n) for y0 being Element of REAL m st g1 is_differentiable_in y0 & g2 is_differentiable_in y0 holds ( g1 - g2 is_differentiable_in y0 & diff ((g1 - g2),y0) = (diff (g1,y0)) - (diff (g2,y0)) ) proof let n, m be non empty Element of NAT ; ::_thesis: for g1, g2 being PartFunc of (REAL m),(REAL n) for y0 being Element of REAL m st g1 is_differentiable_in y0 & g2 is_differentiable_in y0 holds ( g1 - g2 is_differentiable_in y0 & diff ((g1 - g2),y0) = (diff (g1,y0)) - (diff (g2,y0)) ) let g1, g2 be PartFunc of (REAL m),(REAL n); ::_thesis: for y0 being Element of REAL m st g1 is_differentiable_in y0 & g2 is_differentiable_in y0 holds ( g1 - g2 is_differentiable_in y0 & diff ((g1 - g2),y0) = (diff (g1,y0)) - (diff (g2,y0)) ) let y0 be Element of REAL m; ::_thesis: ( g1 is_differentiable_in y0 & g2 is_differentiable_in y0 implies ( g1 - g2 is_differentiable_in y0 & diff ((g1 - g2),y0) = (diff (g1,y0)) - (diff (g2,y0)) ) ) assume A1: ( g1 is_differentiable_in y0 & g2 is_differentiable_in y0 ) ; ::_thesis: ( g1 - g2 is_differentiable_in y0 & diff ((g1 - g2),y0) = (diff (g1,y0)) - (diff (g2,y0)) ) reconsider f1 = g1 as PartFunc of (REAL-NS m),(REAL-NS n) by Th1; reconsider f2 = g2 as PartFunc of (REAL-NS m),(REAL-NS n) by Th1; reconsider x0 = y0 as Point of (REAL-NS m) by REAL_NS1:def_4; ( f1 is_differentiable_in x0 & f2 is_differentiable_in x0 ) by A1, Th2; then A2: ( f1 - f2 is_differentiable_in x0 & diff ((f1 - f2),x0) = (diff (f1,x0)) - (diff (f2,x0)) ) by NDIFF_1:36; f1 - f2 = g1 - g2 by Th5; hence g1 - g2 is_differentiable_in y0 by A2, Th2; ::_thesis: diff ((g1 - g2),y0) = (diff (g1,y0)) - (diff (g2,y0)) then A3: diff ((g1 - g2),y0) = diff ((f1 - f2),x0) by Th3, Th5; ( diff (f1,x0) = diff (g1,y0) & diff (f2,x0) = diff (g2,y0) ) by Th3, A1; hence diff ((g1 - g2),y0) = (diff (g1,y0)) - (diff (g2,y0)) by A2, A3, Th8; ::_thesis: verum end; theorem :: PDIFF_6:22 for n, m being non empty Element of NAT for g being PartFunc of (REAL m),(REAL n) for y0 being Element of REAL m for r being Real st g is_differentiable_in y0 holds ( r (#) g is_differentiable_in y0 & diff ((r (#) g),y0) = r (#) (diff (g,y0)) ) proof let n, m be non empty Element of NAT ; ::_thesis: for g being PartFunc of (REAL m),(REAL n) for y0 being Element of REAL m for r being Real st g is_differentiable_in y0 holds ( r (#) g is_differentiable_in y0 & diff ((r (#) g),y0) = r (#) (diff (g,y0)) ) let g be PartFunc of (REAL m),(REAL n); ::_thesis: for y0 being Element of REAL m for r being Real st g is_differentiable_in y0 holds ( r (#) g is_differentiable_in y0 & diff ((r (#) g),y0) = r (#) (diff (g,y0)) ) let y0 be Element of REAL m; ::_thesis: for r being Real st g is_differentiable_in y0 holds ( r (#) g is_differentiable_in y0 & diff ((r (#) g),y0) = r (#) (diff (g,y0)) ) let r be Real; ::_thesis: ( g is_differentiable_in y0 implies ( r (#) g is_differentiable_in y0 & diff ((r (#) g),y0) = r (#) (diff (g,y0)) ) ) assume A1: g is_differentiable_in y0 ; ::_thesis: ( r (#) g is_differentiable_in y0 & diff ((r (#) g),y0) = r (#) (diff (g,y0)) ) reconsider f = g as PartFunc of (REAL-NS m),(REAL-NS n) by Th1; reconsider x0 = y0 as Point of (REAL-NS m) by REAL_NS1:def_4; f is_differentiable_in x0 by A1, Th2; then A2: ( r (#) f is_differentiable_in x0 & diff ((r (#) f),x0) = r * (diff (f,x0)) ) by NDIFF_1:37; r (#) f = r (#) g by Th6; hence r (#) g is_differentiable_in y0 by A2, Th2; ::_thesis: diff ((r (#) g),y0) = r (#) (diff (g,y0)) then diff ((r (#) g),y0) = diff ((r (#) f),x0) by Th3, Th6; hence diff ((r (#) g),y0) = r (#) (diff (g,y0)) by A2, Th9, Th3, A1; ::_thesis: verum end; theorem Th23: :: PDIFF_6:23 for m being Element of NAT for x0 being Element of REAL m for y0 being Point of (REAL-NS m) for r being Real st x0 = y0 holds { y where y is Element of REAL m : |.(y - x0).| < r } = { z where z is Point of (REAL-NS m) : ||.(z - y0).|| < r } proof let m be Element of NAT ; ::_thesis: for x0 being Element of REAL m for y0 being Point of (REAL-NS m) for r being Real st x0 = y0 holds { y where y is Element of REAL m : |.(y - x0).| < r } = { z where z is Point of (REAL-NS m) : ||.(z - y0).|| < r } let x0 be Element of REAL m; ::_thesis: for y0 being Point of (REAL-NS m) for r being Real st x0 = y0 holds { y where y is Element of REAL m : |.(y - x0).| < r } = { z where z is Point of (REAL-NS m) : ||.(z - y0).|| < r } let y0 be Point of (REAL-NS m); ::_thesis: for r being Real st x0 = y0 holds { y where y is Element of REAL m : |.(y - x0).| < r } = { z where z is Point of (REAL-NS m) : ||.(z - y0).|| < r } let r be Real; ::_thesis: ( x0 = y0 implies { y where y is Element of REAL m : |.(y - x0).| < r } = { z where z is Point of (REAL-NS m) : ||.(z - y0).|| < r } ) assume A1: x0 = y0 ; ::_thesis: { y where y is Element of REAL m : |.(y - x0).| < r } = { z where z is Point of (REAL-NS m) : ||.(z - y0).|| < r } now__::_thesis:_for_w_being_set_st_w_in__{__y_where_y_is_Element_of_REAL_m_:_|.(y_-_x0).|_<_r__}__holds_ w_in__{__z1_where_z1_is_Point_of_(REAL-NS_m)_:_||.(z1_-_y0).||_<_r__}_ let w be set ; ::_thesis: ( w in { y where y is Element of REAL m : |.(y - x0).| < r } implies w in { z1 where z1 is Point of (REAL-NS m) : ||.(z1 - y0).|| < r } ) assume w in { y where y is Element of REAL m : |.(y - x0).| < r } ; ::_thesis: w in { z1 where z1 is Point of (REAL-NS m) : ||.(z1 - y0).|| < r } then consider y being Element of REAL m such that A2: ( y = w & |.(y - x0).| < r ) ; reconsider z = y as Point of (REAL-NS m) by REAL_NS1:def_4; ||.(z - y0).|| < r by A1, A2, REAL_NS1:1, REAL_NS1:5; hence w in { z1 where z1 is Point of (REAL-NS m) : ||.(z1 - y0).|| < r } by A2; ::_thesis: verum end; then A3: { y where y is Element of REAL m : |.(y - x0).| < r } c= { z where z is Point of (REAL-NS m) : ||.(z - y0).|| < r } by TARSKI:def_3; now__::_thesis:_for_w_being_set_st_w_in__{__z_where_z_is_Point_of_(REAL-NS_m)_:_||.(z_-_y0).||_<_r__}__holds_ w_in__{__z1_where_z1_is_Element_of_REAL_m_:_|.(z1_-_x0).|_<_r__}_ let w be set ; ::_thesis: ( w in { z where z is Point of (REAL-NS m) : ||.(z - y0).|| < r } implies w in { z1 where z1 is Element of REAL m : |.(z1 - x0).| < r } ) assume w in { z where z is Point of (REAL-NS m) : ||.(z - y0).|| < r } ; ::_thesis: w in { z1 where z1 is Element of REAL m : |.(z1 - x0).| < r } then consider y being Point of (REAL-NS m) such that A4: ( y = w & ||.(y - y0).|| < r ) ; reconsider z = y as Element of REAL m by REAL_NS1:def_4; |.(z - x0).| < r by A1, A4, REAL_NS1:1, REAL_NS1:5; hence w in { z1 where z1 is Element of REAL m : |.(z1 - x0).| < r } by A4; ::_thesis: verum end; then { z where z is Point of (REAL-NS m) : ||.(z - y0).|| < r } c= { y where y is Element of REAL m : |.(y - x0).| < r } by TARSKI:def_3; hence { y where y is Element of REAL m : |.(y - x0).| < r } = { z where z is Point of (REAL-NS m) : ||.(z - y0).|| < r } by A3, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th24: :: PDIFF_6:24 for m, n being non empty Element of NAT for f being PartFunc of (REAL m),(REAL n) for x0 being Element of REAL m for L, R being Function of (REAL m),(REAL n) st L is LinearOperator of m,n & ex r0 being Real st ( 0 < r0 & { y where y is Element of REAL m : |.(y - x0).| < r0 } c= dom f & ( for r being Real st r > 0 holds ex d being Real st ( d > 0 & ( for z being Element of REAL m for w being Element of REAL n st z <> 0* m & |.z.| < d & w = R . z holds (|.z.| ") * |.w.| < r ) ) ) & ( for x being Element of REAL m st |.(x - x0).| < r0 holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R . (x - x0)) ) ) holds ( f is_differentiable_in x0 & diff (f,x0) = L ) proof let m, n be non empty Element of NAT ; ::_thesis: for f being PartFunc of (REAL m),(REAL n) for x0 being Element of REAL m for L, R being Function of (REAL m),(REAL n) st L is LinearOperator of m,n & ex r0 being Real st ( 0 < r0 & { y where y is Element of REAL m : |.(y - x0).| < r0 } c= dom f & ( for r being Real st r > 0 holds ex d being Real st ( d > 0 & ( for z being Element of REAL m for w being Element of REAL n st z <> 0* m & |.z.| < d & w = R . z holds (|.z.| ") * |.w.| < r ) ) ) & ( for x being Element of REAL m st |.(x - x0).| < r0 holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R . (x - x0)) ) ) holds ( f is_differentiable_in x0 & diff (f,x0) = L ) let f be PartFunc of (REAL m),(REAL n); ::_thesis: for x0 being Element of REAL m for L, R being Function of (REAL m),(REAL n) st L is LinearOperator of m,n & ex r0 being Real st ( 0 < r0 & { y where y is Element of REAL m : |.(y - x0).| < r0 } c= dom f & ( for r being Real st r > 0 holds ex d being Real st ( d > 0 & ( for z being Element of REAL m for w being Element of REAL n st z <> 0* m & |.z.| < d & w = R . z holds (|.z.| ") * |.w.| < r ) ) ) & ( for x being Element of REAL m st |.(x - x0).| < r0 holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R . (x - x0)) ) ) holds ( f is_differentiable_in x0 & diff (f,x0) = L ) let x0 be Element of REAL m; ::_thesis: for L, R being Function of (REAL m),(REAL n) st L is LinearOperator of m,n & ex r0 being Real st ( 0 < r0 & { y where y is Element of REAL m : |.(y - x0).| < r0 } c= dom f & ( for r being Real st r > 0 holds ex d being Real st ( d > 0 & ( for z being Element of REAL m for w being Element of REAL n st z <> 0* m & |.z.| < d & w = R . z holds (|.z.| ") * |.w.| < r ) ) ) & ( for x being Element of REAL m st |.(x - x0).| < r0 holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R . (x - x0)) ) ) holds ( f is_differentiable_in x0 & diff (f,x0) = L ) let L, R be Function of (REAL m),(REAL n); ::_thesis: ( L is LinearOperator of m,n & ex r0 being Real st ( 0 < r0 & { y where y is Element of REAL m : |.(y - x0).| < r0 } c= dom f & ( for r being Real st r > 0 holds ex d being Real st ( d > 0 & ( for z being Element of REAL m for w being Element of REAL n st z <> 0* m & |.z.| < d & w = R . z holds (|.z.| ") * |.w.| < r ) ) ) & ( for x being Element of REAL m st |.(x - x0).| < r0 holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R . (x - x0)) ) ) implies ( f is_differentiable_in x0 & diff (f,x0) = L ) ) reconsider g = f as PartFunc of (REAL-NS m),(REAL-NS n) by Th1; reconsider y0 = x0 as Point of (REAL-NS m) by REAL_NS1:def_4; assume A1: ( L is LinearOperator of m,n & ex r0 being Real st ( 0 < r0 & { y where y is Element of REAL m : |.(y - x0).| < r0 } c= dom f & ( for r being Real st r > 0 holds ex d being Real st ( d > 0 & ( for z being Element of REAL m for w being Element of REAL n st z <> 0* m & |.z.| < d & w = R . z holds (|.z.| ") * |.w.| < r ) ) ) & ( for x being Element of REAL m st |.(x - x0).| < r0 holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ; ::_thesis: ( f is_differentiable_in x0 & diff (f,x0) = L ) then consider r0 being Real such that A2: ( 0 < r0 & { y where y is Element of REAL m : |.(y - x0).| < r0 } c= dom f & ( for r being Real st r > 0 holds ex d being Real st ( d > 0 & ( for z being Element of REAL m for w being Element of REAL n st z <> 0* m & |.z.| < d & w = R . z holds (|.z.| ") * |.w.| < r ) ) ) & ( for x being Element of REAL m st |.(x - x0).| < r0 holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ; L is LinearOperator of (REAL-NS m),(REAL-NS n) by A1, Th14; then reconsider GL = L as Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))) by LOPBAN_1:def_9; ( REAL m = the carrier of (REAL-NS m) & REAL n = the carrier of (REAL-NS n) ) by REAL_NS1:def_4; then reconsider GR = R as Function of (REAL-NS m),(REAL-NS n) ; the carrier of (REAL-NS m) = REAL m by REAL_NS1:def_4; then A3: dom R = the carrier of (REAL-NS m) by FUNCT_2:def_1; now__::_thesis:_for_r_being_Real_st_r_>_0_holds_ ex_d_being_Real_st_ (_d_>_0_&_(_for_z_being_Point_of_(REAL-NS_m)_st_z_<>_0._(REAL-NS_m)_&_||.z.||_<_d_holds_ (||.z.||_")_*_||.(GR_/._z).||_<_r_)_) let r be Real; ::_thesis: ( r > 0 implies ex d being Real st ( d > 0 & ( for z being Point of (REAL-NS m) st z <> 0. (REAL-NS m) & ||.z.|| < d holds (||.z.|| ") * ||.(GR /. z).|| < r ) ) ) assume r > 0 ; ::_thesis: ex d being Real st ( d > 0 & ( for z being Point of (REAL-NS m) st z <> 0. (REAL-NS m) & ||.z.|| < d holds (||.z.|| ") * ||.(GR /. z).|| < r ) ) then consider d being Real such that A4: ( d > 0 & ( for z being Element of REAL m for w being Element of REAL n st z <> 0* m & |.z.| < d & w = R . z holds (|.z.| ") * |.w.| < r ) ) by A2; take d = d; ::_thesis: ( d > 0 & ( for z being Point of (REAL-NS m) st z <> 0. (REAL-NS m) & ||.z.|| < d holds (||.z.|| ") * ||.(GR /. z).|| < r ) ) thus d > 0 by A4; ::_thesis: for z being Point of (REAL-NS m) st z <> 0. (REAL-NS m) & ||.z.|| < d holds (||.z.|| ") * ||.(GR /. z).|| < r thus for z being Point of (REAL-NS m) st z <> 0. (REAL-NS m) & ||.z.|| < d holds (||.z.|| ") * ||.(GR /. z).|| < r ::_thesis: verum proof let z be Point of (REAL-NS m); ::_thesis: ( z <> 0. (REAL-NS m) & ||.z.|| < d implies (||.z.|| ") * ||.(GR /. z).|| < r ) assume A5: ( z <> 0. (REAL-NS m) & ||.z.|| < d ) ; ::_thesis: (||.z.|| ") * ||.(GR /. z).|| < r reconsider s = z as Element of REAL m by REAL_NS1:def_4; reconsider w = R . s as Element of REAL n ; A6: s <> 0* m by A5, REAL_NS1:def_4; |.s.| < d by A5, REAL_NS1:1; then (|.s.| ") * |.w.| < r by A4, A6; then (||.z.|| ") * |.w.| < r by REAL_NS1:1; hence (||.z.|| ") * ||.(GR /. z).|| < r by REAL_NS1:1; ::_thesis: verum end; end; then reconsider GR = GR as RestFunc of (REAL-NS m),(REAL-NS n) by NDIFF_1:23; set N = { y where y is Point of (REAL-NS m) : ||.(y - y0).|| < r0 } ; reconsider N = { y where y is Point of (REAL-NS m) : ||.(y - y0).|| < r0 } as Neighbourhood of y0 by A2, NFCONT_1:3; A7: N c= dom g by A2, Th23; A8: for y being Point of (REAL-NS m) st y in N holds (g /. y) - (g /. y0) = (GL . (y - y0)) + (GR /. (y - y0)) proof let y be Point of (REAL-NS m); ::_thesis: ( y in N implies (g /. y) - (g /. y0) = (GL . (y - y0)) + (GR /. (y - y0)) ) assume A9: y in N ; ::_thesis: (g /. y) - (g /. y0) = (GL . (y - y0)) + (GR /. (y - y0)) reconsider x = y as Element of REAL m by REAL_NS1:def_4; x in { s where s is Element of REAL m : |.(s - x0).| < r0 } by A9, Th23; then ex s being Element of REAL m st ( s = x & |.(s - x0).| < r0 ) ; then A10: (f /. x) - (f /. x0) = (L . (x - x0)) + (R . (x - x0)) by A2; A11: y0 in N by NFCONT_1:4; then ( f /. x = f . x & f /. x0 = f . x0 ) by A9, A7, PARTFUN1:def_6; then A12: ( f /. x = g /. y & f /. x0 = g /. y0 ) by A9, A11, A7, PARTFUN1:def_6; x - x0 = y - y0 by REAL_NS1:5; then ( L . (x - x0) = GL . (y - y0) & R . (x - x0) = GR /. (y - y0) ) by A3, PARTFUN1:def_6; then (L . (x - x0)) + (R . (x - x0)) = (GL . (y - y0)) + (GR /. (y - y0)) by REAL_NS1:2; hence (g /. y) - (g /. y0) = (GL . (y - y0)) + (GR /. (y - y0)) by A10, A12, REAL_NS1:5; ::_thesis: verum end; then A13: g is_differentiable_in y0 by A7, NDIFF_1:def_6; hence A14: f is_differentiable_in x0 by Th2; ::_thesis: diff (f,x0) = L diff (g,y0) = GL by A13, A8, A7, NDIFF_1:def_7; hence diff (f,x0) = L by Th3, A14; ::_thesis: verum end; theorem :: PDIFF_6:25 for m, n being non empty Element of NAT for f being PartFunc of (REAL m),(REAL n) for x0 being Element of REAL m holds ( f is_differentiable_in x0 iff ex r0 being Real st ( 0 < r0 & { y where y is Element of REAL m : |.(y - x0).| < r0 } c= dom f & ex L, R being Function of (REAL m),(REAL n) st ( L is LinearOperator of m,n & ( for r being Real st r > 0 holds ex d being Real st ( d > 0 & ( for z being Element of REAL m for w being Element of REAL n st z <> 0* m & |.z.| < d & w = R . z holds (|.z.| ") * |.w.| < r ) ) ) & ( for x being Element of REAL m st |.(x - x0).| < r0 holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) proof let m, n be non empty Element of NAT ; ::_thesis: for f being PartFunc of (REAL m),(REAL n) for x0 being Element of REAL m holds ( f is_differentiable_in x0 iff ex r0 being Real st ( 0 < r0 & { y where y is Element of REAL m : |.(y - x0).| < r0 } c= dom f & ex L, R being Function of (REAL m),(REAL n) st ( L is LinearOperator of m,n & ( for r being Real st r > 0 holds ex d being Real st ( d > 0 & ( for z being Element of REAL m for w being Element of REAL n st z <> 0* m & |.z.| < d & w = R . z holds (|.z.| ") * |.w.| < r ) ) ) & ( for x being Element of REAL m st |.(x - x0).| < r0 holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) let f be PartFunc of (REAL m),(REAL n); ::_thesis: for x0 being Element of REAL m holds ( f is_differentiable_in x0 iff ex r0 being Real st ( 0 < r0 & { y where y is Element of REAL m : |.(y - x0).| < r0 } c= dom f & ex L, R being Function of (REAL m),(REAL n) st ( L is LinearOperator of m,n & ( for r being Real st r > 0 holds ex d being Real st ( d > 0 & ( for z being Element of REAL m for w being Element of REAL n st z <> 0* m & |.z.| < d & w = R . z holds (|.z.| ") * |.w.| < r ) ) ) & ( for x being Element of REAL m st |.(x - x0).| < r0 holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) let x0 be Element of REAL m; ::_thesis: ( f is_differentiable_in x0 iff ex r0 being Real st ( 0 < r0 & { y where y is Element of REAL m : |.(y - x0).| < r0 } c= dom f & ex L, R being Function of (REAL m),(REAL n) st ( L is LinearOperator of m,n & ( for r being Real st r > 0 holds ex d being Real st ( d > 0 & ( for z being Element of REAL m for w being Element of REAL n st z <> 0* m & |.z.| < d & w = R . z holds (|.z.| ") * |.w.| < r ) ) ) & ( for x being Element of REAL m st |.(x - x0).| < r0 holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) reconsider g = f as PartFunc of (REAL-NS m),(REAL-NS n) by Th1; reconsider y0 = x0 as Point of (REAL-NS m) by REAL_NS1:def_4; hereby ::_thesis: ( ex r0 being Real st ( 0 < r0 & { y where y is Element of REAL m : |.(y - x0).| < r0 } c= dom f & ex L, R being Function of (REAL m),(REAL n) st ( L is LinearOperator of m,n & ( for r being Real st r > 0 holds ex d being Real st ( d > 0 & ( for z being Element of REAL m for w being Element of REAL n st z <> 0* m & |.z.| < d & w = R . z holds (|.z.| ") * |.w.| < r ) ) ) & ( for x being Element of REAL m st |.(x - x0).| < r0 holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) implies f is_differentiable_in x0 ) assume f is_differentiable_in x0 ; ::_thesis: ex r0 being Real st ( 0 < r0 & { y where y is Element of REAL m : |.(y - x0).| < r0 } c= dom f & ex L, R being Function of (REAL m),(REAL n) st ( L is LinearOperator of m,n & ( for r being Real st r > 0 holds ex d being Real st ( d > 0 & ( for z being Element of REAL m for w being Element of REAL n st z <> 0* m & |.z.| < d & w = R . z holds (|.z.| ") * |.w.| < r ) ) ) & ( for x being Element of REAL m st |.(x - x0).| < r0 holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) then g is_differentiable_in y0 by Th2; then consider N being Neighbourhood of y0 such that A1: ( N c= dom g & ex GL being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))) ex GR being RestFunc of (REAL-NS m),(REAL-NS n) st for y being Point of (REAL-NS m) st y in N holds (g /. y) - (g /. y0) = (GL . (y - y0)) + (GR /. (y - y0)) ) by NDIFF_1:def_6; consider GL being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))), GR being RestFunc of (REAL-NS m),(REAL-NS n) such that A2: for y being Point of (REAL-NS m) st y in N holds (g /. y) - (g /. y0) = (GL . (y - y0)) + (GR /. (y - y0)) by A1; consider r0 being Real such that A3: ( 0 < r0 & { y where y is Point of (REAL-NS m) : ||.(y - y0).|| < r0 } c= N ) by NFCONT_1:def_1; take r0 = r0; ::_thesis: ( 0 < r0 & { y where y is Element of REAL m : |.(y - x0).| < r0 } c= dom f & ex L, R being Function of (REAL m),(REAL n) st ( L is LinearOperator of m,n & ( for r being Real st r > 0 holds ex d being Real st ( d > 0 & ( for z being Element of REAL m for w being Element of REAL n st z <> 0* m & |.z.| < d & w = R . z holds (|.z.| ") * |.w.| < r ) ) ) & ( for x being Element of REAL m st |.(x - x0).| < r0 holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) thus 0 < r0 by A3; ::_thesis: ( { y where y is Element of REAL m : |.(y - x0).| < r0 } c= dom f & ex L, R being Function of (REAL m),(REAL n) st ( L is LinearOperator of m,n & ( for r being Real st r > 0 holds ex d being Real st ( d > 0 & ( for z being Element of REAL m for w being Element of REAL n st z <> 0* m & |.z.| < d & w = R . z holds (|.z.| ") * |.w.| < r ) ) ) & ( for x being Element of REAL m st |.(x - x0).| < r0 holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) { y where y is Point of (REAL-NS m) : ||.(y - y0).|| < r0 } c= dom g by A3, A1, XBOOLE_1:1; hence { y where y is Element of REAL m : |.(y - x0).| < r0 } c= dom f by Th23; ::_thesis: ex L, R being Function of (REAL m),(REAL n) st ( L is LinearOperator of m,n & ( for r being Real st r > 0 holds ex d being Real st ( d > 0 & ( for z being Element of REAL m for w being Element of REAL n st z <> 0* m & |.z.| < d & w = R . z holds (|.z.| ") * |.w.| < r ) ) ) & ( for x being Element of REAL m st |.(x - x0).| < r0 holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R . (x - x0)) ) ) A4: GR is total by NDIFF_1:def_5; then A5: dom GR = the carrier of (REAL-NS m) by PARTFUN1:def_2; A6: ( the carrier of (REAL-NS m) = REAL m & the carrier of (REAL-NS n) = REAL n ) by REAL_NS1:def_4; then reconsider L = GL as Function of (REAL m),(REAL n) by LOPBAN_1:def_9; reconsider R = GR as Function of (REAL m),(REAL n) by A6, A4; take L = L; ::_thesis: ex R being Function of (REAL m),(REAL n) st ( L is LinearOperator of m,n & ( for r being Real st r > 0 holds ex d being Real st ( d > 0 & ( for z being Element of REAL m for w being Element of REAL n st z <> 0* m & |.z.| < d & w = R . z holds (|.z.| ") * |.w.| < r ) ) ) & ( for x being Element of REAL m st |.(x - x0).| < r0 holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R . (x - x0)) ) ) take R = R; ::_thesis: ( L is LinearOperator of m,n & ( for r being Real st r > 0 holds ex d being Real st ( d > 0 & ( for z being Element of REAL m for w being Element of REAL n st z <> 0* m & |.z.| < d & w = R . z holds (|.z.| ") * |.w.| < r ) ) ) & ( for x being Element of REAL m st |.(x - x0).| < r0 holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R . (x - x0)) ) ) GL is LinearOperator of (REAL-NS m),(REAL-NS n) by LOPBAN_1:def_9; hence L is LinearOperator of m,n by Th14; ::_thesis: ( ( for r being Real st r > 0 holds ex d being Real st ( d > 0 & ( for z being Element of REAL m for w being Element of REAL n st z <> 0* m & |.z.| < d & w = R . z holds (|.z.| ") * |.w.| < r ) ) ) & ( for x being Element of REAL m st |.(x - x0).| < r0 holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R . (x - x0)) ) ) thus for r being Real st r > 0 holds ex d being Real st ( d > 0 & ( for z being Element of REAL m for w being Element of REAL n st z <> 0* m & |.z.| < d & w = R . z holds (|.z.| ") * |.w.| < r ) ) ::_thesis: for x being Element of REAL m st |.(x - x0).| < r0 holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R . (x - x0)) proof let r be Real; ::_thesis: ( r > 0 implies ex d being Real st ( d > 0 & ( for z being Element of REAL m for w being Element of REAL n st z <> 0* m & |.z.| < d & w = R . z holds (|.z.| ") * |.w.| < r ) ) ) assume r > 0 ; ::_thesis: ex d being Real st ( d > 0 & ( for z being Element of REAL m for w being Element of REAL n st z <> 0* m & |.z.| < d & w = R . z holds (|.z.| ") * |.w.| < r ) ) then consider d being Real such that A7: ( d > 0 & ( for z being Point of (REAL-NS m) st z <> 0. (REAL-NS m) & ||.z.|| < d holds (||.z.|| ") * ||.(GR /. z).|| < r ) ) by A4, NDIFF_1:23; take d ; ::_thesis: ( d > 0 & ( for z being Element of REAL m for w being Element of REAL n st z <> 0* m & |.z.| < d & w = R . z holds (|.z.| ") * |.w.| < r ) ) thus d > 0 by A7; ::_thesis: for z being Element of REAL m for w being Element of REAL n st z <> 0* m & |.z.| < d & w = R . z holds (|.z.| ") * |.w.| < r let z be Element of REAL m; ::_thesis: for w being Element of REAL n st z <> 0* m & |.z.| < d & w = R . z holds (|.z.| ") * |.w.| < r let w be Element of REAL n; ::_thesis: ( z <> 0* m & |.z.| < d & w = R . z implies (|.z.| ") * |.w.| < r ) assume A8: ( z <> 0* m & |.z.| < d & w = R . z ) ; ::_thesis: (|.z.| ") * |.w.| < r reconsider s = z as Element of (REAL-NS m) by REAL_NS1:def_4; A9: s <> 0. (REAL-NS m) by A8, REAL_NS1:def_4; ||.s.|| < d by A8, REAL_NS1:1; then (||.s.|| ") * ||.(GR /. s).|| < r by A7, A9; then (|.z.| ") * ||.(GR /. s).|| < r by REAL_NS1:1; hence (|.z.| ") * |.w.| < r by A5, A8, PARTFUN1:def_6, REAL_NS1:1; ::_thesis: verum end; thus for x being Element of REAL m st |.(x - x0).| < r0 holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R . (x - x0)) ::_thesis: verum proof let x be Element of REAL m; ::_thesis: ( |.(x - x0).| < r0 implies (f /. x) - (f /. x0) = (L . (x - x0)) + (R . (x - x0)) ) assume |.(x - x0).| < r0 ; ::_thesis: (f /. x) - (f /. x0) = (L . (x - x0)) + (R . (x - x0)) then x in { s where s is Element of REAL m : |.(s - x0).| < r0 } ; then A10: x in { y where y is Point of (REAL-NS m) : ||.(y - y0).|| < r0 } by Th23; reconsider y = x as Point of (REAL-NS m) by REAL_NS1:def_4; A11: (g /. y) - (g /. y0) = (GL . (y - y0)) + (GR /. (y - y0)) by A3, A10, A2; A12: ( y in N & y0 in N ) by A3, A10, NFCONT_1:4; then ( f /. x = f . x & f /. x0 = f . x0 ) by A1, PARTFUN1:def_6; then A13: ( f /. x = g /. y & f /. x0 = g /. y0 ) by A12, A1, PARTFUN1:def_6; x - x0 = y - y0 by REAL_NS1:5; then ( L . (x - x0) = GL . (y - y0) & R . (x - x0) = GR /. (y - y0) ) by A5, PARTFUN1:def_6; then (L . (x - x0)) + (R . (x - x0)) = (GL . (y - y0)) + (GR /. (y - y0)) by REAL_NS1:2; hence (f /. x) - (f /. x0) = (L . (x - x0)) + (R . (x - x0)) by A11, A13, REAL_NS1:5; ::_thesis: verum end; end; assume ex r0 being Real st ( 0 < r0 & { y where y is Element of REAL m : |.(y - x0).| < r0 } c= dom f & ex L, R being Function of (REAL m),(REAL n) st ( L is LinearOperator of m,n & ( for r being Real st r > 0 holds ex d being Real st ( d > 0 & ( for z being Element of REAL m for w being Element of REAL n st z <> 0* m & |.z.| < d & w = R . z holds (|.z.| ") * |.w.| < r ) ) ) & ( for x being Element of REAL m st |.(x - x0).| < r0 holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ; ::_thesis: f is_differentiable_in x0 hence f is_differentiable_in x0 by Th24; ::_thesis: verum end; begin theorem Th26: :: PDIFF_6:26 for n, i being Element of NAT for y1, y2 being Point of (REAL-NS n) holds (Proj (i,n)) . (y1 + y2) = ((Proj (i,n)) . y1) + ((Proj (i,n)) . y2) proof let n, i be Element of NAT ; ::_thesis: for y1, y2 being Point of (REAL-NS n) holds (Proj (i,n)) . (y1 + y2) = ((Proj (i,n)) . y1) + ((Proj (i,n)) . y2) let y1, y2 be Point of (REAL-NS n); ::_thesis: (Proj (i,n)) . (y1 + y2) = ((Proj (i,n)) . y1) + ((Proj (i,n)) . y2) reconsider yy1 = y1, yy2 = y2 as Element of REAL n by REAL_NS1:def_4; reconsider ry1 = yy1 . i as Element of REAL ; reconsider ry2 = yy2 . i as Element of REAL ; ( (Proj (i,n)) . y1 = <*((proj (i,n)) . y1)*> & (Proj (i,n)) . y2 = <*((proj (i,n)) . y2)*> ) by PDIFF_1:def_4; then A1: ( (Proj (i,n)) . y1 = <*ry1*> & (Proj (i,n)) . y2 = <*ry2*> ) by PDIFF_1:def_1; A2: ( <*ry1*> is Element of REAL 1 & <*ry2*> is Element of REAL 1 ) by FINSEQ_2:98; (Proj (i,n)) . (y1 + y2) = <*((proj (i,n)) . (y1 + y2))*> by PDIFF_1:def_4 .= <*((proj (i,n)) . (yy1 + yy2))*> by REAL_NS1:2 .= <*((yy1 + yy2) . i)*> by PDIFF_1:def_1 .= <*((yy1 . i) + (yy2 . i))*> by RVSUM_1:11 .= <*ry1*> + <*ry2*> by RVSUM_1:13 ; hence (Proj (i,n)) . (y1 + y2) = ((Proj (i,n)) . y1) + ((Proj (i,n)) . y2) by A1, A2, REAL_NS1:2; ::_thesis: verum end; theorem Th27: :: PDIFF_6:27 for n, i being Element of NAT for y1 being Point of (REAL-NS n) for r being Real holds (Proj (i,n)) . (r * y1) = r * ((Proj (i,n)) . y1) proof let n, i be Element of NAT ; ::_thesis: for y1 being Point of (REAL-NS n) for r being Real holds (Proj (i,n)) . (r * y1) = r * ((Proj (i,n)) . y1) let y1 be Point of (REAL-NS n); ::_thesis: for r being Real holds (Proj (i,n)) . (r * y1) = r * ((Proj (i,n)) . y1) let r be Real; ::_thesis: (Proj (i,n)) . (r * y1) = r * ((Proj (i,n)) . y1) reconsider yy1 = y1 as Element of REAL n by REAL_NS1:def_4; reconsider y1i = yy1 . i as Element of REAL ; (Proj (i,n)) . y1 = <*((proj (i,n)) . y1)*> by PDIFF_1:def_4; then A1: (Proj (i,n)) . y1 = <*y1i*> by PDIFF_1:def_1; A2: <*y1i*> is Element of REAL 1 by FINSEQ_2:98; (Proj (i,n)) . (r * y1) = <*((proj (i,n)) . (r * y1))*> by PDIFF_1:def_4 .= <*((proj (i,n)) . (r * yy1))*> by REAL_NS1:3 .= <*((r * yy1) . i)*> by PDIFF_1:def_1 .= <*(r * (yy1 . i))*> by RVSUM_1:44 .= r * <*y1i*> by RVSUM_1:47 ; hence (Proj (i,n)) . (r * y1) = r * ((Proj (i,n)) . y1) by A1, A2, REAL_NS1:3; ::_thesis: verum end; theorem Th28: :: PDIFF_6:28 for m, n being non empty Element of NAT for g being PartFunc of (REAL-NS m),(REAL-NS n) for x0 being Point of (REAL-NS m) for i being Element of NAT st 1 <= i & i <= n & g is_differentiable_in x0 holds ( (Proj (i,n)) * g is_differentiable_in x0 & (Proj (i,n)) * (diff (g,x0)) = diff (((Proj (i,n)) * g),x0) ) proof let m, n be non empty Element of NAT ; ::_thesis: for g being PartFunc of (REAL-NS m),(REAL-NS n) for x0 being Point of (REAL-NS m) for i being Element of NAT st 1 <= i & i <= n & g is_differentiable_in x0 holds ( (Proj (i,n)) * g is_differentiable_in x0 & (Proj (i,n)) * (diff (g,x0)) = diff (((Proj (i,n)) * g),x0) ) let g be PartFunc of (REAL-NS m),(REAL-NS n); ::_thesis: for x0 being Point of (REAL-NS m) for i being Element of NAT st 1 <= i & i <= n & g is_differentiable_in x0 holds ( (Proj (i,n)) * g is_differentiable_in x0 & (Proj (i,n)) * (diff (g,x0)) = diff (((Proj (i,n)) * g),x0) ) let x0 be Point of (REAL-NS m); ::_thesis: for i being Element of NAT st 1 <= i & i <= n & g is_differentiable_in x0 holds ( (Proj (i,n)) * g is_differentiable_in x0 & (Proj (i,n)) * (diff (g,x0)) = diff (((Proj (i,n)) * g),x0) ) let i be Element of NAT ; ::_thesis: ( 1 <= i & i <= n & g is_differentiable_in x0 implies ( (Proj (i,n)) * g is_differentiable_in x0 & (Proj (i,n)) * (diff (g,x0)) = diff (((Proj (i,n)) * g),x0) ) ) assume A1: ( 1 <= i & i <= n & g is_differentiable_in x0 ) ; ::_thesis: ( (Proj (i,n)) * g is_differentiable_in x0 & (Proj (i,n)) * (diff (g,x0)) = diff (((Proj (i,n)) * g),x0) ) then consider N being Neighbourhood of x0 such that A2: ( N c= dom g & ex GR being RestFunc of (REAL-NS m),(REAL-NS n) st for x being Point of (REAL-NS m) st x in N holds (g /. x) - (g /. x0) = ((diff (g,x0)) . (x - x0)) + (GR /. (x - x0)) ) by NDIFF_1:def_7; consider GR being RestFunc of (REAL-NS m),(REAL-NS n) such that A3: for x being Point of (REAL-NS m) st x in N holds (g /. x) - (g /. x0) = ((diff (g,x0)) . (x - x0)) + (GR /. (x - x0)) by A2; set RLB0 = R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1)); reconsider DFG = diff (g,x0) as LinearOperator of (REAL-NS m),(REAL-NS n) by LOPBAN_1:def_9; reconsider PG = Proj (i,n) as Function of the carrier of (REAL-NS n), the carrier of (REAL-NS 1) ; PG * DFG is Function of the carrier of (REAL-NS m), the carrier of (REAL-NS 1) ; then reconsider L = (Proj (i,n)) * (diff (g,x0)) as Function of (REAL-NS m),(REAL-NS 1) ; A4: for x, y being VECTOR of (REAL-NS m) holds L . (x + y) = (L . x) + (L . y) proof let x, y be VECTOR of (REAL-NS m); ::_thesis: L . (x + y) = (L . x) + (L . y) A5: dom L = the carrier of (REAL-NS m) by FUNCT_2:def_1; A6: DFG . (x + y) = (DFG . x) + (DFG . y) by VECTSP_1:def_20; L . (x + y) = (Proj (i,n)) . (DFG . (x + y)) by A5, FUNCT_1:12 .= ((Proj (i,n)) . (DFG . x)) + ((Proj (i,n)) . (DFG . y)) by A6, Th26 .= ((Proj (i,n)) . (DFG . x)) + (L . y) by A5, FUNCT_1:12 ; hence L . (x + y) = (L . x) + (L . y) by A5, FUNCT_1:12; ::_thesis: verum end; for x being VECTOR of (REAL-NS m) for r being Real holds L . (r * x) = r * (L . x) proof let x be VECTOR of (REAL-NS m); ::_thesis: for r being Real holds L . (r * x) = r * (L . x) let r be Real; ::_thesis: L . (r * x) = r * (L . x) A7: dom L = the carrier of (REAL-NS m) by FUNCT_2:def_1; DFG . (r * x) = r * (DFG . x) by LOPBAN_1:def_5; then (Proj (i,n)) . (DFG . (r * x)) = r * ((Proj (i,n)) . (DFG . x)) by Th27; then L . (r * x) = r * ((Proj (i,n)) . (DFG . x)) by A7, FUNCT_1:12; hence L . (r * x) = r * (L . x) by A7, FUNCT_1:12; ::_thesis: verum end; then reconsider L = L as LinearOperator of (REAL-NS m),(REAL-NS 1) by A4, VECTSP_1:def_20, LOPBAN_1:def_5; reconsider L = L as Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))) by LOPBAN_1:def_9; A8: GR is total by NDIFF_1:def_5; then reconsider FGR = GR as Function of the carrier of (REAL-NS m), the carrier of (REAL-NS n) ; A9: (Proj (i,n)) * FGR is Function of the carrier of (REAL-NS m), the carrier of (REAL-NS 1) ; (Proj (i,n)) * GR is RestFunc of (REAL-NS m),(REAL-NS 1) proof A10: dom GR = the carrier of (REAL-NS m) by A8, PARTFUN1:def_2; reconsider R = (Proj (i,n)) * GR as PartFunc of (REAL-NS m),(REAL-NS 1) ; for r being Real st r > 0 holds ex d being Real st ( d > 0 & ( for z being Point of (REAL-NS m) st z <> 0. (REAL-NS m) & ||.z.|| < d holds (||.z.|| ") * ||.(R /. z).|| < r ) ) proof let r be Real; ::_thesis: ( r > 0 implies ex d being Real st ( d > 0 & ( for z being Point of (REAL-NS m) st z <> 0. (REAL-NS m) & ||.z.|| < d holds (||.z.|| ") * ||.(R /. z).|| < r ) ) ) assume r > 0 ; ::_thesis: ex d being Real st ( d > 0 & ( for z being Point of (REAL-NS m) st z <> 0. (REAL-NS m) & ||.z.|| < d holds (||.z.|| ") * ||.(R /. z).|| < r ) ) then consider d being Real such that A11: ( d > 0 & ( for z being Point of (REAL-NS m) st z <> 0. (REAL-NS m) & ||.z.|| < d holds (||.z.|| ") * ||.(GR /. z).|| < r ) ) by A8, NDIFF_1:23; take d ; ::_thesis: ( d > 0 & ( for z being Point of (REAL-NS m) st z <> 0. (REAL-NS m) & ||.z.|| < d holds (||.z.|| ") * ||.(R /. z).|| < r ) ) thus d > 0 by A11; ::_thesis: for z being Point of (REAL-NS m) st z <> 0. (REAL-NS m) & ||.z.|| < d holds (||.z.|| ") * ||.(R /. z).|| < r let z be Point of (REAL-NS m); ::_thesis: ( z <> 0. (REAL-NS m) & ||.z.|| < d implies (||.z.|| ") * ||.(R /. z).|| < r ) assume A12: ( z <> 0. (REAL-NS m) & ||.z.|| < d ) ; ::_thesis: (||.z.|| ") * ||.(R /. z).|| < r A13: GR /. z = GR . z by A10, PARTFUN1:def_6; A14: i in Seg n by A1; reconsider GRz = GR /. z as Point of (REAL-NS n) ; reconsider GRz1 = GRz as Element of REAL n by REAL_NS1:def_4; reconsider GRzi = GRz1 . i as Element of REAL ; dom (Proj (i,n)) = the carrier of (REAL-NS n) by PARTFUN1:def_2; then A15: z in dom ((Proj (i,n)) * GR) by A10, A13, FUNCT_1:11; then ((Proj (i,n)) * GR) . z = (Proj (i,n)) . (GR . z) by FUNCT_1:12 .= <*((proj (i,n)) . GRz1)*> by A13, PDIFF_1:def_4 ; then A16: ((Proj (i,n)) * GR) . z = <*GRzi*> by PDIFF_1:def_1; A17: abs GRzi <= ||.(GR /. z).|| by A14, REAL_NS1:9; A18: 0 <= ||.z.|| by NORMSP_1:4; 0 <= abs GRzi by COMPLEX1:46; then A19: (||.z.|| ") * (abs GRzi) <= (||.z.|| ") * ||.(GR /. z).|| by A17, A18, XREAL_1:66; (||.z.|| ") * ||.(GR /. z).|| < r by A11, A12; then A20: (||.z.|| ") * (abs GRzi) < r by A19, XXREAL_0:2; ((Proj (i,n)) * GR) . z in rng ((Proj (i,n)) * GR) by A15, FUNCT_1:3; then reconsider Rz = ((Proj (i,n)) * GR) . z as VECTOR of (REAL-NS 1) ; set VGRzi = <*GRzi*>; <*GRzi*> is Element of REAL 1 by FINSEQ_2:98; then ||.Rz.|| = |.<*GRzi*>.| by A16, REAL_NS1:1; then (||.z.|| ") * ||.Rz.|| < r by A20, JORDAN2C:10; hence (||.z.|| ") * ||.(R /. z).|| < r by A15, PARTFUN1:def_6; ::_thesis: verum end; hence (Proj (i,n)) * GR is RestFunc of (REAL-NS m),(REAL-NS 1) by A9, NDIFF_1:23; ::_thesis: verum end; then reconsider R = (Proj (i,n)) * GR as RestFunc of (REAL-NS m),(REAL-NS 1) ; set pg = (Proj (i,n)) * g; A21: dom (Proj (i,n)) = the carrier of (REAL-NS n) by FUNCT_2:def_1; then rng g c= dom (Proj (i,n)) ; then A22: dom g = dom ((Proj (i,n)) * g) by RELAT_1:27; A23: dom (Proj (i,n)) = REAL n by A21, REAL_NS1:def_4; A24: for x being Point of (REAL-NS m) st x in N holds (((Proj (i,n)) * g) /. x) - (((Proj (i,n)) * g) /. x0) = (L . (x - x0)) + (R /. (x - x0)) proof let x be Point of (REAL-NS m); ::_thesis: ( x in N implies (((Proj (i,n)) * g) /. x) - (((Proj (i,n)) * g) /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) now__::_thesis:_(_x_in_N_&_x_in_N_implies_(((Proj_(i,n))_*_g)_/._x)_-_(((Proj_(i,n))_*_g)_/._x0)_=_(L_._(x_-_x0))_+_(R_/._(x_-_x0))_) assume A25: x in N ; ::_thesis: ( x in N implies (((Proj (i,n)) * g) /. x) - (((Proj (i,n)) * g) /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) then A26: (g /. x) - (g /. x0) = ((diff (g,x0)) . (x - x0)) + (GR /. (x - x0)) by A3; A27: x0 in N by NFCONT_1:4; then A28: ( ((Proj (i,n)) * g) /. x = ((Proj (i,n)) * g) . x & ((Proj (i,n)) * g) /. x0 = ((Proj (i,n)) * g) . x0 ) by A2, A22, A25, PARTFUN1:def_6; A29: ( g /. x = g . x & g /. x0 = g . x0 ) by A2, A25, A27, PARTFUN1:def_6; reconsider PGSx = (((Proj (i,n)) * g) /. x) - (((Proj (i,n)) * g) /. x0) as Element of REAL 1 by REAL_NS1:def_4; ((Proj (i,n)) * g) . x in rng ((Proj (i,n)) * g) by A2, A22, A25, FUNCT_1:3; then reconsider PGdx = ((Proj (i,n)) * g) . x as Element of REAL 1 by REAL_NS1:def_4; ((Proj (i,n)) * g) . x0 in rng ((Proj (i,n)) * g) by A2, A22, A27, FUNCT_1:3; then reconsider PGdx0 = ((Proj (i,n)) * g) . x0 as Element of REAL 1 by REAL_NS1:def_4; g . x in rng g by A2, A25, FUNCT_1:3; then reconsider Gx = g . x as Element of REAL n by REAL_NS1:def_4; g . x0 in rng g by A2, A27, FUNCT_1:3; then reconsider Gx0 = g . x0 as Element of REAL n by REAL_NS1:def_4; set ProjGx = (Proj (i,n)) . (g . x); Gx in dom (Proj (i,n)) by A23; then (Proj (i,n)) . (g . x) in rng (Proj (i,n)) by FUNCT_1:3; then reconsider ProjGx = (Proj (i,n)) . (g . x) as Element of REAL 1 by REAL_NS1:def_4; set ProjGx0 = (Proj (i,n)) . (g . x0); Gx0 in dom (Proj (i,n)) by A23; then (Proj (i,n)) . (g . x0) in rng (Proj (i,n)) by FUNCT_1:3; then reconsider ProjGx0 = (Proj (i,n)) . (g . x0) as Element of REAL 1 by REAL_NS1:def_4; reconsider Gx1 = Gx as Element of (REAL-NS n) by REAL_NS1:def_4; reconsider Gx01 = Gx0 as Element of (REAL-NS n) by REAL_NS1:def_4; reconsider Gsx = g /. x as Element of REAL n by REAL_NS1:def_4; reconsider Gsx0 = g /. x0 as Element of REAL n by REAL_NS1:def_4; set dxx0 = x - x0; reconsider Ldxx0 = L . (x - x0) as Element of (REAL-NS 1) ; A30: dom R = the carrier of (REAL-NS m) by A9, PARTFUN1:def_2; then A31: R /. (x - x0) = R . (x - x0) by PARTFUN1:def_6; then reconsider Rdxx0 = R . (x - x0) as Element of (REAL-NS 1) ; reconsider Ldiff = (diff (g,x0)) . (x - x0) as Element of REAL n by REAL_NS1:def_4; set ProjLdiff = (Proj (i,n)) . Ldiff; (Proj (i,n)) . Ldiff in rng (Proj (i,n)) by A21, FUNCT_1:3; then reconsider ProjLdiff = (Proj (i,n)) . Ldiff as Element of REAL 1 by REAL_NS1:def_4; A32: dom GR = the carrier of (REAL-NS m) by A8, PARTFUN1:def_2; then GR . (x - x0) in rng GR by FUNCT_1:3; then reconsider Rdiff = GR . (x - x0) as Element of REAL n by REAL_NS1:def_4; A33: Rdiff = GR /. (x - x0) by A32, PARTFUN1:def_6; set ProjRdiff = (Proj (i,n)) . Rdiff; (Proj (i,n)) . Rdiff in rng (Proj (i,n)) by A23, FUNCT_1:3; then reconsider ProjRdiff = (Proj (i,n)) . Rdiff as Element of REAL 1 by REAL_NS1:def_4; dom L = the carrier of (REAL-NS m) by FUNCT_2:def_1; then ( L . (x - x0) = (Proj (i,n)) . Ldiff & R . (x - x0) = (Proj (i,n)) . Rdiff ) by A30, FUNCT_1:12; then A34: Ldxx0 + Rdxx0 = ProjLdiff + ProjRdiff by REAL_NS1:2; (Proj (i,n)) . Ldiff = <*((proj (i,n)) . Ldiff)*> by PDIFF_1:def_4; then A35: (Proj (i,n)) . Ldiff = <*(Ldiff . i)*> by PDIFF_1:def_1; Rdiff in dom (Proj (i,n)) by A23; then (Proj (i,n)) . Rdiff = <*((proj (i,n)) . Rdiff)*> by PDIFF_1:def_4; then A36: (Proj (i,n)) . Rdiff = <*(Rdiff . i)*> by PDIFF_1:def_1; reconsider diffGR = ((diff (g,x0)) . (x - x0)) + (GR /. (x - x0)) as Element of REAL n by REAL_NS1:def_4; reconsider Rsdiff = GR /. (x - x0) as Element of REAL n by REAL_NS1:def_4; PGSx = PGdx - PGdx0 by A28, REAL_NS1:5 .= ProjGx - PGdx0 by A2, A22, A25, FUNCT_1:12 .= ProjGx - ProjGx0 by A2, A22, A27, FUNCT_1:12 .= <*((proj (i,n)) . Gx1)*> - ProjGx0 by PDIFF_1:def_4 .= <*((proj (i,n)) . Gx1)*> - <*((proj (i,n)) . Gx01)*> by PDIFF_1:def_4 .= <*(Gx . i)*> - <*((proj (i,n)) . Gx01)*> by PDIFF_1:def_1 .= <*(Gx . i)*> - <*(Gx0 . i)*> by PDIFF_1:def_1 .= <*((Gx . i) - (Gx0 . i))*> by RVSUM_1:29 .= <*((Gsx - Gsx0) . i)*> by A29, RVSUM_1:27 .= <*(diffGR . i)*> by A26, REAL_NS1:5 .= <*((Ldiff + Rsdiff) . i)*> by REAL_NS1:2 .= <*((Ldiff . i) + (Rsdiff . i))*> by RVSUM_1:11 ; hence ( x in N implies (((Proj (i,n)) * g) /. x) - (((Proj (i,n)) * g) /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) by A31, A34, A35, A36, A33, RVSUM_1:13; ::_thesis: verum end; hence ( x in N implies (((Proj (i,n)) * g) /. x) - (((Proj (i,n)) * g) /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) ; ::_thesis: verum end; hence (Proj (i,n)) * g is_differentiable_in x0 by A2, A22, NDIFF_1:def_6; ::_thesis: (Proj (i,n)) * (diff (g,x0)) = diff (((Proj (i,n)) * g),x0) hence (Proj (i,n)) * (diff (g,x0)) = diff (((Proj (i,n)) * g),x0) by A2, A22, A24, NDIFF_1:def_7; ::_thesis: verum end; theorem :: PDIFF_6:29 for m, n being non empty Element of NAT for g being PartFunc of (REAL-NS m),(REAL-NS n) for x0 being Point of (REAL-NS m) holds ( g is_differentiable_in x0 iff for i being Element of NAT st 1 <= i & i <= n holds (Proj (i,n)) * g is_differentiable_in x0 ) proof let m, n be non empty Element of NAT ; ::_thesis: for g being PartFunc of (REAL-NS m),(REAL-NS n) for x0 being Point of (REAL-NS m) holds ( g is_differentiable_in x0 iff for i being Element of NAT st 1 <= i & i <= n holds (Proj (i,n)) * g is_differentiable_in x0 ) let g be PartFunc of (REAL-NS m),(REAL-NS n); ::_thesis: for x0 being Point of (REAL-NS m) holds ( g is_differentiable_in x0 iff for i being Element of NAT st 1 <= i & i <= n holds (Proj (i,n)) * g is_differentiable_in x0 ) let x0 be Point of (REAL-NS m); ::_thesis: ( g is_differentiable_in x0 iff for i being Element of NAT st 1 <= i & i <= n holds (Proj (i,n)) * g is_differentiable_in x0 ) set RB = 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)) * g is_differentiable_in x0 ) implies g is_differentiable_in x0 ) proof assume A1: for i being Element of NAT st 1 <= i & i <= n holds (Proj (i,n)) * g is_differentiable_in x0 ; ::_thesis: g is_differentiable_in x0 defpred S1[ Element of NAT , Element of REAL ] means ( $2 > 0 & { y where y is Point of (REAL-NS m) : ||.(y - x0).|| < $2 } c= dom ((Proj ($1,n)) * g) & ex Ri being RestFunc of (REAL-NS m),(REAL-NS 1) st for x being Point of (REAL-NS m) st x in { y where y is Point of (REAL-NS m) : ||.(y - x0).|| < $2 } holds (((Proj ($1,n)) * g) /. x) - (((Proj ($1,n)) * g) /. x0) = ((diff (((Proj ($1,n)) * g),x0)) . (x - x0)) + (Ri /. (x - x0)) ); A2: for k being Element of NAT st k in Seg n holds ex dk being Element of REAL st S1[k,dk] proof let k be Element of NAT ; ::_thesis: ( k in Seg n implies ex dk being Element of REAL st S1[k,dk] ) assume k in Seg n ; ::_thesis: ex dk being Element of REAL st S1[k,dk] then ( 1 <= k & k <= n ) by FINSEQ_1:1; then (Proj (k,n)) * g is_differentiable_in x0 by A1; then consider Nk being Neighbourhood of x0 such that A3: ( Nk c= dom ((Proj (k,n)) * g) & ex Rk being RestFunc of (REAL-NS m),(REAL-NS 1) st for x being Point of (REAL-NS m) st x in Nk holds (((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((diff (((Proj (k,n)) * g),x0)) . (x - x0)) + (Rk /. (x - x0)) ) by NDIFF_1:def_7; consider dk being Real such that A4: ( 0 < dk & { y where y is Point of (REAL-NS m) : ||.(y - x0).|| < dk } c= Nk ) by NFCONT_1:def_1; reconsider dk = dk as Element of REAL ; take dk ; ::_thesis: S1[k,dk] thus 0 < dk by A4; ::_thesis: ( { y where y is Point of (REAL-NS m) : ||.(y - x0).|| < dk } c= dom ((Proj (k,n)) * g) & ex Ri being RestFunc of (REAL-NS m),(REAL-NS 1) st for x being Point of (REAL-NS m) st x in { y where y is Point of (REAL-NS m) : ||.(y - x0).|| < dk } holds (((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((diff (((Proj (k,n)) * g),x0)) . (x - x0)) + (Ri /. (x - x0)) ) thus { y where y is Point of (REAL-NS m) : ||.(y - x0).|| < dk } c= dom ((Proj (k,n)) * g) by A4, A3, XBOOLE_1:1; ::_thesis: ex Ri being RestFunc of (REAL-NS m),(REAL-NS 1) st for x being Point of (REAL-NS m) st x in { y where y is Point of (REAL-NS m) : ||.(y - x0).|| < dk } holds (((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((diff (((Proj (k,n)) * g),x0)) . (x - x0)) + (Ri /. (x - x0)) thus ex Rk being RestFunc of (REAL-NS m),(REAL-NS 1) st for x being Point of (REAL-NS m) st x in { y where y is Point of (REAL-NS m) : ||.(y - x0).|| < dk } holds (((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((diff (((Proj (k,n)) * g),x0)) . (x - x0)) + (Rk /. (x - x0)) ::_thesis: verum proof consider Rk being RestFunc of (REAL-NS m),(REAL-NS 1) such that A5: for x being Point of (REAL-NS m) st x in Nk holds (((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((diff (((Proj (k,n)) * g),x0)) . (x - x0)) + (Rk /. (x - x0)) by A3; take Rk ; ::_thesis: for x being Point of (REAL-NS m) st x in { y where y is Point of (REAL-NS m) : ||.(y - x0).|| < dk } holds (((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((diff (((Proj (k,n)) * g),x0)) . (x - x0)) + (Rk /. (x - x0)) thus for x being Point of (REAL-NS m) st x in { y where y is Point of (REAL-NS m) : ||.(y - x0).|| < dk } holds (((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((diff (((Proj (k,n)) * g),x0)) . (x - x0)) + (Rk /. (x - x0)) by A4, A5; ::_thesis: verum end; end; consider d being FinSequence of REAL such that A6: ( dom d = Seg n & ( for k being Element of NAT st k in Seg n holds S1[k,d /. k] ) ) from RECDEF_1:sch_17(A2); set d0 = min d; len d = n by A6, FINSEQ_1:def_3; then A7: min_p d in dom d by RFINSEQ2:def_2; then d /. (min_p d) > 0 by A6; then A8: min d > 0 by A7, PARTFUN1:def_6; defpred S2[ set , set ] means ex y being Element of REAL n st ( $2 = y & ( for i being Element of NAT st i in Seg n holds y . i = (proj (1,1)) . ((diff (((Proj (i,n)) * g),x0)) . $1) ) ); A9: for x being Point of (REAL-NS m) ex y being Point of (REAL-NS n) st S2[x,y] proof let x be Point of (REAL-NS m); ::_thesis: ex y being Point of (REAL-NS n) st S2[x,y] defpred S3[ Element of NAT , set ] means $2 = (proj (1,1)) . ((diff (((Proj ($1,n)) * g),x0)) . x); A10: for i being Element of NAT st i in Seg n holds ex r being Element of REAL st S3[i,r] ; consider y being FinSequence of REAL such that A11: ( dom y = Seg n & ( for i being Element of NAT st i in Seg n holds S3[i,y /. i] ) ) from RECDEF_1:sch_17(A10); len y = n by A11, FINSEQ_1:def_3; then reconsider y = y as Element of REAL n by FINSEQ_2:92; A12: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_Seg_n_holds_ y_._i_=_(proj_(1,1))_._((diff_(((Proj_(i,n))_*_g),x0))_._x) let i be Element of NAT ; ::_thesis: ( i in Seg n implies y . i = (proj (1,1)) . ((diff (((Proj (i,n)) * g),x0)) . x) ) assume i in Seg n ; ::_thesis: y . i = (proj (1,1)) . ((diff (((Proj (i,n)) * g),x0)) . x) then ( S3[i,y /. i] & y /. i = y . i ) by A11, PARTFUN1:def_6; hence y . i = (proj (1,1)) . ((diff (((Proj (i,n)) * g),x0)) . x) ; ::_thesis: verum end; reconsider y0 = y as Point of (REAL-NS n) by REAL_NS1:def_4; ex y being Element of REAL n st ( y0 = y & ( for i being Element of NAT st i in Seg n holds y . i = (proj (1,1)) . ((diff (((Proj (i,n)) * g),x0)) . x) ) ) by A12; hence ex y0 being Point of (REAL-NS n) st S2[x,y0] ; ::_thesis: verum end; consider L being Function of (REAL-NS m),(REAL-NS n) such that A13: for x being Point of (REAL-NS m) holds S2[x,L . x] from FUNCT_2:sch_3(A9); A14: for x, y being VECTOR of (REAL-NS m) holds L . (x + y) = (L . x) + (L . y) proof let x, y be VECTOR of (REAL-NS m); ::_thesis: L . (x + y) = (L . x) + (L . y) consider Lx being Element of REAL n such that A15: ( L . x = Lx & ( for i being Element of NAT st i in Seg n holds Lx . i = (proj (1,1)) . ((diff (((Proj (i,n)) * g),x0)) . x) ) ) by A13; consider Ly being Element of REAL n such that A16: ( L . y = Ly & ( for i being Element of NAT st i in Seg n holds Ly . i = (proj (1,1)) . ((diff (((Proj (i,n)) * g),x0)) . y) ) ) by A13; consider Lxy being Element of REAL n such that A17: ( L . (x + y) = Lxy & ( for i being Element of NAT st i in Seg n holds Lxy . i = (proj (1,1)) . ((diff (((Proj (i,n)) * g),x0)) . (x + y)) ) ) by A13; dom Lxy = Seg n by FINSEQ_1:89; then A18: dom Lxy = dom (Lx + Ly) by FINSEQ_1:89; for i0 being Nat st i0 in dom Lxy holds Lxy . i0 = (Lx + Ly) . i0 proof let i0 be Nat; ::_thesis: ( i0 in dom Lxy implies Lxy . i0 = (Lx + Ly) . i0 ) reconsider i = i0 as Element of NAT by ORDINAL1:def_12; assume i0 in dom Lxy ; ::_thesis: Lxy . i0 = (Lx + Ly) . i0 then i in Seg n by FINSEQ_1:89; then A19: ( Lxy . i = (proj (1,1)) . ((diff (((Proj (i,n)) * g),x0)) . (x + y)) & Lx . i = (proj (1,1)) . ((diff (((Proj (i,n)) * g),x0)) . x) & Ly . i = (proj (1,1)) . ((diff (((Proj (i,n)) * g),x0)) . y) ) by A15, A16, A17; diff (((Proj (i,n)) * g),x0) is LinearOperator of (REAL-NS m),(REAL-NS 1) by LOPBAN_1:def_9; then A20: (diff (((Proj (i,n)) * g),x0)) . (x + y) = ((diff (((Proj (i,n)) * g),x0)) . x) + ((diff (((Proj (i,n)) * g),x0)) . y) by VECTSP_1:def_20; reconsider Diffxy = (diff (((Proj (i,n)) * g),x0)) . (x + y) as Element of REAL 1 by REAL_NS1:def_4; reconsider Diffx = (diff (((Proj (i,n)) * g),x0)) . x as Element of REAL 1 by REAL_NS1:def_4; reconsider Diffy = (diff (((Proj (i,n)) * g),x0)) . y as Element of REAL 1 by REAL_NS1:def_4; Diffxy = Diffx + Diffy by A20, REAL_NS1:2; then Lxy . i0 = (Diffx + Diffy) . 1 by A19, PDIFF_1:def_1; then Lxy . i0 = (Diffx . 1) + (Diffy . 1) by RVSUM_1:11; then Lxy . i0 = (Lx . i0) + (Diffy . 1) by A19, PDIFF_1:def_1; then Lxy . i0 = (Lx . i0) + (Ly . i0) by A19, PDIFF_1:def_1; hence Lxy . i0 = (Lx + Ly) . i0 by RVSUM_1:11; ::_thesis: verum end; then Lxy = Lx + Ly by A18, FINSEQ_1:13; hence L . (x + y) = (L . x) + (L . y) by A15, A16, A17, REAL_NS1:2; ::_thesis: verum end; for x being VECTOR of (REAL-NS m) for r being Real holds L . (r * x) = r * (L . x) proof let x be VECTOR of (REAL-NS m); ::_thesis: for r being Real holds L . (r * x) = r * (L . x) let r be Real; ::_thesis: L . (r * x) = r * (L . x) consider Lx being Element of REAL n such that A21: ( L . x = Lx & ( for i being Element of NAT st i in Seg n holds Lx . i = (proj (1,1)) . ((diff (((Proj (i,n)) * g),x0)) . x) ) ) by A13; consider Lrx being Element of REAL n such that A22: ( L . (r * x) = Lrx & ( for i being Element of NAT st i in Seg n holds Lrx . i = (proj (1,1)) . ((diff (((Proj (i,n)) * g),x0)) . (r * x)) ) ) by A13; dom (r * Lx) = Seg n by FINSEQ_1:89; then A23: dom (r * Lx) = dom Lrx by FINSEQ_1:89; for i0 being Nat st i0 in dom (r * Lx) holds (r * Lx) . i0 = Lrx . i0 proof let i0 be Nat; ::_thesis: ( i0 in dom (r * Lx) implies (r * Lx) . i0 = Lrx . i0 ) reconsider i = i0 as Element of NAT by ORDINAL1:def_12; assume i0 in dom (r * Lx) ; ::_thesis: (r * Lx) . i0 = Lrx . i0 then i0 in Seg n by FINSEQ_1:89; then A24: ( Lx . i = (proj (1,1)) . ((diff (((Proj (i,n)) * g),x0)) . x) & Lrx . i = (proj (1,1)) . ((diff (((Proj (i,n)) * g),x0)) . (r * x)) ) by A21, A22; diff (((Proj (i,n)) * g),x0) is LinearOperator of (REAL-NS m),(REAL-NS 1) by LOPBAN_1:def_9; then A25: (diff (((Proj (i,n)) * g),x0)) . (r * x) = r * ((diff (((Proj (i,n)) * g),x0)) . x) by LOPBAN_1:def_5; reconsider Diffrx = (diff (((Proj (i,n)) * g),x0)) . (r * x) as Element of REAL 1 by REAL_NS1:def_4; reconsider Diffx = (diff (((Proj (i,n)) * g),x0)) . x as Element of REAL 1 by REAL_NS1:def_4; Diffrx = r * Diffx by A25, REAL_NS1:3; then Lrx . i0 = (r * Diffx) . 1 by A24, PDIFF_1:def_1; then Lrx . i0 = r * (Diffx . 1) by RVSUM_1:45; then Lrx . i0 = r * (Lx . i0) by A24, PDIFF_1:def_1; hence (r * Lx) . i0 = Lrx . i0 by RVSUM_1:45; ::_thesis: verum end; then r * Lx = Lrx by A23, FINSEQ_1:13; hence L . (r * x) = r * (L . x) by A21, A22, REAL_NS1:3; ::_thesis: verum end; then reconsider L = L as LinearOperator of (REAL-NS m),(REAL-NS n) by A14, VECTSP_1:def_20, LOPBAN_1:def_5; reconsider L0 = L as Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))) by LOPBAN_1:def_9; deffunc H1( Element of (REAL-NS m)) -> Element of the carrier of (REAL-NS n) = ((g /. ($1 + x0)) - (g /. x0)) - (L . $1); consider R being Function of (REAL-NS m),(REAL-NS n) such that A26: for x being Element of (REAL-NS m) holds R . x = H1(x) from FUNCT_2:sch_4(); A27: for x being Element of (REAL-NS m) for i being Element of NAT st i in Seg n & x + x0 in dom g holds ((Proj (i,n)) * R) . x = ((((Proj (i,n)) * g) /. (x + x0)) - (((Proj (i,n)) * g) /. x0)) - (((Proj (i,n)) * L) . x) proof let x be Element of (REAL-NS m); ::_thesis: for i being Element of NAT st i in Seg n & x + x0 in dom g holds ((Proj (i,n)) * R) . x = ((((Proj (i,n)) * g) /. (x + x0)) - (((Proj (i,n)) * g) /. x0)) - (((Proj (i,n)) * L) . x) let i be Element of NAT ; ::_thesis: ( i in Seg n & x + x0 in dom g implies ((Proj (i,n)) * R) . x = ((((Proj (i,n)) * g) /. (x + x0)) - (((Proj (i,n)) * g) /. x0)) - (((Proj (i,n)) * L) . x) ) assume that A28: i in Seg n and A29: x + x0 in dom g ; ::_thesis: ((Proj (i,n)) * R) . x = ((((Proj (i,n)) * g) /. (x + x0)) - (((Proj (i,n)) * g) /. x0)) - (((Proj (i,n)) * L) . x) x0 - x0 = 0. (REAL-NS m) by RLVECT_1:15; then x0 - x0 = 0* m by REAL_NS1:def_4; then ||.(x0 - x0).|| = |.(0* m).| by REAL_NS1:1; then A30: ||.(x0 - x0).|| = 0 by EUCLID:7; A31: ( 0 < d /. i & { y where y is Point of (REAL-NS m) : ||.(y - x0).|| < d /. i } c= dom ((Proj (i,n)) * g) ) by A28, A6; then x0 in { y where y is Point of (REAL-NS m) : ||.(y - x0).|| < d /. i } by A30; then A32: x0 in dom ((Proj (i,n)) * g) by A31; A33: dom ((Proj (i,n)) * g) c= dom g by RELAT_1:25; reconsider gxx0 = g /. (x + x0), gx0 = g /. x0, Lx = L . x as Element of REAL n by REAL_NS1:def_4; reconsider Lx1 = L . x as Point of (REAL-NS n) ; A34: ( - gx0 = (- 1) * (g /. x0) & - Lx = (- 1) * (L . x) ) by REAL_NS1:3; then gxx0 + (- gx0) = (g /. (x + x0)) + ((- 1) * (g /. x0)) by REAL_NS1:2; then A35: (gxx0 + (- gx0)) + (- Lx) = ((g /. (x + x0)) + ((- 1) * (g /. x0))) + ((- 1) * (L . x)) by A34, REAL_NS1:2; gxx0 - gx0 = (g /. (x + x0)) - (g /. x0) by REAL_NS1:5; then A36: ((g /. (x + x0)) - (g /. x0)) - (L . x) = (gxx0 - gx0) - Lx by REAL_NS1:5; ((Proj (i,n)) * R) . x = (Proj (i,n)) . (R . x) by FUNCT_2:15; then ((Proj (i,n)) * R) . x = (Proj (i,n)) . (((g /. (x + x0)) - (g /. x0)) - (L . x)) by A26; then ((Proj (i,n)) * R) . x = ((Proj (i,n)) . ((g /. (x + x0)) + ((- 1) * (g /. x0)))) + ((Proj (i,n)) . ((- 1) * (L . x))) by A36, A35, Th26; then A37: ((Proj (i,n)) * R) . x = (((Proj (i,n)) . (g /. (x + x0))) + ((Proj (i,n)) . ((- 1) * (g /. x0)))) + ((Proj (i,n)) . ((- 1) * (L . x))) by Th26; ( (Proj (i,n)) . ((- 1) * (g /. x0)) = (- 1) * ((Proj (i,n)) . (g /. x0)) & (Proj (i,n)) . ((- 1) * Lx1) = (- 1) * ((Proj (i,n)) . Lx1) ) by Th27; then ((Proj (i,n)) * R) . x = (((Proj (i,n)) . (g /. (x + x0))) + (- ((Proj (i,n)) . (g /. x0)))) + ((- 1) * ((Proj (i,n)) . (L . x))) by A37, RLVECT_1:16; then ((Proj (i,n)) * R) . x = (((Proj (i,n)) . (g /. (x + x0))) + (- ((Proj (i,n)) . (g /. x0)))) + (- ((Proj (i,n)) . (L . x))) by RLVECT_1:16; then ((Proj (i,n)) * R) . x = (((Proj (i,n)) . (g /. (x + x0))) - ((Proj (i,n)) . (g /. x0))) + (- ((Proj (i,n)) . (L . x))) by RLVECT_1:def_11; then A38: ((Proj (i,n)) * R) . x = (((Proj (i,n)) . (g /. (x + x0))) - ((Proj (i,n)) . (g /. x0))) - ((Proj (i,n)) . (L . x)) by RLVECT_1:def_11; ( g /. (x + x0) in the carrier of (REAL-NS n) & g /. x0 in the carrier of (REAL-NS n) ) ; then A39: ( g /. (x + x0) in dom (Proj (i,n)) & g /. x0 in dom (Proj (i,n)) ) by FUNCT_2:def_1; A40: (Proj (i,n)) . (g /. (x + x0)) = (Proj (i,n)) /. (g /. (x + x0)) .= ((Proj (i,n)) * g) /. (x + x0) by A29, A39, PARTFUN2:4 ; (Proj (i,n)) . (g /. x0) = (Proj (i,n)) /. (g /. x0) .= ((Proj (i,n)) * g) /. x0 by A32, A33, A39, PARTFUN2:4 ; hence ((Proj (i,n)) * R) . x = ((((Proj (i,n)) * g) /. (x + x0)) - (((Proj (i,n)) * g) /. x0)) - (((Proj (i,n)) * L) . x) by A38, A40, FUNCT_2:15; ::_thesis: verum end; for r being Real st r > 0 holds ex d being Real st ( d > 0 & ( for z being Point of (REAL-NS m) st z <> 0. (REAL-NS m) & ||.z.|| < d holds (||.z.|| ") * ||.(R /. z).|| < r ) ) proof let r be Real; ::_thesis: ( r > 0 implies ex d being Real st ( d > 0 & ( for z being Point of (REAL-NS m) st z <> 0. (REAL-NS m) & ||.z.|| < d holds (||.z.|| ") * ||.(R /. z).|| < r ) ) ) assume A41: r > 0 ; ::_thesis: ex d being Real st ( d > 0 & ( for z being Point of (REAL-NS m) st z <> 0. (REAL-NS m) & ||.z.|| < d holds (||.z.|| ") * ||.(R /. z).|| < r ) ) set r0 = ((sqrt n) ") * r; A42: sqrt n > 0 by SQUARE_1:25; then A43: ((sqrt n) ") * r > 0 by A41, XREAL_1:129; defpred S3[ Element of NAT , Element of REAL ] means ( $2 > 0 & ( for z being Point of (REAL-NS m) st z <> 0. (REAL-NS m) & ||.z.|| < $2 holds (||.z.|| ") * ||.(((Proj ($1,n)) * R) /. z).|| < ((sqrt n) ") * r ) ); A44: for k being Element of NAT st k in Seg n holds ex dd being Element of REAL st S3[k,dd] proof let k be Element of NAT ; ::_thesis: ( k in Seg n implies ex dd being Element of REAL st S3[k,dd] ) assume A45: k in Seg n ; ::_thesis: ex dd being Element of REAL st S3[k,dd] then ( 1 <= k & k <= n ) by FINSEQ_1:1; then (Proj (k,n)) * g is_differentiable_in x0 by A1; then consider Nk being Neighbourhood of x0 such that A46: ( Nk c= dom ((Proj (k,n)) * g) & ex PR being RestFunc of (REAL-NS m),(REAL-NS 1) st for x being Point of (REAL-NS m) st x in Nk holds (((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((diff (((Proj (k,n)) * g),x0)) . (x - x0)) + (PR /. (x - x0)) ) by NDIFF_1:def_7; consider d0 being Real such that A47: ( 0 < d0 & { y where y is Point of (REAL-NS m) : ||.(y - x0).|| < d0 } c= Nk ) by NFCONT_1:def_1; consider PR being RestFunc of (REAL-NS m),(REAL-NS 1) such that A48: for x being Point of (REAL-NS m) st x in Nk holds (((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((diff (((Proj (k,n)) * g),x0)) . (x - x0)) + (PR /. (x - x0)) by A46; PR is total by NDIFF_1:def_5; then consider d1 being Real such that A49: ( d1 > 0 & ( for z being Point of (REAL-NS m) st z <> 0. (REAL-NS m) & ||.z.|| < d1 holds (||.z.|| ") * ||.(PR /. z).|| < ((sqrt n) ") * r ) ) by A43, NDIFF_1:23; set dd = min (d0,d1); take min (d0,d1) ; ::_thesis: S3[k, min (d0,d1)] for z being Point of (REAL-NS m) st z <> 0. (REAL-NS m) & ||.z.|| < min (d0,d1) holds (||.z.|| ") * ||.(((Proj (k,n)) * R) /. z).|| < ((sqrt n) ") * r proof let z be Point of (REAL-NS m); ::_thesis: ( z <> 0. (REAL-NS m) & ||.z.|| < min (d0,d1) implies (||.z.|| ") * ||.(((Proj (k,n)) * R) /. z).|| < ((sqrt n) ") * r ) assume A50: ( z <> 0. (REAL-NS m) & ||.z.|| < min (d0,d1) ) ; ::_thesis: (||.z.|| ") * ||.(((Proj (k,n)) * R) /. z).|| < ((sqrt n) ") * r min (d0,d1) <= d1 by XXREAL_0:17; then ||.z.|| < d1 by A50, XXREAL_0:2; then A51: (||.z.|| ") * ||.(PR /. z).|| < ((sqrt n) ") * r by A50, A49; min (d0,d1) <= d0 by XXREAL_0:17; then A52: ||.z.|| < d0 by A50, XXREAL_0:2; A53: (z + x0) - x0 = z by RLVECT_4:1; then A54: z + x0 in { y where y is Point of (REAL-NS m) : ||.(y - x0).|| < d0 } by A52; then z + x0 in Nk by A47; then A55: z + x0 in dom ((Proj (k,n)) * g) by A46; (((Proj (k,n)) * g) /. (z + x0)) - (((Proj (k,n)) * g) /. x0) = ((diff (((Proj (k,n)) * g),x0)) . ((z + x0) - x0)) + (PR /. ((z + x0) - x0)) by A54, A47, A48; then A56: PR /. z = ((((Proj (k,n)) * g) /. (z + x0)) - (((Proj (k,n)) * g) /. x0)) - ((diff (((Proj (k,n)) * g),x0)) . z) by A53, RLVECT_4:1; dom ((Proj (k,n)) * g) c= dom g by RELAT_1:25; then A57: ((Proj (k,n)) * R) . z = ((((Proj (k,n)) * g) /. (z + x0)) - (((Proj (k,n)) * g) /. x0)) - (((Proj (k,n)) * L) . z) by A55, A45, A27; consider y being Element of REAL n such that A58: ( L . z = y & ( for i being Element of NAT st i in Seg n holds y . i = (proj (1,1)) . ((diff (((Proj (i,n)) * g),x0)) . z) ) ) by A13; A59: y . k = (proj (1,1)) . ((diff (((Proj (k,n)) * g),x0)) . z) by A58, A45; (diff (((Proj (k,n)) * g),x0)) . z is Element of REAL 1 by REAL_NS1:def_4; then consider Dk being Element of REAL such that A60: (diff (((Proj (k,n)) * g),x0)) . z = <*Dk*> by FINSEQ_2:97; reconsider y1 = y as Point of (REAL-NS n) by REAL_NS1:def_4; dom L = the carrier of (REAL-NS m) by FUNCT_2:def_1; then ((Proj (k,n)) * L) . z = (Proj (k,n)) . (L . z) by FUNCT_1:13; then ((Proj (k,n)) * L) . z = <*((proj (k,n)) . y1)*> by A58, PDIFF_1:def_4; then ((Proj (k,n)) * L) . z = <*((proj (1,1)) . ((diff (((Proj (k,n)) * g),x0)) . z))*> by A59, PDIFF_1:def_1; hence (||.z.|| ") * ||.(((Proj (k,n)) * R) /. z).|| < ((sqrt n) ") * r by A51, A56, A57, A60, PDIFF_1:1; ::_thesis: verum end; hence S3[k, min (d0,d1)] by A47, A49, XXREAL_0:21; ::_thesis: verum end; consider dd being FinSequence of REAL such that A61: ( dom dd = Seg n & ( for i being Element of NAT st i in Seg n holds S3[i,dd /. i] ) ) from RECDEF_1:sch_17(A44); set d = min dd; take min dd ; ::_thesis: ( min dd > 0 & ( for z being Point of (REAL-NS m) st z <> 0. (REAL-NS m) & ||.z.|| < min dd holds (||.z.|| ") * ||.(R /. z).|| < r ) ) len dd = n by A61, FINSEQ_1:def_3; then A62: min_p dd in dom dd by RFINSEQ2:def_2; then A63: dd /. (min_p dd) > 0 by A61; for z being Point of (REAL-NS m) st z <> 0. (REAL-NS m) & ||.z.|| < min dd holds (||.z.|| ") * ||.(R /. z).|| < r proof let z be Point of (REAL-NS m); ::_thesis: ( z <> 0. (REAL-NS m) & ||.z.|| < min dd implies (||.z.|| ") * ||.(R /. z).|| < r ) assume A64: ( z <> 0. (REAL-NS m) & ||.z.|| < min dd ) ; ::_thesis: (||.z.|| ") * ||.(R /. z).|| < r reconsider Rz = R /. z as Element of REAL n by REAL_NS1:def_4; reconsider R0 = n |-> ((||.z.|| * (((sqrt n) ") * r)) ^2) as Element of n -tuples_on REAL ; reconsider SRz = sqr Rz as Element of n -tuples_on REAL ; ||.z.|| <> 0 by A64, NORMSP_0:def_5; then A65: ||.z.|| > 0 by NORMSP_1:4; A66: for i0 being Nat st i0 in Seg n holds SRz . i0 < R0 . i0 proof let i0 be Nat; ::_thesis: ( i0 in Seg n implies SRz . i0 < R0 . i0 ) reconsider i = i0 as Element of NAT by ORDINAL1:def_12; assume A67: i0 in Seg n ; ::_thesis: SRz . i0 < R0 . i0 then i in dom Rz by FINSEQ_2:124; then (sqr Rz) . i = sqrreal . (Rz . i) by FUNCT_1:13; then A68: (sqr Rz) . i = (Rz . i) ^2 by RVSUM_1:def_2; ( 1 <= i & i <= n ) by A67, FINSEQ_1:1; then ( 1 <= i & i <= len dd ) by A61, FINSEQ_1:def_3; then min dd <= dd . i by RFINSEQ2:2; then min dd <= dd /. i by A67, A61, PARTFUN1:def_6; then ||.z.|| < dd /. i by A64, XXREAL_0:2; then (||.z.|| ") * ||.(((Proj (i,n)) * R) /. z).|| < ((sqrt n) ") * r by A64, A67, A61; then A69: ||.(((Proj (i,n)) * R) /. z).|| < (((sqrt n) ") * r) / (||.z.|| ") by A65, XREAL_1:81; reconsider Rzi = <*(Rz . i)*> as Element of REAL 1 by FINSEQ_2:98; ((Proj (i,n)) * R) . z = (Proj (i,n)) . (R . z) by FUNCT_2:15; then ((Proj (i,n)) * R) . z = <*((proj (i,n)) . Rz)*> by PDIFF_1:def_4; then ((Proj (i,n)) * R) . z = <*(Rz . i)*> by PDIFF_1:def_1; then ||.(((Proj (i,n)) * R) . z).|| = |.Rzi.| by REAL_NS1:1; then |.(Rz . i).| < ||.z.|| * (((sqrt n) ") * r) by A69, JORDAN2C:10; then |.(Rz . i).| ^2 < (||.z.|| * (((sqrt n) ") * r)) ^2 by COMPLEX1:46, SQUARE_1:16; then (Rz . i0) ^2 < (||.z.|| * (((sqrt n) ") * r)) ^2 by COMPLEX1:75; hence SRz . i0 < R0 . i0 by A67, A68, FINSEQ_2:57; ::_thesis: verum end; A70: for i being Nat st i in dom (sqr Rz) holds 0 <= (sqr Rz) . i proof let i be Nat; ::_thesis: ( i in dom (sqr Rz) implies 0 <= (sqr Rz) . i ) assume i in dom (sqr Rz) ; ::_thesis: 0 <= (sqr Rz) . i then ( i in dom (sqrreal * Rz) & dom (sqrreal * Rz) c= dom Rz ) by RELAT_1:25; then (sqr Rz) . i = sqrreal . (Rz . i) by FUNCT_1:13; then (sqr Rz) . i = (Rz . i) ^2 by RVSUM_1:def_2; hence 0 <= (sqr Rz) . i by XREAL_1:63; ::_thesis: verum end; A71: (||.z.|| * (((sqrt n) ") * r)) ^2 >= 0 by XREAL_1:63; A72: ex i being Nat st ( i in Seg n & SRz . i < R0 . i ) proof take 1 ; ::_thesis: ( 1 in Seg n & SRz . 1 < R0 . 1 ) 1 <= n by NAT_1:14; hence 1 in Seg n ; ::_thesis: SRz . 1 < R0 . 1 hence SRz . 1 < R0 . 1 by A66; ::_thesis: verum end; A73: sqrt n > 0 by SQUARE_1:25; for i0 being Nat st i0 in Seg n holds SRz . i0 <= R0 . i0 by A66; then Sum SRz < Sum R0 by A72, RVSUM_1:83; then Sum (sqr Rz) < n * ((||.z.|| * (((sqrt n) ") * r)) ^2) by RVSUM_1:80; then |.Rz.| < sqrt (n * ((||.z.|| * (((sqrt n) ") * r)) ^2)) by A70, RVSUM_1:84, SQUARE_1:27; then |.Rz.| < (sqrt n) * (sqrt ((||.z.|| * (((sqrt n) ") * r)) ^2)) by A71, SQUARE_1:29; then |.Rz.| < (sqrt n) * |.(||.z.|| * (((sqrt n) ") * r)).| by COMPLEX1:72; then |.Rz.| < (sqrt n) * (||.z.|| * (((sqrt n) ") * r)) by A42, A41, A65, ABSVALUE:def_1; then |.Rz.| < ((sqrt n) * (((sqrt n) ") * r)) * ||.z.|| ; then |.Rz.| / ||.z.|| < (sqrt n) * (((sqrt n) ") * r) by A65, XREAL_1:83; then (||.z.|| ") * ||.(R /. z).|| < ((sqrt n) * ((sqrt n) ")) * r by REAL_NS1:1; then (||.z.|| ") * ||.(R /. z).|| < 1 * r by A73, XCMPLX_0:def_7; hence (||.z.|| ") * ||.(R /. z).|| < r ; ::_thesis: verum end; hence ( min dd > 0 & ( for z being Point of (REAL-NS m) st z <> 0. (REAL-NS m) & ||.z.|| < min dd holds (||.z.|| ") * ||.(R /. z).|| < r ) ) by A63, A62, PARTFUN1:def_6; ::_thesis: verum end; then reconsider R = R as RestFunc of (REAL-NS m),(REAL-NS n) by NDIFF_1:23; set N = { y where y is Point of (REAL-NS m) : ||.(y - x0).|| < min d } ; reconsider N = { y where y is Point of (REAL-NS m) : ||.(y - x0).|| < min d } as Neighbourhood of x0 by A8, NFCONT_1:3; now__::_thesis:_for_x_being_set_st_x_in_N_holds_ x_in_dom_g let x be set ; ::_thesis: ( x in N implies x in dom g ) assume x in N ; ::_thesis: x in dom g then consider y being Point of (REAL-NS m) such that A74: ( x = y & ||.(y - x0).|| < min d ) ; 1 <= n by NAT_1:14; then A75: ( 1 in Seg n & 1 in dom d ) by A6; then A76: { z where z is Point of (REAL-NS m) : ||.(z - x0).|| < d /. 1 } c= dom ((Proj (1,n)) * g) by A6; dom ((Proj (1,n)) * g) c= dom g by RELAT_1:25; then A77: { z where z is Point of (REAL-NS m) : ||.(z - x0).|| < d /. 1 } c= dom g by A76, XBOOLE_1:1; len d = n by A6, FINSEQ_1:def_3; then 1 <= len d by NAT_1:14; then min d <= d . 1 by RFINSEQ2:2; then min d <= d /. 1 by A75, PARTFUN1:def_6; then ||.(y - x0).|| < d /. 1 by A74, XXREAL_0:2; then y in { z where z is Point of (REAL-NS m) : ||.(z - x0).|| < d /. 1 } ; hence x in dom g by A74, A77; ::_thesis: verum end; then A78: N c= dom g by TARSKI:def_3; ex L being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))) ex R being RestFunc of (REAL-NS m),(REAL-NS n) st for x being Point of (REAL-NS m) st x in N holds (g /. x) - (g /. x0) = (L . (x - x0)) + (R /. (x - x0)) proof take L0 ; ::_thesis: ex R being RestFunc of (REAL-NS m),(REAL-NS n) st for x being Point of (REAL-NS m) st x in N holds (g /. x) - (g /. x0) = (L0 . (x - x0)) + (R /. (x - x0)) take R ; ::_thesis: for x being Point of (REAL-NS m) st x in N holds (g /. x) - (g /. x0) = (L0 . (x - x0)) + (R /. (x - x0)) hereby ::_thesis: verum let x be Point of (REAL-NS m); ::_thesis: ( x in N implies (g /. x) - (g /. x0) = (L0 . (x - x0)) + (R /. (x - x0)) ) assume x in N ; ::_thesis: (g /. x) - (g /. x0) = (L0 . (x - x0)) + (R /. (x - x0)) A79: dom R = the carrier of (REAL-NS m) by PARTFUN1:def_2; R . (x - x0) = ((g /. ((x - x0) + x0)) - (g /. x0)) - (L . (x - x0)) by A26; then R . (x - x0) = ((g /. (x - (x0 - x0))) - (g /. x0)) - (L0 . (x - x0)) by RLVECT_1:29; then R . (x - x0) = ((g /. (x - (x0 + (- x0)))) - (g /. x0)) - (L0 . (x - x0)) by RLVECT_1:def_11; then R . (x - x0) = ((g /. (x - (0. (REAL-NS m)))) - (g /. x0)) - (L0 . (x - x0)) by RLVECT_1:5; then R . (x - x0) = ((g /. x) - (g /. x0)) - (L0 . (x - x0)) by RLVECT_1:13; then R . (x - x0) = ((g /. x) - (g /. x0)) + (- (L0 . (x - x0))) by RLVECT_1:def_11; then R /. (x - x0) = ((g /. x) - (g /. x0)) + (- (L0 . (x - x0))) by A79, PARTFUN1:def_6; then (L0 . (x - x0)) + (R /. (x - x0)) = ((g /. x) - (g /. x0)) + ((- (L0 . (x - x0))) + (L0 . (x - x0))) by RLVECT_1:def_3; then (L0 . (x - x0)) + (R /. (x - x0)) = ((g /. x) - (g /. x0)) + (0. (REAL-NS n)) by RLVECT_1:5; hence (g /. x) - (g /. x0) = (L0 . (x - x0)) + (R /. (x - x0)) by RLVECT_1:4; ::_thesis: verum end; end; hence g is_differentiable_in x0 by A78, NDIFF_1:def_6; ::_thesis: verum end; hence ( g is_differentiable_in x0 iff for i being Element of NAT st 1 <= i & i <= n holds (Proj (i,n)) * g is_differentiable_in x0 ) by Th28; ::_thesis: verum end; definition let X be set ; let n, m be non empty Element of NAT ; let f be PartFunc of (REAL m),(REAL n); predf is_differentiable_on X means :Def4: :: PDIFF_6:def 4 ( X c= dom f & ( for x being Element of REAL m st x in X holds f | X is_differentiable_in x ) ); end; :: deftheorem Def4 defines is_differentiable_on PDIFF_6:def_4_:_ for X being set for n, m being non empty Element of NAT for f being PartFunc of (REAL m),(REAL n) holds ( f is_differentiable_on X iff ( X c= dom f & ( for x being Element of REAL m st x in X holds f | X is_differentiable_in x ) ) ); theorem Th30: :: PDIFF_6:30 for X being set for m, n being non empty Element of NAT for f being PartFunc of (REAL m),(REAL n) for g being PartFunc of (REAL-NS m),(REAL-NS n) st f = g holds ( f is_differentiable_on X iff g is_differentiable_on X ) proof let X be set ; ::_thesis: for m, n being non empty Element of NAT for f being PartFunc of (REAL m),(REAL n) for g being PartFunc of (REAL-NS m),(REAL-NS n) st f = g holds ( f is_differentiable_on X iff g is_differentiable_on X ) let m, n be non empty Element of NAT ; ::_thesis: for f being PartFunc of (REAL m),(REAL n) for g being PartFunc of (REAL-NS m),(REAL-NS n) st f = g holds ( f is_differentiable_on X iff g is_differentiable_on X ) let f be PartFunc of (REAL m),(REAL n); ::_thesis: for g being PartFunc of (REAL-NS m),(REAL-NS n) st f = g holds ( f is_differentiable_on X iff g is_differentiable_on X ) let g be PartFunc of (REAL-NS m),(REAL-NS n); ::_thesis: ( f = g implies ( f is_differentiable_on X iff g is_differentiable_on X ) ) assume A1: f = g ; ::_thesis: ( f is_differentiable_on X iff g is_differentiable_on X ) A2: now__::_thesis:_(_f_is_differentiable_on_X_implies_g_is_differentiable_on_X_) assume A3: f is_differentiable_on X ; ::_thesis: g is_differentiable_on X then A4: ( X c= dom f & ( for x being Element of REAL m st x in X holds f | X is_differentiable_in x ) ) by Def4; now__::_thesis:_for_y_being_Point_of_(REAL-NS_m)_st_y_in_X_holds_ g_|_X_is_differentiable_in_y let y be Point of (REAL-NS m); ::_thesis: ( y in X implies g | X is_differentiable_in y ) reconsider x = y as Element of REAL m by REAL_NS1:def_4; assume y in X ; ::_thesis: g | X is_differentiable_in y then f | X is_differentiable_in x by A3, Def4; then ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st ( f | X = g & x = y & g is_differentiable_in y ) by PDIFF_1:def_7; hence g | X is_differentiable_in y by A1; ::_thesis: verum end; hence g is_differentiable_on X by A1, A4, NDIFF_1:def_8; ::_thesis: verum end; now__::_thesis:_(_g_is_differentiable_on_X_implies_(_X_c=_dom_f_&_f_is_differentiable_on_X_)_) assume A5: g is_differentiable_on X ; ::_thesis: ( X c= dom f & f is_differentiable_on X ) hence X c= dom f by A1, NDIFF_1:def_8; ::_thesis: f is_differentiable_on X A6: ( X c= dom g & ( for x being Point of (REAL-NS m) st x in X holds g | X is_differentiable_in x ) ) by A5, NDIFF_1:def_8; now__::_thesis:_for_y_being_Element_of_REAL_m_st_y_in_X_holds_ f_|_X_is_differentiable_in_y let y be Element of REAL m; ::_thesis: ( y in X implies f | X is_differentiable_in y ) reconsider x = y as Point of (REAL-NS m) by REAL_NS1:def_4; assume y in X ; ::_thesis: f | X is_differentiable_in y then g | X is_differentiable_in x by A5, NDIFF_1:def_8; hence f | X is_differentiable_in y by A1, PDIFF_1:def_7; ::_thesis: verum end; hence f is_differentiable_on X by A1, A6, Def4; ::_thesis: verum end; hence ( f is_differentiable_on X iff g is_differentiable_on X ) by A2; ::_thesis: verum end; theorem :: PDIFF_6:31 for X being set for m, n being non empty Element of NAT for f being PartFunc of (REAL m),(REAL n) st f is_differentiable_on X holds X is Subset of (REAL m) proof let X be set ; ::_thesis: for m, n being non empty Element of NAT for f being PartFunc of (REAL m),(REAL n) st f is_differentiable_on X holds X is Subset of (REAL m) let m, n be non empty Element of NAT ; ::_thesis: for f being PartFunc of (REAL m),(REAL n) st f is_differentiable_on X holds X is Subset of (REAL m) let f be PartFunc of (REAL m),(REAL n); ::_thesis: ( f is_differentiable_on X implies X is Subset of (REAL m) ) assume f is_differentiable_on X ; ::_thesis: X is Subset of (REAL m) then X c= dom f by Def4; hence X is Subset of (REAL m) by XBOOLE_1:1; ::_thesis: verum end; theorem :: PDIFF_6:32 for m, n being non empty Element of NAT for f being PartFunc of (REAL m),(REAL n) for Z being Subset of (REAL m) st ex Z0 being Subset of (REAL-NS m) st ( Z = Z0 & Z0 is open ) holds ( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Element of REAL m st x in Z holds f is_differentiable_in x ) ) ) proof let m, n be non empty Element of NAT ; ::_thesis: for f being PartFunc of (REAL m),(REAL n) for Z being Subset of (REAL m) st ex Z0 being Subset of (REAL-NS m) st ( Z = Z0 & Z0 is open ) holds ( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Element of REAL m st x in Z holds f is_differentiable_in x ) ) ) let f be PartFunc of (REAL m),(REAL n); ::_thesis: for Z being Subset of (REAL m) st ex Z0 being Subset of (REAL-NS m) st ( Z = Z0 & Z0 is open ) holds ( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Element of REAL m st x in Z holds f is_differentiable_in x ) ) ) let Z be Subset of (REAL m); ::_thesis: ( ex Z0 being Subset of (REAL-NS m) st ( Z = Z0 & Z0 is open ) implies ( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Element of REAL m st x in Z holds f is_differentiable_in x ) ) ) ) assume ex Z0 being Subset of (REAL-NS m) st ( Z = Z0 & Z0 is open ) ; ::_thesis: ( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Element of REAL m st x in Z holds f is_differentiable_in x ) ) ) then consider Z0 being Subset of (REAL-NS m) such that A1: ( Z = Z0 & Z0 is open ) ; ( the carrier of (REAL-NS m) = REAL m & the carrier of (REAL-NS n) = REAL n ) by REAL_NS1:def_4; then reconsider g = f as PartFunc of (REAL-NS m),(REAL-NS n) ; A2: ( g is_differentiable_on Z0 iff ( Z0 c= dom g & ( for x being Point of (REAL-NS m) st x in Z0 holds g is_differentiable_in x ) ) ) by A1, NDIFF_1:31; thus ( f is_differentiable_on Z implies ( Z c= dom f & ( for x being Element of REAL m st x in Z holds f is_differentiable_in x ) ) ) ::_thesis: ( Z c= dom f & ( for x being Element of REAL m st x in Z holds f is_differentiable_in x ) implies f is_differentiable_on Z ) proof assume A3: f is_differentiable_on Z ; ::_thesis: ( Z c= dom f & ( for x being Element of REAL m st x in Z holds f is_differentiable_in x ) ) hence Z c= dom f by Def4; ::_thesis: for x being Element of REAL m st x in Z holds f is_differentiable_in x let x be Element of REAL m; ::_thesis: ( x in Z implies f is_differentiable_in x ) reconsider y = x as Point of (REAL-NS m) by REAL_NS1:def_4; assume x in Z ; ::_thesis: f is_differentiable_in x then g is_differentiable_in y by A1, A2, A3, Th30; hence f is_differentiable_in x by PDIFF_1:def_7; ::_thesis: verum end; assume A4: ( Z c= dom f & ( for x being Element of REAL m st x in Z holds f is_differentiable_in x ) ) ; ::_thesis: f is_differentiable_on Z now__::_thesis:_for_y_being_Point_of_(REAL-NS_m)_st_y_in_Z0_holds_ g_is_differentiable_in_y let y be Point of (REAL-NS m); ::_thesis: ( y in Z0 implies g is_differentiable_in y ) reconsider x = y as Element of REAL m by REAL_NS1:def_4; assume y in Z0 ; ::_thesis: g is_differentiable_in y then f is_differentiable_in x by A1, A4; then ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st ( f = g & x = y & g is_differentiable_in y ) by PDIFF_1:def_7; hence g is_differentiable_in y ; ::_thesis: verum end; hence f is_differentiable_on Z by A1, A2, A4, Th30; ::_thesis: verum end; theorem :: PDIFF_6:33 for m, n being non empty Element of NAT for f being PartFunc of (REAL m),(REAL n) for Z being Subset of (REAL m) st f is_differentiable_on Z holds ex Z0 being Subset of (REAL-NS m) st ( Z = Z0 & Z0 is open ) proof let m, n be non empty Element of NAT ; ::_thesis: for f being PartFunc of (REAL m),(REAL n) for Z being Subset of (REAL m) st f is_differentiable_on Z holds ex Z0 being Subset of (REAL-NS m) st ( Z = Z0 & Z0 is open ) let f be PartFunc of (REAL m),(REAL n); ::_thesis: for Z being Subset of (REAL m) st f is_differentiable_on Z holds ex Z0 being Subset of (REAL-NS m) st ( Z = Z0 & Z0 is open ) let Z be Subset of (REAL m); ::_thesis: ( f is_differentiable_on Z implies ex Z0 being Subset of (REAL-NS m) st ( Z = Z0 & Z0 is open ) ) assume A1: f is_differentiable_on Z ; ::_thesis: ex Z0 being Subset of (REAL-NS m) st ( Z = Z0 & Z0 is open ) ( the carrier of (REAL-NS m) = REAL m & the carrier of (REAL-NS n) = REAL n ) by REAL_NS1:def_4; then reconsider g = f as PartFunc of (REAL-NS m),(REAL-NS n) ; reconsider Z0 = Z as Subset of (REAL-NS m) by REAL_NS1:def_4; take Z0 ; ::_thesis: ( Z = Z0 & Z0 is open ) g is_differentiable_on Z0 by A1, Th30; hence ( Z = Z0 & Z0 is open ) by NDIFF_1:32; ::_thesis: verum end;