:: DIFF_1 semantic presentation begin definition let f be PartFunc of REAL,REAL; let h be real number ; func Shift (f,h) -> PartFunc of REAL,REAL means :Def1: :: DIFF_1:def 1 ( dom it = (- h) ++ (dom f) & ( for x being Real st x in (- h) ++ (dom f) holds it . x = f . (x + h) ) ); existence ex b1 being PartFunc of REAL,REAL st ( dom b1 = (- h) ++ (dom f) & ( for x being Real st x in (- h) ++ (dom f) holds b1 . x = f . (x + h) ) ) proof deffunc H1( Real) -> Element of REAL = f . (\$1 + h); set X = (- h) ++ (dom f); defpred S1[ set ] means \$1 in (- h) ++ (dom f); consider F being PartFunc of REAL,REAL such that A1: ( ( for x being Element of REAL holds ( x in dom F iff S1[x] ) ) & ( for x being Element of REAL st x in dom F holds F . x = H1(x) ) ) from SEQ_1:sch_3(); take F ; ::_thesis: ( dom F = (- h) ++ (dom f) & ( for x being Real st x in (- h) ++ (dom f) holds F . x = f . (x + h) ) ) for y being set st y in (- h) ++ (dom f) holds y in dom F by A1; then A2: (- h) ++ (dom f) c= dom F by TARSKI:def_3; for y being set st y in dom F holds y in (- h) ++ (dom f) by A1; then dom F c= (- h) ++ (dom f) by TARSKI:def_3; hence dom F = (- h) ++ (dom f) by A2, XBOOLE_0:def_10; ::_thesis: for x being Real st x in (- h) ++ (dom f) holds F . x = f . (x + h) now__::_thesis:_for_x_being_Real_st_x_in_(-_h)_++_(dom_f)_holds_ F_._x_=_f_._(x_+_h) let x be Real; ::_thesis: ( x in (- h) ++ (dom f) implies F . x = f . (x + h) ) assume x in (- h) ++ (dom f) ; ::_thesis: F . x = f . (x + h) then x in dom F by A1; hence F . x = f . (x + h) by A1; ::_thesis: verum end; hence for x being Real st x in (- h) ++ (dom f) holds F . x = f . (x + h) ; ::_thesis: verum end; uniqueness for b1, b2 being PartFunc of REAL,REAL st dom b1 = (- h) ++ (dom f) & ( for x being Real st x in (- h) ++ (dom f) holds b1 . x = f . (x + h) ) & dom b2 = (- h) ++ (dom f) & ( for x being Real st x in (- h) ++ (dom f) holds b2 . x = f . (x + h) ) holds b1 = b2 proof let f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( dom f1 = (- h) ++ (dom f) & ( for x being Real st x in (- h) ++ (dom f) holds f1 . x = f . (x + h) ) & dom f2 = (- h) ++ (dom f) & ( for x being Real st x in (- h) ++ (dom f) holds f2 . x = f . (x + h) ) implies f1 = f2 ) set X = (- h) ++ (dom f); assume that A3: dom f1 = (- h) ++ (dom f) and A4: for x being Real st x in (- h) ++ (dom f) holds f1 . x = f . (x + h) and A5: dom f2 = (- h) ++ (dom f) and A6: for x being Real st x in (- h) ++ (dom f) holds f2 . x = f . (x + h) ; ::_thesis: f1 = f2 for x being Element of REAL st x in dom f1 holds f1 . x = f2 . x proof let x be Element of REAL ; ::_thesis: ( x in dom f1 implies f1 . x = f2 . x ) assume A7: x in dom f1 ; ::_thesis: f1 . x = f2 . x then f1 . x = f . (x + h) by A3, A4; hence f1 . x = f2 . x by A3, A6, A7; ::_thesis: verum end; hence f1 = f2 by A3, A5, PARTFUN1:5; ::_thesis: verum end; end; :: deftheorem Def1 defines Shift DIFF_1:def_1_:_ for f being PartFunc of REAL,REAL for h being real number for b3 being PartFunc of REAL,REAL holds ( b3 = Shift (f,h) iff ( dom b3 = (- h) ++ (dom f) & ( for x being Real st x in (- h) ++ (dom f) holds b3 . x = f . (x + h) ) ) ); definition let f be Function of REAL,REAL; let h be real number ; :: original: Shift redefine func Shift (f,h) -> Function of REAL,REAL means :Def2: :: DIFF_1:def 2 for x being Real holds it . x = f . (x + h); coherence Shift (f,h) is Function of REAL,REAL proof ( dom (Shift (f,h)) = (- h) ++ (dom f) & dom f = REAL ) by Def1, FUNCT_2:def_1; then dom (Shift (f,h)) = REAL by MEASURE6:24; hence Shift (f,h) is Function of REAL,REAL by FUNCT_2:def_1; ::_thesis: verum end; compatibility for b1 being Function of REAL,REAL holds ( b1 = Shift (f,h) iff for x being Real holds b1 . x = f . (x + h) ) proof for IT being Function of REAL,REAL holds ( IT = Shift (f,h) iff for x being Real holds IT . x = f . (x + h) ) proof let IT be Function of REAL,REAL; ::_thesis: ( IT = Shift (f,h) iff for x being Real holds IT . x = f . (x + h) ) hereby ::_thesis: ( ( for x being Real holds IT . x = f . (x + h) ) implies IT = Shift (f,h) ) assume A1: IT = Shift (f,h) ; ::_thesis: for x being Real holds IT . x = f . (x + h) let x be Real; ::_thesis: IT . x = f . (x + h) dom (Shift (f,h)) = REAL by A1, FUNCT_2:def_1; then x in dom (Shift (f,h)) ; then x in (- h) ++ (dom f) by Def1; hence IT . x = f . (x + h) by A1, Def1; ::_thesis: verum end; ( dom (Shift (f,h)) = (- h) ++ (dom f) & dom f = REAL ) by Def1, FUNCT_2:def_1; then dom (Shift (f,h)) = REAL by MEASURE6:24; then A2: dom IT = dom (Shift (f,h)) by FUNCT_2:def_1; assume A3: for x being Real holds IT . x = f . (x + h) ; ::_thesis: IT = Shift (f,h) for x being Element of REAL st x in dom IT holds IT . x = (Shift (f,h)) . x proof let x be Element of REAL ; ::_thesis: ( x in dom IT implies IT . x = (Shift (f,h)) . x ) assume x in dom IT ; ::_thesis: IT . x = (Shift (f,h)) . x then A4: x in (- h) ++ (dom f) by A2, Def1; IT . x = f . (x + h) by A3; hence IT . x = (Shift (f,h)) . x by A4, Def1; ::_thesis: verum end; hence IT = Shift (f,h) by A2, PARTFUN1:5; ::_thesis: verum end; hence for b1 being Function of REAL,REAL holds ( b1 = Shift (f,h) iff for x being Real holds b1 . x = f . (x + h) ) ; ::_thesis: verum end; end; :: deftheorem Def2 defines Shift DIFF_1:def_2_:_ for f being Function of REAL,REAL for h being real number for b3 being Function of REAL,REAL holds ( b3 = Shift (f,h) iff for x being Real holds b3 . x = f . (x + h) ); definition let f be PartFunc of REAL,REAL; let h be real number ; func fD (f,h) -> PartFunc of REAL,REAL equals :: DIFF_1:def 3 (Shift (f,h)) - f; coherence (Shift (f,h)) - f is PartFunc of REAL,REAL ; end; :: deftheorem defines fD DIFF_1:def_3_:_ for f being PartFunc of REAL,REAL for h being real number holds fD (f,h) = (Shift (f,h)) - f; registration let f be Function of REAL,REAL; let h be real number ; cluster fD (f,h) -> quasi_total ; coherence fD (f,h) is quasi_total proof dom (fD (f,h)) = (dom (Shift (f,h))) /\ (dom f) by VALUED_1:12 .= REAL /\ (dom f) by FUNCT_2:def_1 .= REAL /\ REAL by FUNCT_2:def_1 .= REAL ; hence fD (f,h) is quasi_total by FUNCT_2:def_1; ::_thesis: verum end; end; definition let f be PartFunc of REAL,REAL; let h be real number ; func bD (f,h) -> PartFunc of REAL,REAL equals :: DIFF_1:def 4 f - (Shift (f,(- h))); coherence f - (Shift (f,(- h))) is PartFunc of REAL,REAL ; end; :: deftheorem defines bD DIFF_1:def_4_:_ for f being PartFunc of REAL,REAL for h being real number holds bD (f,h) = f - (Shift (f,(- h))); registration let f be Function of REAL,REAL; let h be real number ; cluster bD (f,h) -> quasi_total ; coherence bD (f,h) is quasi_total proof dom (bD (f,h)) = (dom (Shift (f,(- h)))) /\ (dom f) by VALUED_1:12 .= REAL /\ (dom f) by FUNCT_2:def_1 .= REAL /\ REAL by FUNCT_2:def_1 .= REAL ; hence bD (f,h) is quasi_total by FUNCT_2:def_1; ::_thesis: verum end; end; definition let f be PartFunc of REAL,REAL; let h be real number ; func cD (f,h) -> PartFunc of REAL,REAL equals :: DIFF_1:def 5 (Shift (f,(h / 2))) - (Shift (f,(- (h / 2)))); coherence (Shift (f,(h / 2))) - (Shift (f,(- (h / 2)))) is PartFunc of REAL,REAL ; end; :: deftheorem defines cD DIFF_1:def_5_:_ for f being PartFunc of REAL,REAL for h being real number holds cD (f,h) = (Shift (f,(h / 2))) - (Shift (f,(- (h / 2)))); registration let f be Function of REAL,REAL; let h be real number ; cluster cD (f,h) -> quasi_total ; coherence cD (f,h) is quasi_total proof dom (cD (f,h)) = (dom (Shift (f,(h / 2)))) /\ (dom (Shift (f,(- (h / 2))))) by VALUED_1:12 .= REAL /\ (dom (Shift (f,(- (h / 2))))) by FUNCT_2:def_1 .= REAL /\ REAL by FUNCT_2:def_1 .= REAL ; hence cD (f,h) is quasi_total by FUNCT_2:def_1; ::_thesis: verum end; end; definition let f be PartFunc of REAL,REAL; let h be real number ; func forward_difference (f,h) -> Functional_Sequence of REAL,REAL means :Def6: :: DIFF_1:def 6 ( it . 0 = f & ( for n being Nat holds it . (n + 1) = fD ((it . n),h) ) ); existence ex b1 being Functional_Sequence of REAL,REAL st ( b1 . 0 = f & ( for n being Nat holds b1 . (n + 1) = fD ((b1 . n),h) ) ) proof reconsider fZ = f as Element of PFuncs (REAL,REAL) by PARTFUN1:45; defpred S1[ set , set , set ] means ex g being PartFunc of REAL,REAL st ( \$2 = g & \$3 = fD (g,h) ); A1: for n being Element of NAT for x being Element of PFuncs (REAL,REAL) ex y being Element of PFuncs (REAL,REAL) st S1[n,x,y] proof let n be Element of NAT ; ::_thesis: for x being Element of PFuncs (REAL,REAL) ex y being Element of PFuncs (REAL,REAL) st S1[n,x,y] let x be Element of PFuncs (REAL,REAL); ::_thesis: ex y being Element of PFuncs (REAL,REAL) st S1[n,x,y] reconsider x9 = x as PartFunc of REAL,REAL by PARTFUN1:46; reconsider y = fD (x9,h) as Element of PFuncs (REAL,REAL) by PARTFUN1:45; ex w being PartFunc of REAL,REAL st ( x = w & y = fD (w,h) ) ; hence ex y being Element of PFuncs (REAL,REAL) st S1[n,x,y] ; ::_thesis: verum end; consider g being Function of NAT,(PFuncs (REAL,REAL)) such that A2: ( g . 0 = fZ & ( for n being Element of NAT holds S1[n,g . n,g . (n + 1)] ) ) from RECDEF_1:sch_2(A1); reconsider g = g as Functional_Sequence of REAL,REAL ; take g ; ::_thesis: ( g . 0 = f & ( for n being Nat holds g . (n + 1) = fD ((g . n),h) ) ) thus g . 0 = f by A2; ::_thesis: for n being Nat holds g . (n + 1) = fD ((g . n),h) let i be Nat; ::_thesis: g . (i + 1) = fD ((g . i),h) i in NAT by ORDINAL1:def_12; then S1[i,g . i,g . (i + 1)] by A2; hence g . (i + 1) = fD ((g . i),h) ; ::_thesis: verum end; uniqueness for b1, b2 being Functional_Sequence of REAL,REAL st b1 . 0 = f & ( for n being Nat holds b1 . (n + 1) = fD ((b1 . n),h) ) & b2 . 0 = f & ( for n being Nat holds b2 . (n + 1) = fD ((b2 . n),h) ) holds b1 = b2 proof let seq1, seq2 be Functional_Sequence of REAL,REAL; ::_thesis: ( seq1 . 0 = f & ( for n being Nat holds seq1 . (n + 1) = fD ((seq1 . n),h) ) & seq2 . 0 = f & ( for n being Nat holds seq2 . (n + 1) = fD ((seq2 . n),h) ) implies seq1 = seq2 ) assume that A3: seq1 . 0 = f and A4: for n being Nat holds seq1 . (n + 1) = fD ((seq1 . n),h) and A5: seq2 . 0 = f and A6: for n being Nat holds seq2 . (n + 1) = fD ((seq2 . n),h) ; ::_thesis: seq1 = seq2 defpred S1[ Nat] means seq1 . \$1 = seq2 . \$1; A7: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A8: S1[k] ; ::_thesis: S1[k + 1] thus seq1 . (k + 1) = fD ((seq1 . k),h) by A4 .= seq2 . (k + 1) by A6, A8 ; ::_thesis: verum end; A9: S1[ 0 ] by A3, A5; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A9, A7); hence seq1 = seq2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def6 defines forward_difference DIFF_1:def_6_:_ for f being PartFunc of REAL,REAL for h being real number for b3 being Functional_Sequence of REAL,REAL holds ( b3 = forward_difference (f,h) iff ( b3 . 0 = f & ( for n being Nat holds b3 . (n + 1) = fD ((b3 . n),h) ) ) ); notation let f be PartFunc of REAL,REAL; let h be real number ; synonym fdif (f,h) for forward_difference (f,h); end; theorem :: DIFF_1:1 for x, h being Real for f being PartFunc of REAL,REAL st x in dom f & x + h in dom f holds (fD (f,h)) . x = (f . (x + h)) - (f . x) proof let x, h be Real; ::_thesis: for f being PartFunc of REAL,REAL st x in dom f & x + h in dom f holds (fD (f,h)) . x = (f . (x + h)) - (f . x) let f be PartFunc of REAL,REAL; ::_thesis: ( x in dom f & x + h in dom f implies (fD (f,h)) . x = (f . (x + h)) - (f . x) ) assume A1: ( x in dom f & x + h in dom f ) ; ::_thesis: (fD (f,h)) . x = (f . (x + h)) - (f . x) A2: dom (Shift (f,h)) = (- h) ++ (dom f) by Def1; A3: (- h) + (x + h) in (- h) ++ (dom f) by A1, MEASURE6:46; then A4: (Shift (f,h)) . x = f . (x + h) by Def1; x in (dom (Shift (f,h))) /\ (dom f) by A3, A2, A1, XBOOLE_0:def_4; then x in dom (fD (f,h)) by VALUED_1:12; hence (fD (f,h)) . x = (f . (x + h)) - (f . x) by A4, VALUED_1:13; ::_thesis: verum end; theorem Th2: :: DIFF_1:2 for h being Real for f being Function of REAL,REAL for n being Nat holds (fdif (f,h)) . n is Function of REAL,REAL proof let h be Real; ::_thesis: for f being Function of REAL,REAL for n being Nat holds (fdif (f,h)) . n is Function of REAL,REAL let f be Function of REAL,REAL; ::_thesis: for n being Nat holds (fdif (f,h)) . n is Function of REAL,REAL defpred S1[ Nat] means (fdif (f,h)) . \$1 is Function of REAL,REAL; A1: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume (fdif (f,h)) . k is Function of REAL,REAL ; ::_thesis: S1[k + 1] then fD (((fdif (f,h)) . k),h) is Function of REAL,REAL ; hence S1[k + 1] by Def6; ::_thesis: verum end; A2: S1[ 0 ] by Def6; for n being Nat holds S1[n] from NAT_1:sch_2(A2, A1); hence for n being Nat holds (fdif (f,h)) . n is Function of REAL,REAL ; ::_thesis: verum end; theorem Th3: :: DIFF_1:3 for h, x being Real for f being Function of REAL,REAL holds (fD (f,h)) . x = (f . (x + h)) - (f . x) proof let h, x be Real; ::_thesis: for f being Function of REAL,REAL holds (fD (f,h)) . x = (f . (x + h)) - (f . x) let f be Function of REAL,REAL; ::_thesis: (fD (f,h)) . x = (f . (x + h)) - (f . x) dom ((Shift (f,h)) - f) = REAL by FUNCT_2:def_1; hence (fD (f,h)) . x = ((Shift (f,h)) . x) - (f . x) by VALUED_1:13 .= (f . (x + h)) - (f . x) by Def2 ; ::_thesis: verum end; theorem Th4: :: DIFF_1:4 for h, x being Real for f being Function of REAL,REAL holds (bD (f,h)) . x = (f . x) - (f . (x - h)) proof let h, x be Real; ::_thesis: for f being Function of REAL,REAL holds (bD (f,h)) . x = (f . x) - (f . (x - h)) let f be Function of REAL,REAL; ::_thesis: (bD (f,h)) . x = (f . x) - (f . (x - h)) thus (bD (f,h)) . x = (- (fD (f,(- h)))) . x by RFUNCT_1:19 .= - ((fD (f,(- h))) . x) by VALUED_1:8 .= - ((f . (x + (- h))) - (f . x)) by Th3 .= (f . x) - (f . (x - h)) ; ::_thesis: verum end; theorem Th5: :: DIFF_1:5 for h, x being Real for f being Function of REAL,REAL holds (cD (f,h)) . x = (f . (x + (h / 2))) - (f . (x - (h / 2))) proof let h, x be Real; ::_thesis: for f being Function of REAL,REAL holds (cD (f,h)) . x = (f . (x + (h / 2))) - (f . (x - (h / 2))) let f be Function of REAL,REAL; ::_thesis: (cD (f,h)) . x = (f . (x + (h / 2))) - (f . (x - (h / 2))) dom ((Shift (f,(h / 2))) - (Shift (f,(- (h / 2))))) = REAL by FUNCT_2:def_1; hence (cD (f,h)) . x = ((Shift (f,(h / 2))) . x) - ((Shift (f,(- (h / 2)))) . x) by VALUED_1:13 .= (f . (x + (h / 2))) - ((Shift (f,(- (h / 2)))) . x) by Def2 .= (f . (x + (h / 2))) - (f . (x + (- (h / 2)))) by Def2 .= (f . (x + (h / 2))) - (f . (x - (h / 2))) ; ::_thesis: verum end; theorem :: DIFF_1:6 for n being Element of NAT for h being Real for f being Function of REAL,REAL st f is constant holds for x being Real holds ((fdif (f,h)) . (n + 1)) . x = 0 proof let n be Element of NAT ; ::_thesis: for h being Real for f being Function of REAL,REAL st f is constant holds for x being Real holds ((fdif (f,h)) . (n + 1)) . x = 0 let h be Real; ::_thesis: for f being Function of REAL,REAL st f is constant holds for x being Real holds ((fdif (f,h)) . (n + 1)) . x = 0 let f be Function of REAL,REAL; ::_thesis: ( f is constant implies for x being Real holds ((fdif (f,h)) . (n + 1)) . x = 0 ) assume A1: f is constant ; ::_thesis: for x being Real holds ((fdif (f,h)) . (n + 1)) . x = 0 A2: for x being Real holds (f . (x + h)) - (f . x) = 0 proof let x be Real; ::_thesis: (f . (x + h)) - (f . x) = 0 x + h in REAL ; then A3: x + h in dom f by FUNCT_2:def_1; x in REAL ; then x in dom f by FUNCT_2:def_1; then f . x = f . (x + h) by A1, A3, FUNCT_1:def_10; hence (f . (x + h)) - (f . x) = 0 ; ::_thesis: verum end; for x being Real holds ((fdif (f,h)) . (n + 1)) . x = 0 proof defpred S1[ Element of NAT ] means for x being Real holds ((fdif (f,h)) . (\$1 + 1)) . x = 0 ; A4: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A5: for x being Real holds ((fdif (f,h)) . (k + 1)) . x = 0 ; ::_thesis: S1[k + 1] let x be Real; ::_thesis: ((fdif (f,h)) . ((k + 1) + 1)) . x = 0 A6: ((fdif (f,h)) . (k + 1)) . (x + h) = 0 by A5; A7: (fdif (f,h)) . (k + 1) is Function of REAL,REAL by Th2; ((fdif (f,h)) . (k + 2)) . x = ((fdif (f,h)) . ((k + 1) + 1)) . x .= (fD (((fdif (f,h)) . (k + 1)),h)) . x by Def6 .= (((fdif (f,h)) . (k + 1)) . (x + h)) - (((fdif (f,h)) . (k + 1)) . x) by A7, Th3 .= 0 - 0 by A5, A6 .= 0 ; hence ((fdif (f,h)) . ((k + 1) + 1)) . x = 0 ; ::_thesis: verum end; A8: S1[ 0 ] proof let x be Real; ::_thesis: ((fdif (f,h)) . (0 + 1)) . x = 0 thus ((fdif (f,h)) . (0 + 1)) . x = (fD (((fdif (f,h)) . 0),h)) . x by Def6 .= (fD (f,h)) . x by Def6 .= (f . (x + h)) - (f . x) by Th3 .= 0 by A2 ; ::_thesis: verum end; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A8, A4); hence for x being Real holds ((fdif (f,h)) . (n + 1)) . x = 0 ; ::_thesis: verum end; hence for x being Real holds ((fdif (f,h)) . (n + 1)) . x = 0 ; ::_thesis: verum end; theorem Th7: :: DIFF_1:7 for n being Element of NAT for r, h, x being Real for f being Function of REAL,REAL holds ((fdif ((r (#) f),h)) . (n + 1)) . x = r * (((fdif (f,h)) . (n + 1)) . x) proof let n be Element of NAT ; ::_thesis: for r, h, x being Real for f being Function of REAL,REAL holds ((fdif ((r (#) f),h)) . (n + 1)) . x = r * (((fdif (f,h)) . (n + 1)) . x) let r, h, x be Real; ::_thesis: for f being Function of REAL,REAL holds ((fdif ((r (#) f),h)) . (n + 1)) . x = r * (((fdif (f,h)) . (n + 1)) . x) let f be Function of REAL,REAL; ::_thesis: ((fdif ((r (#) f),h)) . (n + 1)) . x = r * (((fdif (f,h)) . (n + 1)) . x) defpred S1[ Element of NAT ] means for x being Real holds ((fdif ((r (#) f),h)) . (\$1 + 1)) . x = r * (((fdif (f,h)) . (\$1 + 1)) . x); A1: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A2: for x being Real holds ((fdif ((r (#) f),h)) . (k + 1)) . x = r * (((fdif (f,h)) . (k + 1)) . x) ; ::_thesis: S1[k + 1] let x be Real; ::_thesis: ((fdif ((r (#) f),h)) . ((k + 1) + 1)) . x = r * (((fdif (f,h)) . ((k + 1) + 1)) . x) A3: ( ((fdif ((r (#) f),h)) . (k + 1)) . x = r * (((fdif (f,h)) . (k + 1)) . x) & ((fdif ((r (#) f),h)) . (k + 1)) . (x + h) = r * (((fdif (f,h)) . (k + 1)) . (x + h)) ) by A2; A4: (fdif ((r (#) f),h)) . (k + 1) is Function of REAL,REAL by Th2; A5: (fdif (f,h)) . (k + 1) is Function of REAL,REAL by Th2; ((fdif ((r (#) f),h)) . ((k + 1) + 1)) . x = (fD (((fdif ((r (#) f),h)) . (k + 1)),h)) . x by Def6 .= (r * (((fdif (f,h)) . (k + 1)) . (x + h))) - (r * (((fdif (f,h)) . (k + 1)) . x)) by A3, A4, Th3 .= r * ((((fdif (f,h)) . (k + 1)) . (x + h)) - (((fdif (f,h)) . (k + 1)) . x)) .= r * ((fD (((fdif (f,h)) . (k + 1)),h)) . x) by A5, Th3 .= r * (((fdif (f,h)) . ((k + 1) + 1)) . x) by Def6 ; hence ((fdif ((r (#) f),h)) . ((k + 1) + 1)) . x = r * (((fdif (f,h)) . ((k + 1) + 1)) . x) ; ::_thesis: verum end; A6: S1[ 0 ] proof let x be Real; ::_thesis: ((fdif ((r (#) f),h)) . (0 + 1)) . x = r * (((fdif (f,h)) . (0 + 1)) . x) x in REAL ; then A7: x in dom (r (#) f) by FUNCT_2:def_1; x + h in REAL ; then A8: x + h in dom (r (#) f) by FUNCT_2:def_1; ((fdif ((r (#) f),h)) . (0 + 1)) . x = (fD (((fdif ((r (#) f),h)) . 0),h)) . x by Def6 .= (fD ((r (#) f),h)) . x by Def6 .= ((r (#) f) . (x + h)) - ((r (#) f) . x) by Th3 .= (r * (f . (x + h))) - ((r (#) f) . x) by A8, VALUED_1:def_5 .= (r * (f . (x + h))) - (r * (f . x)) by A7, VALUED_1:def_5 .= r * ((f . (x + h)) - (f . x)) .= r * ((fD (f,h)) . x) by Th3 .= r * ((fD (((fdif (f,h)) . 0),h)) . x) by Def6 .= r * (((fdif (f,h)) . (0 + 1)) . x) by Def6 ; hence ((fdif ((r (#) f),h)) . (0 + 1)) . x = r * (((fdif (f,h)) . (0 + 1)) . x) ; ::_thesis: verum end; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A6, A1); hence ((fdif ((r (#) f),h)) . (n + 1)) . x = r * (((fdif (f,h)) . (n + 1)) . x) ; ::_thesis: verum end; theorem Th8: :: DIFF_1:8 for n being Element of NAT for h, x being Real for f1, f2 being Function of REAL,REAL holds ((fdif ((f1 + f2),h)) . (n + 1)) . x = (((fdif (f1,h)) . (n + 1)) . x) + (((fdif (f2,h)) . (n + 1)) . x) proof let n be Element of NAT ; ::_thesis: for h, x being Real for f1, f2 being Function of REAL,REAL holds ((fdif ((f1 + f2),h)) . (n + 1)) . x = (((fdif (f1,h)) . (n + 1)) . x) + (((fdif (f2,h)) . (n + 1)) . x) let h, x be Real; ::_thesis: for f1, f2 being Function of REAL,REAL holds ((fdif ((f1 + f2),h)) . (n + 1)) . x = (((fdif (f1,h)) . (n + 1)) . x) + (((fdif (f2,h)) . (n + 1)) . x) let f1, f2 be Function of REAL,REAL; ::_thesis: ((fdif ((f1 + f2),h)) . (n + 1)) . x = (((fdif (f1,h)) . (n + 1)) . x) + (((fdif (f2,h)) . (n + 1)) . x) defpred S1[ Element of NAT ] means for x being Real holds ((fdif ((f1 + f2),h)) . (\$1 + 1)) . x = (((fdif (f1,h)) . (\$1 + 1)) . x) + (((fdif (f2,h)) . (\$1 + 1)) . x); A1: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A2: for x being Real holds ((fdif ((f1 + f2),h)) . (k + 1)) . x = (((fdif (f1,h)) . (k + 1)) . x) + (((fdif (f2,h)) . (k + 1)) . x) ; ::_thesis: S1[k + 1] let x be Real; ::_thesis: ((fdif ((f1 + f2),h)) . ((k + 1) + 1)) . x = (((fdif (f1,h)) . ((k + 1) + 1)) . x) + (((fdif (f2,h)) . ((k + 1) + 1)) . x) A3: ( ((fdif ((f1 + f2),h)) . (k + 1)) . x = (((fdif (f1,h)) . (k + 1)) . x) + (((fdif (f2,h)) . (k + 1)) . x) & ((fdif ((f1 + f2),h)) . (k + 1)) . (x + h) = (((fdif (f1,h)) . (k + 1)) . (x + h)) + (((fdif (f2,h)) . (k + 1)) . (x + h)) ) by A2; A4: (fdif ((f1 + f2),h)) . (k + 1) is Function of REAL,REAL by Th2; A5: (fdif (f2,h)) . (k + 1) is Function of REAL,REAL by Th2; A6: (fdif (f1,h)) . (k + 1) is Function of REAL,REAL by Th2; ((fdif ((f1 + f2),h)) . ((k + 1) + 1)) . x = (fD (((fdif ((f1 + f2),h)) . (k + 1)),h)) . x by Def6 .= (((fdif ((f1 + f2),h)) . (k + 1)) . (x + h)) - (((fdif ((f1 + f2),h)) . (k + 1)) . x) by A4, Th3 .= ((((fdif (f1,h)) . (k + 1)) . (x + h)) - (((fdif (f1,h)) . (k + 1)) . x)) + ((((fdif (f2,h)) . (k + 1)) . (x + h)) - (((fdif (f2,h)) . (k + 1)) . x)) by A3 .= ((fD (((fdif (f1,h)) . (k + 1)),h)) . x) + ((((fdif (f2,h)) . (k + 1)) . (x + h)) - (((fdif (f2,h)) . (k + 1)) . x)) by A6, Th3 .= ((fD (((fdif (f1,h)) . (k + 1)),h)) . x) + ((fD (((fdif (f2,h)) . (k + 1)),h)) . x) by A5, Th3 .= (((fdif (f1,h)) . ((k + 1) + 1)) . x) + ((fD (((fdif (f2,h)) . (k + 1)),h)) . x) by Def6 .= (((fdif (f1,h)) . ((k + 1) + 1)) . x) + (((fdif (f2,h)) . ((k + 1) + 1)) . x) by Def6 ; hence ((fdif ((f1 + f2),h)) . ((k + 1) + 1)) . x = (((fdif (f1,h)) . ((k + 1) + 1)) . x) + (((fdif (f2,h)) . ((k + 1) + 1)) . x) ; ::_thesis: verum end; A7: S1[ 0 ] proof let x be Real; ::_thesis: ((fdif ((f1 + f2),h)) . (0 + 1)) . x = (((fdif (f1,h)) . (0 + 1)) . x) + (((fdif (f2,h)) . (0 + 1)) . x) ((fdif ((f1 + f2),h)) . (0 + 1)) . x = (fD (((fdif ((f1 + f2),h)) . 0),h)) . x by Def6 .= (fD ((f1 + f2),h)) . x by Def6 .= ((f1 + f2) . (x + h)) - ((f1 + f2) . x) by Th3 .= ((f1 . (x + h)) + (f2 . (x + h))) - ((f1 + f2) . x) by VALUED_1:1 .= ((f1 . (x + h)) + (f2 . (x + h))) - ((f1 . x) + (f2 . x)) by VALUED_1:1 .= ((f1 . (x + h)) - (f1 . x)) + ((f2 . (x + h)) - (f2 . x)) .= ((fD (f1,h)) . x) + ((f2 . (x + h)) - (f2 . x)) by Th3 .= ((fD (f1,h)) . x) + ((fD (f2,h)) . x) by Th3 .= ((fD (((fdif (f1,h)) . 0),h)) . x) + ((fD (f2,h)) . x) by Def6 .= ((fD (((fdif (f1,h)) . 0),h)) . x) + ((fD (((fdif (f2,h)) . 0),h)) . x) by Def6 .= (((fdif (f1,h)) . (0 + 1)) . x) + ((fD (((fdif (f2,h)) . 0),h)) . x) by Def6 .= (((fdif (f1,h)) . (0 + 1)) . x) + (((fdif (f2,h)) . (0 + 1)) . x) by Def6 ; hence ((fdif ((f1 + f2),h)) . (0 + 1)) . x = (((fdif (f1,h)) . (0 + 1)) . x) + (((fdif (f2,h)) . (0 + 1)) . x) ; ::_thesis: verum end; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A7, A1); hence ((fdif ((f1 + f2),h)) . (n + 1)) . x = (((fdif (f1,h)) . (n + 1)) . x) + (((fdif (f2,h)) . (n + 1)) . x) ; ::_thesis: verum end; theorem :: DIFF_1:9 for n being Element of NAT for h, x being Real for f1, f2 being Function of REAL,REAL holds ((fdif ((f1 - f2),h)) . (n + 1)) . x = (((fdif (f1,h)) . (n + 1)) . x) - (((fdif (f2,h)) . (n + 1)) . x) proof let n be Element of NAT ; ::_thesis: for h, x being Real for f1, f2 being Function of REAL,REAL holds ((fdif ((f1 - f2),h)) . (n + 1)) . x = (((fdif (f1,h)) . (n + 1)) . x) - (((fdif (f2,h)) . (n + 1)) . x) let h, x be Real; ::_thesis: for f1, f2 being Function of REAL,REAL holds ((fdif ((f1 - f2),h)) . (n + 1)) . x = (((fdif (f1,h)) . (n + 1)) . x) - (((fdif (f2,h)) . (n + 1)) . x) let f1, f2 be Function of REAL,REAL; ::_thesis: ((fdif ((f1 - f2),h)) . (n + 1)) . x = (((fdif (f1,h)) . (n + 1)) . x) - (((fdif (f2,h)) . (n + 1)) . x) defpred S1[ Element of NAT ] means for x being Real holds ((fdif ((f1 - f2),h)) . (\$1 + 1)) . x = (((fdif (f1,h)) . (\$1 + 1)) . x) - (((fdif (f2,h)) . (\$1 + 1)) . x); A1: S1[ 0 ] proof let x be Real; ::_thesis: ((fdif ((f1 - f2),h)) . (0 + 1)) . x = (((fdif (f1,h)) . (0 + 1)) . x) - (((fdif (f2,h)) . (0 + 1)) . x) x in REAL ; then ( x in dom f1 & x in dom f2 ) by FUNCT_2:def_1; then x in (dom f1) /\ (dom f2) by XBOOLE_0:def_4; then A2: x in dom (f1 - f2) by VALUED_1:12; x + h in REAL ; then ( x + h in dom f1 & x + h in dom f2 ) by FUNCT_2:def_1; then x + h in (dom f1) /\ (dom f2) by XBOOLE_0:def_4; then A3: x + h in dom (f1 - f2) by VALUED_1:12; ((fdif ((f1 - f2),h)) . (0 + 1)) . x = (fD (((fdif ((f1 - f2),h)) . 0),h)) . x by Def6 .= (fD ((f1 - f2),h)) . x by Def6 .= ((f1 - f2) . (x + h)) - ((f1 - f2) . x) by Th3 .= ((f1 . (x + h)) - (f2 . (x + h))) - ((f1 - f2) . x) by A3, VALUED_1:13 .= ((f1 . (x + h)) - (f2 . (x + h))) - ((f1 . x) - (f2 . x)) by A2, VALUED_1:13 .= ((f1 . (x + h)) - (f1 . x)) - ((f2 . (x + h)) - (f2 . x)) .= ((fD (f1,h)) . x) - ((f2 . (x + h)) - (f2 . x)) by Th3 .= ((fD (f1,h)) . x) - ((fD (f2,h)) . x) by Th3 .= ((fD (((fdif (f1,h)) . 0),h)) . x) - ((fD (f2,h)) . x) by Def6 .= ((fD (((fdif (f1,h)) . 0),h)) . x) - ((fD (((fdif (f2,h)) . 0),h)) . x) by Def6 .= (((fdif (f1,h)) . (0 + 1)) . x) - ((fD (((fdif (f2,h)) . 0),h)) . x) by Def6 .= (((fdif (f1,h)) . (0 + 1)) . x) - (((fdif (f2,h)) . (0 + 1)) . x) by Def6 ; hence ((fdif ((f1 - f2),h)) . (0 + 1)) . x = (((fdif (f1,h)) . (0 + 1)) . x) - (((fdif (f2,h)) . (0 + 1)) . x) ; ::_thesis: verum end; A4: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A5: for x being Real holds ((fdif ((f1 - f2),h)) . (k + 1)) . x = (((fdif (f1,h)) . (k + 1)) . x) - (((fdif (f2,h)) . (k + 1)) . x) ; ::_thesis: S1[k + 1] let x be Real; ::_thesis: ((fdif ((f1 - f2),h)) . ((k + 1) + 1)) . x = (((fdif (f1,h)) . ((k + 1) + 1)) . x) - (((fdif (f2,h)) . ((k + 1) + 1)) . x) A6: ( ((fdif ((f1 - f2),h)) . (k + 1)) . x = (((fdif (f1,h)) . (k + 1)) . x) - (((fdif (f2,h)) . (k + 1)) . x) & ((fdif ((f1 - f2),h)) . (k + 1)) . (x + h) = (((fdif (f1,h)) . (k + 1)) . (x + h)) - (((fdif (f2,h)) . (k + 1)) . (x + h)) ) by A5; A7: (fdif ((f1 - f2),h)) . (k + 1) is Function of REAL,REAL by Th2; A8: (fdif (f2,h)) . (k + 1) is Function of REAL,REAL by Th2; A9: (fdif (f1,h)) . (k + 1) is Function of REAL,REAL by Th2; ((fdif ((f1 - f2),h)) . ((k + 1) + 1)) . x = (fD (((fdif ((f1 - f2),h)) . (k + 1)),h)) . x by Def6 .= (((fdif ((f1 - f2),h)) . (k + 1)) . (x + h)) - (((fdif ((f1 - f2),h)) . (k + 1)) . x) by A7, Th3 .= ((((fdif (f1,h)) . (k + 1)) . (x + h)) - (((fdif (f1,h)) . (k + 1)) . x)) - ((((fdif (f2,h)) . (k + 1)) . (x + h)) - (((fdif (f2,h)) . (k + 1)) . x)) by A6 .= ((fD (((fdif (f1,h)) . (k + 1)),h)) . x) - ((((fdif (f2,h)) . (k + 1)) . (x + h)) - (((fdif (f2,h)) . (k + 1)) . x)) by A9, Th3 .= ((fD (((fdif (f1,h)) . (k + 1)),h)) . x) - ((fD (((fdif (f2,h)) . (k + 1)),h)) . x) by A8, Th3 .= (((fdif (f1,h)) . ((k + 1) + 1)) . x) - ((fD (((fdif (f2,h)) . (k + 1)),h)) . x) by Def6 .= (((fdif (f1,h)) . ((k + 1) + 1)) . x) - (((fdif (f2,h)) . ((k + 1) + 1)) . x) by Def6 ; hence ((fdif ((f1 - f2),h)) . ((k + 1) + 1)) . x = (((fdif (f1,h)) . ((k + 1) + 1)) . x) - (((fdif (f2,h)) . ((k + 1) + 1)) . x) ; ::_thesis: verum end; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A1, A4); hence ((fdif ((f1 - f2),h)) . (n + 1)) . x = (((fdif (f1,h)) . (n + 1)) . x) - (((fdif (f2,h)) . (n + 1)) . x) ; ::_thesis: verum end; theorem :: DIFF_1:10 for n being Element of NAT for r1, r2, h, x being Real for f1, f2 being Function of REAL,REAL holds ((fdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) . x = (r1 * (((fdif (f1,h)) . (n + 1)) . x)) + (r2 * (((fdif (f2,h)) . (n + 1)) . x)) proof let n be Element of NAT ; ::_thesis: for r1, r2, h, x being Real for f1, f2 being Function of REAL,REAL holds ((fdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) . x = (r1 * (((fdif (f1,h)) . (n + 1)) . x)) + (r2 * (((fdif (f2,h)) . (n + 1)) . x)) let r1, r2, h, x be Real; ::_thesis: for f1, f2 being Function of REAL,REAL holds ((fdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) . x = (r1 * (((fdif (f1,h)) . (n + 1)) . x)) + (r2 * (((fdif (f2,h)) . (n + 1)) . x)) let f1, f2 be Function of REAL,REAL; ::_thesis: ((fdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) . x = (r1 * (((fdif (f1,h)) . (n + 1)) . x)) + (r2 * (((fdif (f2,h)) . (n + 1)) . x)) set g1 = r1 (#) f1; set g2 = r2 (#) f2; ((fdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) . x = (((fdif ((r1 (#) f1),h)) . (n + 1)) . x) + (((fdif ((r2 (#) f2),h)) . (n + 1)) . x) by Th8 .= (r1 * (((fdif (f1,h)) . (n + 1)) . x)) + (((fdif ((r2 (#) f2),h)) . (n + 1)) . x) by Th7 .= (r1 * (((fdif (f1,h)) . (n + 1)) . x)) + (r2 * (((fdif (f2,h)) . (n + 1)) . x)) by Th7 ; hence ((fdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) . x = (r1 * (((fdif (f1,h)) . (n + 1)) . x)) + (r2 * (((fdif (f2,h)) . (n + 1)) . x)) ; ::_thesis: verum end; theorem :: DIFF_1:11 for h, x being Real for f being Function of REAL,REAL holds ((fdif (f,h)) . 1) . x = ((Shift (f,h)) . x) - (f . x) proof let h, x be Real; ::_thesis: for f being Function of REAL,REAL holds ((fdif (f,h)) . 1) . x = ((Shift (f,h)) . x) - (f . x) let f be Function of REAL,REAL; ::_thesis: ((fdif (f,h)) . 1) . x = ((Shift (f,h)) . x) - (f . x) set f1 = Shift (f,h); ((fdif (f,h)) . 1) . x = ((fdif (f,h)) . (0 + 1)) . x .= (fD (((fdif (f,h)) . 0),h)) . x by Def6 .= (fD (f,h)) . x by Def6 .= (f . (x + h)) - (f . x) by Th3 .= ((Shift (f,h)) . x) - (f . x) by Def2 ; hence ((fdif (f,h)) . 1) . x = ((Shift (f,h)) . x) - (f . x) ; ::_thesis: verum end; definition let f be PartFunc of REAL,REAL; let h be real number ; func backward_difference (f,h) -> Functional_Sequence of REAL,REAL means :Def7: :: DIFF_1:def 7 ( it . 0 = f & ( for n being Nat holds it . (n + 1) = bD ((it . n),h) ) ); existence ex b1 being Functional_Sequence of REAL,REAL st ( b1 . 0 = f & ( for n being Nat holds b1 . (n + 1) = bD ((b1 . n),h) ) ) proof reconsider fZ = f as Element of PFuncs (REAL,REAL) by PARTFUN1:45; defpred S1[ set , set , set ] means ex g being PartFunc of REAL,REAL st ( \$2 = g & \$3 = bD (g,h) ); A1: for n being Element of NAT for x being Element of PFuncs (REAL,REAL) ex y being Element of PFuncs (REAL,REAL) st S1[n,x,y] proof let n be Element of NAT ; ::_thesis: for x being Element of PFuncs (REAL,REAL) ex y being Element of PFuncs (REAL,REAL) st S1[n,x,y] let x be Element of PFuncs (REAL,REAL); ::_thesis: ex y being Element of PFuncs (REAL,REAL) st S1[n,x,y] reconsider x9 = x as PartFunc of REAL,REAL by PARTFUN1:46; reconsider y = bD (x9,h) as Element of PFuncs (REAL,REAL) by PARTFUN1:45; ex w being PartFunc of REAL,REAL st ( x = w & y = bD (w,h) ) ; hence ex y being Element of PFuncs (REAL,REAL) st S1[n,x,y] ; ::_thesis: verum end; consider g being Function of NAT,(PFuncs (REAL,REAL)) such that A2: ( g . 0 = fZ & ( for n being Element of NAT holds S1[n,g . n,g . (n + 1)] ) ) from RECDEF_1:sch_2(A1); reconsider g = g as Functional_Sequence of REAL,REAL ; take g ; ::_thesis: ( g . 0 = f & ( for n being Nat holds g . (n + 1) = bD ((g . n),h) ) ) thus g . 0 = f by A2; ::_thesis: for n being Nat holds g . (n + 1) = bD ((g . n),h) let i be Nat; ::_thesis: g . (i + 1) = bD ((g . i),h) i in NAT by ORDINAL1:def_12; then S1[i,g . i,g . (i + 1)] by A2; hence g . (i + 1) = bD ((g . i),h) ; ::_thesis: verum end; uniqueness for b1, b2 being Functional_Sequence of REAL,REAL st b1 . 0 = f & ( for n being Nat holds b1 . (n + 1) = bD ((b1 . n),h) ) & b2 . 0 = f & ( for n being Nat holds b2 . (n + 1) = bD ((b2 . n),h) ) holds b1 = b2 proof let seq1, seq2 be Functional_Sequence of REAL,REAL; ::_thesis: ( seq1 . 0 = f & ( for n being Nat holds seq1 . (n + 1) = bD ((seq1 . n),h) ) & seq2 . 0 = f & ( for n being Nat holds seq2 . (n + 1) = bD ((seq2 . n),h) ) implies seq1 = seq2 ) assume that A3: seq1 . 0 = f and A4: for n being Nat holds seq1 . (n + 1) = bD ((seq1 . n),h) and A5: seq2 . 0 = f and A6: for n being Nat holds seq2 . (n + 1) = bD ((seq2 . n),h) ; ::_thesis: seq1 = seq2 defpred S1[ Nat] means seq1 . \$1 = seq2 . \$1; A7: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A8: S1[k] ; ::_thesis: S1[k + 1] thus seq1 . (k + 1) = bD ((seq1 . k),h) by A4 .= seq2 . (k + 1) by A6, A8 ; ::_thesis: verum end; A9: S1[ 0 ] by A3, A5; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A9, A7); hence seq1 = seq2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def7 defines backward_difference DIFF_1:def_7_:_ for f being PartFunc of REAL,REAL for h being real number for b3 being Functional_Sequence of REAL,REAL holds ( b3 = backward_difference (f,h) iff ( b3 . 0 = f & ( for n being Nat holds b3 . (n + 1) = bD ((b3 . n),h) ) ) ); notation let f be PartFunc of REAL,REAL; let h be real number ; synonym bdif (f,h) for backward_difference (f,h); end; theorem Th12: :: DIFF_1:12 for h being Real for f being Function of REAL,REAL for n being Nat holds (bdif (f,h)) . n is Function of REAL,REAL proof let h be Real; ::_thesis: for f being Function of REAL,REAL for n being Nat holds (bdif (f,h)) . n is Function of REAL,REAL let f be Function of REAL,REAL; ::_thesis: for n being Nat holds (bdif (f,h)) . n is Function of REAL,REAL defpred S1[ Nat] means (bdif (f,h)) . \$1 is Function of REAL,REAL; A1: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume (bdif (f,h)) . k is Function of REAL,REAL ; ::_thesis: S1[k + 1] then bD (((bdif (f,h)) . k),h) is Function of REAL,REAL ; hence S1[k + 1] by Def7; ::_thesis: verum end; A2: S1[ 0 ] by Def7; for n being Nat holds S1[n] from NAT_1:sch_2(A2, A1); hence for n being Nat holds (bdif (f,h)) . n is Function of REAL,REAL ; ::_thesis: verum end; theorem :: DIFF_1:13 for n being Element of NAT for h being Real for f being Function of REAL,REAL st f is constant holds for x being Real holds ((bdif (f,h)) . (n + 1)) . x = 0 proof let n be Element of NAT ; ::_thesis: for h being Real for f being Function of REAL,REAL st f is constant holds for x being Real holds ((bdif (f,h)) . (n + 1)) . x = 0 let h be Real; ::_thesis: for f being Function of REAL,REAL st f is constant holds for x being Real holds ((bdif (f,h)) . (n + 1)) . x = 0 let f be Function of REAL,REAL; ::_thesis: ( f is constant implies for x being Real holds ((bdif (f,h)) . (n + 1)) . x = 0 ) assume A1: f is constant ; ::_thesis: for x being Real holds ((bdif (f,h)) . (n + 1)) . x = 0 A2: for x being Real holds (f . x) - (f . (x - h)) = 0 proof let x be Real; ::_thesis: (f . x) - (f . (x - h)) = 0 x - h in REAL ; then A3: x - h in dom f by FUNCT_2:def_1; x in REAL ; then x in dom f by FUNCT_2:def_1; then f . x = f . (x - h) by A1, A3, FUNCT_1:def_10; hence (f . x) - (f . (x - h)) = 0 ; ::_thesis: verum end; for x being Real holds ((bdif (f,h)) . (n + 1)) . x = 0 proof defpred S1[ Element of NAT ] means for x being Real holds ((bdif (f,h)) . (\$1 + 1)) . x = 0 ; A4: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A5: for x being Real holds ((bdif (f,h)) . (k + 1)) . x = 0 ; ::_thesis: S1[k + 1] let x be Real; ::_thesis: ((bdif (f,h)) . ((k + 1) + 1)) . x = 0 A6: ((bdif (f,h)) . (k + 1)) . (x - h) = 0 by A5; A7: (bdif (f,h)) . (k + 1) is Function of REAL,REAL by Th12; ((bdif (f,h)) . (k + 2)) . x = ((bdif (f,h)) . ((k + 1) + 1)) . x .= (bD (((bdif (f,h)) . (k + 1)),h)) . x by Def7 .= (((bdif (f,h)) . (k + 1)) . x) - (((bdif (f,h)) . (k + 1)) . (x - h)) by A7, Th4 .= 0 by A5, A6 ; hence ((bdif (f,h)) . ((k + 1) + 1)) . x = 0 ; ::_thesis: verum end; A8: S1[ 0 ] proof let x be Real; ::_thesis: ((bdif (f,h)) . (0 + 1)) . x = 0 thus ((bdif (f,h)) . (0 + 1)) . x = (bD (((bdif (f,h)) . 0),h)) . x by Def7 .= (bD (f,h)) . x by Def7 .= (f . x) - (f . (x - h)) by Th4 .= 0 by A2 ; ::_thesis: verum end; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A8, A4); hence for x being Real holds ((bdif (f,h)) . (n + 1)) . x = 0 ; ::_thesis: verum end; hence for x being Real holds ((bdif (f,h)) . (n + 1)) . x = 0 ; ::_thesis: verum end; theorem Th14: :: DIFF_1:14 for n being Element of NAT for r, h, x being Real for f being Function of REAL,REAL holds ((bdif ((r (#) f),h)) . (n + 1)) . x = r * (((bdif (f,h)) . (n + 1)) . x) proof let n be Element of NAT ; ::_thesis: for r, h, x being Real for f being Function of REAL,REAL holds ((bdif ((r (#) f),h)) . (n + 1)) . x = r * (((bdif (f,h)) . (n + 1)) . x) let r, h, x be Real; ::_thesis: for f being Function of REAL,REAL holds ((bdif ((r (#) f),h)) . (n + 1)) . x = r * (((bdif (f,h)) . (n + 1)) . x) let f be Function of REAL,REAL; ::_thesis: ((bdif ((r (#) f),h)) . (n + 1)) . x = r * (((bdif (f,h)) . (n + 1)) . x) defpred S1[ Element of NAT ] means for x being Real holds ((bdif ((r (#) f),h)) . (\$1 + 1)) . x = r * (((bdif (f,h)) . (\$1 + 1)) . x); A1: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A2: for x being Real holds ((bdif ((r (#) f),h)) . (k + 1)) . x = r * (((bdif (f,h)) . (k + 1)) . x) ; ::_thesis: S1[k + 1] let x be Real; ::_thesis: ((bdif ((r (#) f),h)) . ((k + 1) + 1)) . x = r * (((bdif (f,h)) . ((k + 1) + 1)) . x) A3: ( ((bdif ((r (#) f),h)) . (k + 1)) . x = r * (((bdif (f,h)) . (k + 1)) . x) & ((bdif ((r (#) f),h)) . (k + 1)) . (x - h) = r * (((bdif (f,h)) . (k + 1)) . (x - h)) ) by A2; A4: (bdif ((r (#) f),h)) . (k + 1) is Function of REAL,REAL by Th12; A5: (bdif (f,h)) . (k + 1) is Function of REAL,REAL by Th12; ((bdif ((r (#) f),h)) . ((k + 1) + 1)) . x = (bD (((bdif ((r (#) f),h)) . (k + 1)),h)) . x by Def7 .= (((bdif ((r (#) f),h)) . (k + 1)) . x) - (((bdif ((r (#) f),h)) . (k + 1)) . (x - h)) by A4, Th4 .= r * ((((bdif (f,h)) . (k + 1)) . x) - (((bdif (f,h)) . (k + 1)) . (x - h))) by A3 .= r * ((bD (((bdif (f,h)) . (k + 1)),h)) . x) by A5, Th4 .= r * (((bdif (f,h)) . ((k + 1) + 1)) . x) by Def7 ; hence ((bdif ((r (#) f),h)) . ((k + 1) + 1)) . x = r * (((bdif (f,h)) . ((k + 1) + 1)) . x) ; ::_thesis: verum end; A6: S1[ 0 ] proof let x be Real; ::_thesis: ((bdif ((r (#) f),h)) . (0 + 1)) . x = r * (((bdif (f,h)) . (0 + 1)) . x) x in REAL ; then A7: x in dom (r (#) f) by FUNCT_2:def_1; x - h in REAL ; then A8: x - h in dom (r (#) f) by FUNCT_2:def_1; ((bdif ((r (#) f),h)) . (0 + 1)) . x = (bD (((bdif ((r (#) f),h)) . 0),h)) . x by Def7 .= (bD ((r (#) f),h)) . x by Def7 .= ((r (#) f) . x) - ((r (#) f) . (x - h)) by Th4 .= ((r (#) f) . x) - (r * (f . (x - h))) by A8, VALUED_1:def_5 .= (r * (f . x)) - (r * (f . (x - h))) by A7, VALUED_1:def_5 .= r * ((f . x) - (f . (x - h))) .= r * ((bD (f,h)) . x) by Th4 .= r * ((bD (((bdif (f,h)) . 0),h)) . x) by Def7 .= r * (((bdif (f,h)) . (0 + 1)) . x) by Def7 ; hence ((bdif ((r (#) f),h)) . (0 + 1)) . x = r * (((bdif (f,h)) . (0 + 1)) . x) ; ::_thesis: verum end; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A6, A1); hence ((bdif ((r (#) f),h)) . (n + 1)) . x = r * (((bdif (f,h)) . (n + 1)) . x) ; ::_thesis: verum end; theorem Th15: :: DIFF_1:15 for n being Element of NAT for h, x being Real for f1, f2 being Function of REAL,REAL holds ((bdif ((f1 + f2),h)) . (n + 1)) . x = (((bdif (f1,h)) . (n + 1)) . x) + (((bdif (f2,h)) . (n + 1)) . x) proof let n be Element of NAT ; ::_thesis: for h, x being Real for f1, f2 being Function of REAL,REAL holds ((bdif ((f1 + f2),h)) . (n + 1)) . x = (((bdif (f1,h)) . (n + 1)) . x) + (((bdif (f2,h)) . (n + 1)) . x) let h, x be Real; ::_thesis: for f1, f2 being Function of REAL,REAL holds ((bdif ((f1 + f2),h)) . (n + 1)) . x = (((bdif (f1,h)) . (n + 1)) . x) + (((bdif (f2,h)) . (n + 1)) . x) let f1, f2 be Function of REAL,REAL; ::_thesis: ((bdif ((f1 + f2),h)) . (n + 1)) . x = (((bdif (f1,h)) . (n + 1)) . x) + (((bdif (f2,h)) . (n + 1)) . x) defpred S1[ Element of NAT ] means for x being Real holds ((bdif ((f1 + f2),h)) . (\$1 + 1)) . x = (((bdif (f1,h)) . (\$1 + 1)) . x) + (((bdif (f2,h)) . (\$1 + 1)) . x); A1: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A2: for x being Real holds ((bdif ((f1 + f2),h)) . (k + 1)) . x = (((bdif (f1,h)) . (k + 1)) . x) + (((bdif (f2,h)) . (k + 1)) . x) ; ::_thesis: S1[k + 1] let x be Real; ::_thesis: ((bdif ((f1 + f2),h)) . ((k + 1) + 1)) . x = (((bdif (f1,h)) . ((k + 1) + 1)) . x) + (((bdif (f2,h)) . ((k + 1) + 1)) . x) A3: ( ((bdif ((f1 + f2),h)) . (k + 1)) . x = (((bdif (f1,h)) . (k + 1)) . x) + (((bdif (f2,h)) . (k + 1)) . x) & ((bdif ((f1 + f2),h)) . (k + 1)) . (x - h) = (((bdif (f1,h)) . (k + 1)) . (x - h)) + (((bdif (f2,h)) . (k + 1)) . (x - h)) ) by A2; A4: (bdif ((f1 + f2),h)) . (k + 1) is Function of REAL,REAL by Th12; A5: (bdif (f2,h)) . (k + 1) is Function of REAL,REAL by Th12; A6: (bdif (f1,h)) . (k + 1) is Function of REAL,REAL by Th12; ((bdif ((f1 + f2),h)) . ((k + 1) + 1)) . x = (bD (((bdif ((f1 + f2),h)) . (k + 1)),h)) . x by Def7 .= (((bdif ((f1 + f2),h)) . (k + 1)) . x) - (((bdif ((f1 + f2),h)) . (k + 1)) . (x - h)) by A4, Th4 .= ((((bdif (f1,h)) . (k + 1)) . x) - (((bdif (f1,h)) . (k + 1)) . (x - h))) + ((((bdif (f2,h)) . (k + 1)) . x) - (((bdif (f2,h)) . (k + 1)) . (x - h))) by A3 .= ((bD (((bdif (f1,h)) . (k + 1)),h)) . x) + ((((bdif (f2,h)) . (k + 1)) . x) - (((bdif (f2,h)) . (k + 1)) . (x - h))) by A6, Th4 .= ((bD (((bdif (f1,h)) . (k + 1)),h)) . x) + ((bD (((bdif (f2,h)) . (k + 1)),h)) . x) by A5, Th4 .= (((bdif (f1,h)) . ((k + 1) + 1)) . x) + ((bD (((bdif (f2,h)) . (k + 1)),h)) . x) by Def7 .= (((bdif (f1,h)) . ((k + 1) + 1)) . x) + (((bdif (f2,h)) . ((k + 1) + 1)) . x) by Def7 ; hence ((bdif ((f1 + f2),h)) . ((k + 1) + 1)) . x = (((bdif (f1,h)) . ((k + 1) + 1)) . x) + (((bdif (f2,h)) . ((k + 1) + 1)) . x) ; ::_thesis: verum end; A7: S1[ 0 ] proof let x be Real; ::_thesis: ((bdif ((f1 + f2),h)) . (0 + 1)) . x = (((bdif (f1,h)) . (0 + 1)) . x) + (((bdif (f2,h)) . (0 + 1)) . x) ((bdif ((f1 + f2),h)) . (0 + 1)) . x = (bD (((bdif ((f1 + f2),h)) . 0),h)) . x by Def7 .= (bD ((f1 + f2),h)) . x by Def7 .= ((f1 + f2) . x) - ((f1 + f2) . (x - h)) by Th4 .= ((f1 . x) + (f2 . x)) - ((f1 + f2) . (x - h)) by VALUED_1:1 .= ((f1 . x) + (f2 . x)) - ((f1 . (x - h)) + (f2 . (x - h))) by VALUED_1:1 .= ((f1 . x) - (f1 . (x - h))) + ((f2 . x) - (f2 . (x - h))) .= ((bD (f1,h)) . x) + ((f2 . x) - (f2 . (x - h))) by Th4 .= ((bD (f1,h)) . x) + ((bD (f2,h)) . x) by Th4 .= ((bD (((bdif (f1,h)) . 0),h)) . x) + ((bD (f2,h)) . x) by Def7 .= ((bD (((bdif (f1,h)) . 0),h)) . x) + ((bD (((bdif (f2,h)) . 0),h)) . x) by Def7 .= (((bdif (f1,h)) . (0 + 1)) . x) + ((bD (((bdif (f2,h)) . 0),h)) . x) by Def7 .= (((bdif (f1,h)) . (0 + 1)) . x) + (((bdif (f2,h)) . (0 + 1)) . x) by Def7 ; hence ((bdif ((f1 + f2),h)) . (0 + 1)) . x = (((bdif (f1,h)) . (0 + 1)) . x) + (((bdif (f2,h)) . (0 + 1)) . x) ; ::_thesis: verum end; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A7, A1); hence ((bdif ((f1 + f2),h)) . (n + 1)) . x = (((bdif (f1,h)) . (n + 1)) . x) + (((bdif (f2,h)) . (n + 1)) . x) ; ::_thesis: verum end; theorem :: DIFF_1:16 for n being Element of NAT for h, x being Real for f1, f2 being Function of REAL,REAL holds ((bdif ((f1 - f2),h)) . (n + 1)) . x = (((bdif (f1,h)) . (n + 1)) . x) - (((bdif (f2,h)) . (n + 1)) . x) proof let n be Element of NAT ; ::_thesis: for h, x being Real for f1, f2 being Function of REAL,REAL holds ((bdif ((f1 - f2),h)) . (n + 1)) . x = (((bdif (f1,h)) . (n + 1)) . x) - (((bdif (f2,h)) . (n + 1)) . x) let h, x be Real; ::_thesis: for f1, f2 being Function of REAL,REAL holds ((bdif ((f1 - f2),h)) . (n + 1)) . x = (((bdif (f1,h)) . (n + 1)) . x) - (((bdif (f2,h)) . (n + 1)) . x) let f1, f2 be Function of REAL,REAL; ::_thesis: ((bdif ((f1 - f2),h)) . (n + 1)) . x = (((bdif (f1,h)) . (n + 1)) . x) - (((bdif (f2,h)) . (n + 1)) . x) defpred S1[ Element of NAT ] means for x being Real holds ((bdif ((f1 - f2),h)) . (\$1 + 1)) . x = (((bdif (f1,h)) . (\$1 + 1)) . x) - (((bdif (f2,h)) . (\$1 + 1)) . x); A1: S1[ 0 ] proof let x be Real; ::_thesis: ((bdif ((f1 - f2),h)) . (0 + 1)) . x = (((bdif (f1,h)) . (0 + 1)) . x) - (((bdif (f2,h)) . (0 + 1)) . x) x in REAL ; then ( x in dom f1 & x in dom f2 ) by FUNCT_2:def_1; then x in (dom f1) /\ (dom f2) by XBOOLE_0:def_4; then A2: x in dom (f1 - f2) by VALUED_1:12; x - h in REAL ; then ( x - h in dom f1 & x - h in dom f2 ) by FUNCT_2:def_1; then x - h in (dom f1) /\ (dom f2) by XBOOLE_0:def_4; then A3: x - h in dom (f1 - f2) by VALUED_1:12; ((bdif ((f1 - f2),h)) . (0 + 1)) . x = (bD (((bdif ((f1 - f2),h)) . 0),h)) . x by Def7 .= (bD ((f1 - f2),h)) . x by Def7 .= ((f1 - f2) . x) - ((f1 - f2) . (x - h)) by Th4 .= ((f1 . x) - (f2 . x)) - ((f1 - f2) . (x - h)) by A2, VALUED_1:13 .= ((f1 . x) - (f2 . x)) - ((f1 . (x - h)) - (f2 . (x - h))) by A3, VALUED_1:13 .= ((f1 . x) - (f1 . (x - h))) - ((f2 . x) - (f2 . (x - h))) .= ((bD (f1,h)) . x) - ((f2 . x) - (f2 . (x - h))) by Th4 .= ((bD (f1,h)) . x) - ((bD (f2,h)) . x) by Th4 .= ((bD (((bdif (f1,h)) . 0),h)) . x) - ((bD (f2,h)) . x) by Def7 .= ((bD (((bdif (f1,h)) . 0),h)) . x) - ((bD (((bdif (f2,h)) . 0),h)) . x) by Def7 .= (((bdif (f1,h)) . (0 + 1)) . x) - ((bD (((bdif (f2,h)) . 0),h)) . x) by Def7 .= (((bdif (f1,h)) . (0 + 1)) . x) - (((bdif (f2,h)) . (0 + 1)) . x) by Def7 ; hence ((bdif ((f1 - f2),h)) . (0 + 1)) . x = (((bdif (f1,h)) . (0 + 1)) . x) - (((bdif (f2,h)) . (0 + 1)) . x) ; ::_thesis: verum end; A4: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A5: for x being Real holds ((bdif ((f1 - f2),h)) . (k + 1)) . x = (((bdif (f1,h)) . (k + 1)) . x) - (((bdif (f2,h)) . (k + 1)) . x) ; ::_thesis: S1[k + 1] let x be Real; ::_thesis: ((bdif ((f1 - f2),h)) . ((k + 1) + 1)) . x = (((bdif (f1,h)) . ((k + 1) + 1)) . x) - (((bdif (f2,h)) . ((k + 1) + 1)) . x) A6: ( ((bdif ((f1 - f2),h)) . (k + 1)) . x = (((bdif (f1,h)) . (k + 1)) . x) - (((bdif (f2,h)) . (k + 1)) . x) & ((bdif ((f1 - f2),h)) . (k + 1)) . (x - h) = (((bdif (f1,h)) . (k + 1)) . (x - h)) - (((bdif (f2,h)) . (k + 1)) . (x - h)) ) by A5; A7: (bdif ((f1 - f2),h)) . (k + 1) is Function of REAL,REAL by Th12; A8: (bdif (f2,h)) . (k + 1) is Function of REAL,REAL by Th12; A9: (bdif (f1,h)) . (k + 1) is Function of REAL,REAL by Th12; ((bdif ((f1 - f2),h)) . ((k + 1) + 1)) . x = (bD (((bdif ((f1 - f2),h)) . (k + 1)),h)) . x by Def7 .= (((bdif ((f1 - f2),h)) . (k + 1)) . x) - (((bdif ((f1 - f2),h)) . (k + 1)) . (x - h)) by A7, Th4 .= ((((bdif (f1,h)) . (k + 1)) . x) - (((bdif (f1,h)) . (k + 1)) . (x - h))) - ((((bdif (f2,h)) . (k + 1)) . x) - (((bdif (f2,h)) . (k + 1)) . (x - h))) by A6 .= ((bD (((bdif (f1,h)) . (k + 1)),h)) . x) - ((((bdif (f2,h)) . (k + 1)) . x) - (((bdif (f2,h)) . (k + 1)) . (x - h))) by A9, Th4 .= ((bD (((bdif (f1,h)) . (k + 1)),h)) . x) - ((bD (((bdif (f2,h)) . (k + 1)),h)) . x) by A8, Th4 .= (((bdif (f1,h)) . ((k + 1) + 1)) . x) - ((bD (((bdif (f2,h)) . (k + 1)),h)) . x) by Def7 .= (((bdif (f1,h)) . ((k + 1) + 1)) . x) - (((bdif (f2,h)) . ((k + 1) + 1)) . x) by Def7 ; hence ((bdif ((f1 - f2),h)) . ((k + 1) + 1)) . x = (((bdif (f1,h)) . ((k + 1) + 1)) . x) - (((bdif (f2,h)) . ((k + 1) + 1)) . x) ; ::_thesis: verum end; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A1, A4); hence ((bdif ((f1 - f2),h)) . (n + 1)) . x = (((bdif (f1,h)) . (n + 1)) . x) - (((bdif (f2,h)) . (n + 1)) . x) ; ::_thesis: verum end; theorem :: DIFF_1:17 for n being Element of NAT for r1, r2, h, x being Real for f1, f2 being Function of REAL,REAL holds ((bdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) . x = (r1 * (((bdif (f1,h)) . (n + 1)) . x)) + (r2 * (((bdif (f2,h)) . (n + 1)) . x)) proof let n be Element of NAT ; ::_thesis: for r1, r2, h, x being Real for f1, f2 being Function of REAL,REAL holds ((bdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) . x = (r1 * (((bdif (f1,h)) . (n + 1)) . x)) + (r2 * (((bdif (f2,h)) . (n + 1)) . x)) let r1, r2, h, x be Real; ::_thesis: for f1, f2 being Function of REAL,REAL holds ((bdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) . x = (r1 * (((bdif (f1,h)) . (n + 1)) . x)) + (r2 * (((bdif (f2,h)) . (n + 1)) . x)) let f1, f2 be Function of REAL,REAL; ::_thesis: ((bdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) . x = (r1 * (((bdif (f1,h)) . (n + 1)) . x)) + (r2 * (((bdif (f2,h)) . (n + 1)) . x)) set g1 = r1 (#) f1; set g2 = r2 (#) f2; ((bdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) . x = (((bdif ((r1 (#) f1),h)) . (n + 1)) . x) + (((bdif ((r2 (#) f2),h)) . (n + 1)) . x) by Th15 .= (r1 * (((bdif (f1,h)) . (n + 1)) . x)) + (((bdif ((r2 (#) f2),h)) . (n + 1)) . x) by Th14 .= (r1 * (((bdif (f1,h)) . (n + 1)) . x)) + (r2 * (((bdif (f2,h)) . (n + 1)) . x)) by Th14 ; hence ((bdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) . x = (r1 * (((bdif (f1,h)) . (n + 1)) . x)) + (r2 * (((bdif (f2,h)) . (n + 1)) . x)) ; ::_thesis: verum end; theorem :: DIFF_1:18 for h, x being Real for f being Function of REAL,REAL holds ((bdif (f,h)) . 1) . x = (f . x) - ((Shift (f,(- h))) . x) proof let h, x be Real; ::_thesis: for f being Function of REAL,REAL holds ((bdif (f,h)) . 1) . x = (f . x) - ((Shift (f,(- h))) . x) let f be Function of REAL,REAL; ::_thesis: ((bdif (f,h)) . 1) . x = (f . x) - ((Shift (f,(- h))) . x) set f2 = Shift (f,(- h)); ((bdif (f,h)) . 1) . x = ((bdif (f,h)) . (0 + 1)) . x .= (bD (((bdif (f,h)) . 0),h)) . x by Def7 .= (bD (f,h)) . x by Def7 .= (f . x) - (f . (x - h)) by Th4 .= (f . x) - (f . (x + (- h))) .= (f . x) - ((Shift (f,(- h))) . x) by Def2 ; hence ((bdif (f,h)) . 1) . x = (f . x) - ((Shift (f,(- h))) . x) ; ::_thesis: verum end; definition let f be PartFunc of REAL,REAL; let h be real number ; func central_difference (f,h) -> Functional_Sequence of REAL,REAL means :Def8: :: DIFF_1:def 8 ( it . 0 = f & ( for n being Nat holds it . (n + 1) = cD ((it . n),h) ) ); existence ex b1 being Functional_Sequence of REAL,REAL st ( b1 . 0 = f & ( for n being Nat holds b1 . (n + 1) = cD ((b1 . n),h) ) ) proof reconsider fZ = f as Element of PFuncs (REAL,REAL) by PARTFUN1:45; defpred S1[ set , set , set ] means ex g being PartFunc of REAL,REAL st ( \$2 = g & \$3 = cD (g,h) ); A1: for n being Element of NAT for x being Element of PFuncs (REAL,REAL) ex y being Element of PFuncs (REAL,REAL) st S1[n,x,y] proof let n be Element of NAT ; ::_thesis: for x being Element of PFuncs (REAL,REAL) ex y being Element of PFuncs (REAL,REAL) st S1[n,x,y] let x be Element of PFuncs (REAL,REAL); ::_thesis: ex y being Element of PFuncs (REAL,REAL) st S1[n,x,y] reconsider x9 = x as PartFunc of REAL,REAL by PARTFUN1:46; reconsider y = cD (x9,h) as Element of PFuncs (REAL,REAL) by PARTFUN1:45; ex w being PartFunc of REAL,REAL st ( x = w & y = cD (w,h) ) ; hence ex y being Element of PFuncs (REAL,REAL) st S1[n,x,y] ; ::_thesis: verum end; consider g being Function of NAT,(PFuncs (REAL,REAL)) such that A2: ( g . 0 = fZ & ( for n being Element of NAT holds S1[n,g . n,g . (n + 1)] ) ) from RECDEF_1:sch_2(A1); reconsider g = g as Functional_Sequence of REAL,REAL ; take g ; ::_thesis: ( g . 0 = f & ( for n being Nat holds g . (n + 1) = cD ((g . n),h) ) ) thus g . 0 = f by A2; ::_thesis: for n being Nat holds g . (n + 1) = cD ((g . n),h) let i be Nat; ::_thesis: g . (i + 1) = cD ((g . i),h) i in NAT by ORDINAL1:def_12; then S1[i,g . i,g . (i + 1)] by A2; hence g . (i + 1) = cD ((g . i),h) ; ::_thesis: verum end; uniqueness for b1, b2 being Functional_Sequence of REAL,REAL st b1 . 0 = f & ( for n being Nat holds b1 . (n + 1) = cD ((b1 . n),h) ) & b2 . 0 = f & ( for n being Nat holds b2 . (n + 1) = cD ((b2 . n),h) ) holds b1 = b2 proof let seq1, seq2 be Functional_Sequence of REAL,REAL; ::_thesis: ( seq1 . 0 = f & ( for n being Nat holds seq1 . (n + 1) = cD ((seq1 . n),h) ) & seq2 . 0 = f & ( for n being Nat holds seq2 . (n + 1) = cD ((seq2 . n),h) ) implies seq1 = seq2 ) assume that A3: seq1 . 0 = f and A4: for n being Nat holds seq1 . (n + 1) = cD ((seq1 . n),h) and A5: seq2 . 0 = f and A6: for n being Nat holds seq2 . (n + 1) = cD ((seq2 . n),h) ; ::_thesis: seq1 = seq2 defpred S1[ Nat] means seq1 . \$1 = seq2 . \$1; A7: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A8: S1[k] ; ::_thesis: S1[k + 1] thus seq1 . (k + 1) = cD ((seq1 . k),h) by A4 .= seq2 . (k + 1) by A6, A8 ; ::_thesis: verum end; A9: S1[ 0 ] by A3, A5; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A9, A7); hence seq1 = seq2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def8 defines central_difference DIFF_1:def_8_:_ for f being PartFunc of REAL,REAL for h being real number for b3 being Functional_Sequence of REAL,REAL holds ( b3 = central_difference (f,h) iff ( b3 . 0 = f & ( for n being Nat holds b3 . (n + 1) = cD ((b3 . n),h) ) ) ); notation let f be PartFunc of REAL,REAL; let h be real number ; synonym cdif (f,h) for central_difference (f,h); end; theorem Th19: :: DIFF_1:19 for h being Real for f being Function of REAL,REAL for n being Nat holds (cdif (f,h)) . n is Function of REAL,REAL proof let h be Real; ::_thesis: for f being Function of REAL,REAL for n being Nat holds (cdif (f,h)) . n is Function of REAL,REAL let f be Function of REAL,REAL; ::_thesis: for n being Nat holds (cdif (f,h)) . n is Function of REAL,REAL defpred S1[ Nat] means (cdif (f,h)) . \$1 is Function of REAL,REAL; A1: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume (cdif (f,h)) . k is Function of REAL,REAL ; ::_thesis: S1[k + 1] then cD (((cdif (f,h)) . k),h) is Function of REAL,REAL ; hence S1[k + 1] by Def8; ::_thesis: verum end; A2: S1[ 0 ] by Def8; for n being Nat holds S1[n] from NAT_1:sch_2(A2, A1); hence for n being Nat holds (cdif (f,h)) . n is Function of REAL,REAL ; ::_thesis: verum end; theorem :: DIFF_1:20 for n being Element of NAT for h being Real for f being Function of REAL,REAL st f is constant holds for x being Real holds ((cdif (f,h)) . (n + 1)) . x = 0 proof let n be Element of NAT ; ::_thesis: for h being Real for f being Function of REAL,REAL st f is constant holds for x being Real holds ((cdif (f,h)) . (n + 1)) . x = 0 let h be Real; ::_thesis: for f being Function of REAL,REAL st f is constant holds for x being Real holds ((cdif (f,h)) . (n + 1)) . x = 0 let f be Function of REAL,REAL; ::_thesis: ( f is constant implies for x being Real holds ((cdif (f,h)) . (n + 1)) . x = 0 ) defpred S1[ Element of NAT ] means for x being Real holds ((cdif (f,h)) . (\$1 + 1)) . x = 0 ; assume A1: f is constant ; ::_thesis: for x being Real holds ((cdif (f,h)) . (n + 1)) . x = 0 A2: for x being Real holds (f . (x + (h / 2))) - (f . (x - (h / 2))) = 0 proof let x be Real; ::_thesis: (f . (x + (h / 2))) - (f . (x - (h / 2))) = 0 x - (h / 2) in REAL ; then A3: x - (h / 2) in dom f by FUNCT_2:def_1; x + (h / 2) in REAL ; then x + (h / 2) in dom f by FUNCT_2:def_1; then f . (x + (h / 2)) = f . (x - (h / 2)) by A1, A3, FUNCT_1:def_10; hence (f . (x + (h / 2))) - (f . (x - (h / 2))) = 0 ; ::_thesis: verum end; A4: S1[ 0 ] proof let x be Real; ::_thesis: ((cdif (f,h)) . (0 + 1)) . x = 0 thus ((cdif (f,h)) . (0 + 1)) . x = (cD (((cdif (f,h)) . 0),h)) . x by Def8 .= (cD (f,h)) . x by Def8 .= (f . (x + (h / 2))) - (f . (x - (h / 2))) by Th5 .= 0 by A2 ; ::_thesis: verum end; A5: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A6: for x being Real holds ((cdif (f,h)) . (k + 1)) . x = 0 ; ::_thesis: S1[k + 1] let x be Real; ::_thesis: ((cdif (f,h)) . ((k + 1) + 1)) . x = 0 A7: ((cdif (f,h)) . (k + 1)) . (x - (h / 2)) = 0 by A6; A8: (cdif (f,h)) . (k + 1) is Function of REAL,REAL by Th19; ((cdif (f,h)) . (k + 2)) . x = ((cdif (f,h)) . ((k + 1) + 1)) . x .= (cD (((cdif (f,h)) . (k + 1)),h)) . x by Def8 .= (((cdif (f,h)) . (k + 1)) . (x + (h / 2))) - (((cdif (f,h)) . (k + 1)) . (x - (h / 2))) by A8, Th5 .= 0 by A6, A7 ; hence ((cdif (f,h)) . ((k + 1) + 1)) . x = 0 ; ::_thesis: verum end; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A5); hence for x being Real holds ((cdif (f,h)) . (n + 1)) . x = 0 ; ::_thesis: verum end; theorem Th21: :: DIFF_1:21 for n being Element of NAT for r, h, x being Real for f being Function of REAL,REAL holds ((cdif ((r (#) f),h)) . (n + 1)) . x = r * (((cdif (f,h)) . (n + 1)) . x) proof let n be Element of NAT ; ::_thesis: for r, h, x being Real for f being Function of REAL,REAL holds ((cdif ((r (#) f),h)) . (n + 1)) . x = r * (((cdif (f,h)) . (n + 1)) . x) let r, h, x be Real; ::_thesis: for f being Function of REAL,REAL holds ((cdif ((r (#) f),h)) . (n + 1)) . x = r * (((cdif (f,h)) . (n + 1)) . x) let f be Function of REAL,REAL; ::_thesis: ((cdif ((r (#) f),h)) . (n + 1)) . x = r * (((cdif (f,h)) . (n + 1)) . x) defpred S1[ Element of NAT ] means for x being Real holds ((cdif ((r (#) f),h)) . (\$1 + 1)) . x = r * (((cdif (f,h)) . (\$1 + 1)) . x); A1: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A2: for x being Real holds ((cdif ((r (#) f),h)) . (k + 1)) . x = r * (((cdif (f,h)) . (k + 1)) . x) ; ::_thesis: S1[k + 1] let x be Real; ::_thesis: ((cdif ((r (#) f),h)) . ((k + 1) + 1)) . x = r * (((cdif (f,h)) . ((k + 1) + 1)) . x) A3: ( ((cdif ((r (#) f),h)) . (k + 1)) . (x - (h / 2)) = r * (((cdif (f,h)) . (k + 1)) . (x - (h / 2))) & ((cdif ((r (#) f),h)) . (k + 1)) . (x + (h / 2)) = r * (((cdif (f,h)) . (k + 1)) . (x + (h / 2))) ) by A2; A4: (cdif ((r (#) f),h)) . (k + 1) is Function of REAL,REAL by Th19; A5: (cdif (f,h)) . (k + 1) is Function of REAL,REAL by Th19; ((cdif ((r (#) f),h)) . ((k + 1) + 1)) . x = (cD (((cdif ((r (#) f),h)) . (k + 1)),h)) . x by Def8 .= (((cdif ((r (#) f),h)) . (k + 1)) . (x + (h / 2))) - (((cdif ((r (#) f),h)) . (k + 1)) . (x - (h / 2))) by A4, Th5 .= r * ((((cdif (f,h)) . (k + 1)) . (x + (h / 2))) - (((cdif (f,h)) . (k + 1)) . (x - (h / 2)))) by A3 .= r * ((cD (((cdif (f,h)) . (k + 1)),h)) . x) by A5, Th5 .= r * (((cdif (f,h)) . ((k + 1) + 1)) . x) by Def8 ; hence ((cdif ((r (#) f),h)) . ((k + 1) + 1)) . x = r * (((cdif (f,h)) . ((k + 1) + 1)) . x) ; ::_thesis: verum end; A6: S1[ 0 ] proof let x be Real; ::_thesis: ((cdif ((r (#) f),h)) . (0 + 1)) . x = r * (((cdif (f,h)) . (0 + 1)) . x) x + (h / 2) in REAL ; then A7: x + (h / 2) in dom (r (#) f) by FUNCT_2:def_1; x - (h / 2) in REAL ; then A8: x - (h / 2) in dom (r (#) f) by FUNCT_2:def_1; ((cdif ((r (#) f),h)) . (0 + 1)) . x = (cD (((cdif ((r (#) f),h)) . 0),h)) . x by Def8 .= (cD ((r (#) f),h)) . x by Def8 .= ((r (#) f) . (x + (h / 2))) - ((r (#) f) . (x - (h / 2))) by Th5 .= (r * (f . (x + (h / 2)))) - ((r (#) f) . (x - (h / 2))) by A7, VALUED_1:def_5 .= (r * (f . (x + (h / 2)))) - (r * (f . (x - (h / 2)))) by A8, VALUED_1:def_5 .= r * ((f . (x + (h / 2))) - (f . (x - (h / 2)))) .= r * ((cD (f,h)) . x) by Th5 .= r * ((cD (((cdif (f,h)) . 0),h)) . x) by Def8 .= r * (((cdif (f,h)) . (0 + 1)) . x) by Def8 ; hence ((cdif ((r (#) f),h)) . (0 + 1)) . x = r * (((cdif (f,h)) . (0 + 1)) . x) ; ::_thesis: verum end; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A6, A1); hence ((cdif ((r (#) f),h)) . (n + 1)) . x = r * (((cdif (f,h)) . (n + 1)) . x) ; ::_thesis: verum end; theorem Th22: :: DIFF_1:22 for n being Element of NAT for h, x being Real for f1, f2 being Function of REAL,REAL holds ((cdif ((f1 + f2),h)) . (n + 1)) . x = (((cdif (f1,h)) . (n + 1)) . x) + (((cdif (f2,h)) . (n + 1)) . x) proof let n be Element of NAT ; ::_thesis: for h, x being Real for f1, f2 being Function of REAL,REAL holds ((cdif ((f1 + f2),h)) . (n + 1)) . x = (((cdif (f1,h)) . (n + 1)) . x) + (((cdif (f2,h)) . (n + 1)) . x) let h, x be Real; ::_thesis: for f1, f2 being Function of REAL,REAL holds ((cdif ((f1 + f2),h)) . (n + 1)) . x = (((cdif (f1,h)) . (n + 1)) . x) + (((cdif (f2,h)) . (n + 1)) . x) let f1, f2 be Function of REAL,REAL; ::_thesis: ((cdif ((f1 + f2),h)) . (n + 1)) . x = (((cdif (f1,h)) . (n + 1)) . x) + (((cdif (f2,h)) . (n + 1)) . x) defpred S1[ Element of NAT ] means for x being Real holds ((cdif ((f1 + f2),h)) . (\$1 + 1)) . x = (((cdif (f1,h)) . (\$1 + 1)) . x) + (((cdif (f2,h)) . (\$1 + 1)) . x); A1: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A2: for x being Real holds ((cdif ((f1 + f2),h)) . (k + 1)) . x = (((cdif (f1,h)) . (k + 1)) . x) + (((cdif (f2,h)) . (k + 1)) . x) ; ::_thesis: S1[k + 1] let x be Real; ::_thesis: ((cdif ((f1 + f2),h)) . ((k + 1) + 1)) . x = (((cdif (f1,h)) . ((k + 1) + 1)) . x) + (((cdif (f2,h)) . ((k + 1) + 1)) . x) A3: ( ((cdif ((f1 + f2),h)) . (k + 1)) . (x - (h / 2)) = (((cdif (f1,h)) . (k + 1)) . (x - (h / 2))) + (((cdif (f2,h)) . (k + 1)) . (x - (h / 2))) & ((cdif ((f1 + f2),h)) . (k + 1)) . (x + (h / 2)) = (((cdif (f1,h)) . (k + 1)) . (x + (h / 2))) + (((cdif (f2,h)) . (k + 1)) . (x + (h / 2))) ) by A2; A4: (cdif ((f1 + f2),h)) . (k + 1) is Function of REAL,REAL by Th19; A5: (cdif (f2,h)) . (k + 1) is Function of REAL,REAL by Th19; A6: (cdif (f1,h)) . (k + 1) is Function of REAL,REAL by Th19; ((cdif ((f1 + f2),h)) . ((k + 1) + 1)) . x = (cD (((cdif ((f1 + f2),h)) . (k + 1)),h)) . x by Def8 .= (((cdif ((f1 + f2),h)) . (k + 1)) . (x + (h / 2))) - (((cdif ((f1 + f2),h)) . (k + 1)) . (x - (h / 2))) by A4, Th5 .= ((((cdif (f1,h)) . (k + 1)) . (x + (h / 2))) - (((cdif (f1,h)) . (k + 1)) . (x - (h / 2)))) + ((((cdif (f2,h)) . (k + 1)) . (x + (h / 2))) - (((cdif (f2,h)) . (k + 1)) . (x - (h / 2)))) by A3 .= ((cD (((cdif (f1,h)) . (k + 1)),h)) . x) + ((((cdif (f2,h)) . (k + 1)) . (x + (h / 2))) - (((cdif (f2,h)) . (k + 1)) . (x - (h / 2)))) by A6, Th5 .= ((cD (((cdif (f1,h)) . (k + 1)),h)) . x) + ((cD (((cdif (f2,h)) . (k + 1)),h)) . x) by A5, Th5 .= (((cdif (f1,h)) . ((k + 1) + 1)) . x) + ((cD (((cdif (f2,h)) . (k + 1)),h)) . x) by Def8 .= (((cdif (f1,h)) . ((k + 1) + 1)) . x) + (((cdif (f2,h)) . ((k + 1) + 1)) . x) by Def8 ; hence ((cdif ((f1 + f2),h)) . ((k + 1) + 1)) . x = (((cdif (f1,h)) . ((k + 1) + 1)) . x) + (((cdif (f2,h)) . ((k + 1) + 1)) . x) ; ::_thesis: verum end; A7: S1[ 0 ] proof let x be Real; ::_thesis: ((cdif ((f1 + f2),h)) . (0 + 1)) . x = (((cdif (f1,h)) . (0 + 1)) . x) + (((cdif (f2,h)) . (0 + 1)) . x) ((cdif ((f1 + f2),h)) . (0 + 1)) . x = (cD (((cdif ((f1 + f2),h)) . 0),h)) . x by Def8 .= (cD ((f1 + f2),h)) . x by Def8 .= ((f1 + f2) . (x + (h / 2))) - ((f1 + f2) . (x - (h / 2))) by Th5 .= ((f1 . (x + (h / 2))) + (f2 . (x + (h / 2)))) - ((f1 + f2) . (x - (h / 2))) by VALUED_1:1 .= ((f1 . (x + (h / 2))) + (f2 . (x + (h / 2)))) - ((f1 . (x - (h / 2))) + (f2 . (x - (h / 2)))) by VALUED_1:1 .= ((f1 . (x + (h / 2))) - (f1 . (x - (h / 2)))) + ((f2 . (x + (h / 2))) - (f2 . (x - (h / 2)))) .= ((cD (f1,h)) . x) + ((f2 . (x + (h / 2))) - (f2 . (x - (h / 2)))) by Th5 .= ((cD (f1,h)) . x) + ((cD (f2,h)) . x) by Th5 .= ((cD (((cdif (f1,h)) . 0),h)) . x) + ((cD (f2,h)) . x) by Def8 .= ((cD (((cdif (f1,h)) . 0),h)) . x) + ((cD (((cdif (f2,h)) . 0),h)) . x) by Def8 .= (((cdif (f1,h)) . (0 + 1)) . x) + ((cD (((cdif (f2,h)) . 0),h)) . x) by Def8 .= (((cdif (f1,h)) . (0 + 1)) . x) + (((cdif (f2,h)) . (0 + 1)) . x) by Def8 ; hence ((cdif ((f1 + f2),h)) . (0 + 1)) . x = (((cdif (f1,h)) . (0 + 1)) . x) + (((cdif (f2,h)) . (0 + 1)) . x) ; ::_thesis: verum end; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A7, A1); hence ((cdif ((f1 + f2),h)) . (n + 1)) . x = (((cdif (f1,h)) . (n + 1)) . x) + (((cdif (f2,h)) . (n + 1)) . x) ; ::_thesis: verum end; theorem :: DIFF_1:23 for n being Element of NAT for h, x being Real for f1, f2 being Function of REAL,REAL holds ((cdif ((f1 - f2),h)) . (n + 1)) . x = (((cdif (f1,h)) . (n + 1)) . x) - (((cdif (f2,h)) . (n + 1)) . x) proof let n be Element of NAT ; ::_thesis: for h, x being Real for f1, f2 being Function of REAL,REAL holds ((cdif ((f1 - f2),h)) . (n + 1)) . x = (((cdif (f1,h)) . (n + 1)) . x) - (((cdif (f2,h)) . (n + 1)) . x) let h, x be Real; ::_thesis: for f1, f2 being Function of REAL,REAL holds ((cdif ((f1 - f2),h)) . (n + 1)) . x = (((cdif (f1,h)) . (n + 1)) . x) - (((cdif (f2,h)) . (n + 1)) . x) let f1, f2 be Function of REAL,REAL; ::_thesis: ((cdif ((f1 - f2),h)) . (n + 1)) . x = (((cdif (f1,h)) . (n + 1)) . x) - (((cdif (f2,h)) . (n + 1)) . x) defpred S1[ Element of NAT ] means for x being Real holds ((cdif ((f1 - f2),h)) . (\$1 + 1)) . x = (((cdif (f1,h)) . (\$1 + 1)) . x) - (((cdif (f2,h)) . (\$1 + 1)) . x); A1: S1[ 0 ] proof let x be Real; ::_thesis: ((cdif ((f1 - f2),h)) . (0 + 1)) . x = (((cdif (f1,h)) . (0 + 1)) . x) - (((cdif (f2,h)) . (0 + 1)) . x) x - (h / 2) in REAL ; then ( x - (h / 2) in dom f1 & x - (h / 2) in dom f2 ) by FUNCT_2:def_1; then x - (h / 2) in (dom f1) /\ (dom f2) by XBOOLE_0:def_4; then A2: x - (h / 2) in dom (f1 - f2) by VALUED_1:12; x + (h / 2) in REAL ; then ( x + (h / 2) in dom f1 & x + (h / 2) in dom f2 ) by FUNCT_2:def_1; then x + (h / 2) in (dom f1) /\ (dom f2) by XBOOLE_0:def_4; then A3: x + (h / 2) in dom (f1 - f2) by VALUED_1:12; ((cdif ((f1 - f2),h)) . (0 + 1)) . x = (cD (((cdif ((f1 - f2),h)) . 0),h)) . x by Def8 .= (cD ((f1 - f2),h)) . x by Def8 .= ((f1 - f2) . (x + (h / 2))) - ((f1 - f2) . (x - (h / 2))) by Th5 .= ((f1 . (x + (h / 2))) - (f2 . (x + (h / 2)))) - ((f1 - f2) . (x - (h / 2))) by A3, VALUED_1:13 .= ((f1 . (x + (h / 2))) - (f2 . (x + (h / 2)))) - ((f1 . (x - (h / 2))) - (f2 . (x - (h / 2)))) by A2, VALUED_1:13 .= ((f1 . (x + (h / 2))) - (f1 . (x - (h / 2)))) - ((f2 . (x + (h / 2))) - (f2 . (x - (h / 2)))) .= ((cD (f1,h)) . x) - ((f2 . (x + (h / 2))) - (f2 . (x - (h / 2)))) by Th5 .= ((cD (f1,h)) . x) - ((cD (f2,h)) . x) by Th5 .= ((cD (((cdif (f1,h)) . 0),h)) . x) - ((cD (f2,h)) . x) by Def8 .= ((cD (((cdif (f1,h)) . 0),h)) . x) - ((cD (((cdif (f2,h)) . 0),h)) . x) by Def8 .= (((cdif (f1,h)) . (0 + 1)) . x) - ((cD (((cdif (f2,h)) . 0),h)) . x) by Def8 .= (((cdif (f1,h)) . (0 + 1)) . x) - (((cdif (f2,h)) . (0 + 1)) . x) by Def8 ; hence ((cdif ((f1 - f2),h)) . (0 + 1)) . x = (((cdif (f1,h)) . (0 + 1)) . x) - (((cdif (f2,h)) . (0 + 1)) . x) ; ::_thesis: verum end; A4: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A5: for x being Real holds ((cdif ((f1 - f2),h)) . (k + 1)) . x = (((cdif (f1,h)) . (k + 1)) . x) - (((cdif (f2,h)) . (k + 1)) . x) ; ::_thesis: S1[k + 1] let x be Real; ::_thesis: ((cdif ((f1 - f2),h)) . ((k + 1) + 1)) . x = (((cdif (f1,h)) . ((k + 1) + 1)) . x) - (((cdif (f2,h)) . ((k + 1) + 1)) . x) A6: ( ((cdif ((f1 - f2),h)) . (k + 1)) . (x - (h / 2)) = (((cdif (f1,h)) . (k + 1)) . (x - (h / 2))) - (((cdif (f2,h)) . (k + 1)) . (x - (h / 2))) & ((cdif ((f1 - f2),h)) . (k + 1)) . (x + (h / 2)) = (((cdif (f1,h)) . (k + 1)) . (x + (h / 2))) - (((cdif (f2,h)) . (k + 1)) . (x + (h / 2))) ) by A5; A7: (cdif ((f1 - f2),h)) . (k + 1) is Function of REAL,REAL by Th19; A8: (cdif (f2,h)) . (k + 1) is Function of REAL,REAL by Th19; A9: (cdif (f1,h)) . (k + 1) is Function of REAL,REAL by Th19; ((cdif ((f1 - f2),h)) . ((k + 1) + 1)) . x = (cD (((cdif ((f1 - f2),h)) . (k + 1)),h)) . x by Def8 .= (((cdif ((f1 - f2),h)) . (k + 1)) . (x + (h / 2))) - (((cdif ((f1 - f2),h)) . (k + 1)) . (x - (h / 2))) by A7, Th5 .= ((((cdif (f1,h)) . (k + 1)) . (x + (h / 2))) - (((cdif (f1,h)) . (k + 1)) . (x - (h / 2)))) - ((((cdif (f2,h)) . (k + 1)) . (x + (h / 2))) - (((cdif (f2,h)) . (k + 1)) . (x - (h / 2)))) by A6 .= ((cD (((cdif (f1,h)) . (k + 1)),h)) . x) - ((((cdif (f2,h)) . (k + 1)) . (x + (h / 2))) - (((cdif (f2,h)) . (k + 1)) . (x - (h / 2)))) by A9, Th5 .= ((cD (((cdif (f1,h)) . (k + 1)),h)) . x) - ((cD (((cdif (f2,h)) . (k + 1)),h)) . x) by A8, Th5 .= (((cdif (f1,h)) . ((k + 1) + 1)) . x) - ((cD (((cdif (f2,h)) . (k + 1)),h)) . x) by Def8 .= (((cdif (f1,h)) . ((k + 1) + 1)) . x) - (((cdif (f2,h)) . ((k + 1) + 1)) . x) by Def8 ; hence ((cdif ((f1 - f2),h)) . ((k + 1) + 1)) . x = (((cdif (f1,h)) . ((k + 1) + 1)) . x) - (((cdif (f2,h)) . ((k + 1) + 1)) . x) ; ::_thesis: verum end; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A1, A4); hence ((cdif ((f1 - f2),h)) . (n + 1)) . x = (((cdif (f1,h)) . (n + 1)) . x) - (((cdif (f2,h)) . (n + 1)) . x) ; ::_thesis: verum end; theorem :: DIFF_1:24 for n being Element of NAT for r1, r2, h, x being Real for f1, f2 being Function of REAL,REAL holds ((cdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) . x = (r1 * (((cdif (f1,h)) . (n + 1)) . x)) + (r2 * (((cdif (f2,h)) . (n + 1)) . x)) proof let n be Element of NAT ; ::_thesis: for r1, r2, h, x being Real for f1, f2 being Function of REAL,REAL holds ((cdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) . x = (r1 * (((cdif (f1,h)) . (n + 1)) . x)) + (r2 * (((cdif (f2,h)) . (n + 1)) . x)) let r1, r2, h, x be Real; ::_thesis: for f1, f2 being Function of REAL,REAL holds ((cdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) . x = (r1 * (((cdif (f1,h)) . (n + 1)) . x)) + (r2 * (((cdif (f2,h)) . (n + 1)) . x)) let f1, f2 be Function of REAL,REAL; ::_thesis: ((cdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) . x = (r1 * (((cdif (f1,h)) . (n + 1)) . x)) + (r2 * (((cdif (f2,h)) . (n + 1)) . x)) set g1 = r1 (#) f1; set g2 = r2 (#) f2; ((cdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) . x = (((cdif ((r1 (#) f1),h)) . (n + 1)) . x) + (((cdif ((r2 (#) f2),h)) . (n + 1)) . x) by Th22 .= (r1 * (((cdif (f1,h)) . (n + 1)) . x)) + (((cdif ((r2 (#) f2),h)) . (n + 1)) . x) by Th21 .= (r1 * (((cdif (f1,h)) . (n + 1)) . x)) + (r2 * (((cdif (f2,h)) . (n + 1)) . x)) by Th21 ; hence ((cdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) . x = (r1 * (((cdif (f1,h)) . (n + 1)) . x)) + (r2 * (((cdif (f2,h)) . (n + 1)) . x)) ; ::_thesis: verum end; theorem :: DIFF_1:25 for h, x being Real for f being Function of REAL,REAL holds ((cdif (f,h)) . 1) . x = ((Shift (f,(h / 2))) . x) - ((Shift (f,(- (h / 2)))) . x) proof let h, x be Real; ::_thesis: for f being Function of REAL,REAL holds ((cdif (f,h)) . 1) . x = ((Shift (f,(h / 2))) . x) - ((Shift (f,(- (h / 2)))) . x) let f be Function of REAL,REAL; ::_thesis: ((cdif (f,h)) . 1) . x = ((Shift (f,(h / 2))) . x) - ((Shift (f,(- (h / 2)))) . x) set f2 = Shift (f,(- (h / 2))); set f1 = Shift (f,(h / 2)); ((cdif (f,h)) . 1) . x = ((cdif (f,h)) . (0 + 1)) . x .= (cD (((cdif (f,h)) . 0),h)) . x by Def8 .= (cD (f,h)) . x by Def8 .= (f . (x + (h / 2))) - (f . (x - (h / 2))) by Th5 .= ((Shift (f,(h / 2))) . x) - (f . (x + (- (h / 2)))) by Def2 .= ((Shift (f,(h / 2))) . x) - ((Shift (f,(- (h / 2)))) . x) by Def2 ; hence ((cdif (f,h)) . 1) . x = ((Shift (f,(h / 2))) . x) - ((Shift (f,(- (h / 2)))) . x) ; ::_thesis: verum end; theorem :: DIFF_1:26 for n being Element of NAT for h, x being Real for f being Function of REAL,REAL holds ((fdif (f,h)) . n) . x = ((bdif (f,h)) . n) . (x + (n * h)) proof let n be Element of NAT ; ::_thesis: for h, x being Real for f being Function of REAL,REAL holds ((fdif (f,h)) . n) . x = ((bdif (f,h)) . n) . (x + (n * h)) let h, x be Real; ::_thesis: for f being Function of REAL,REAL holds ((fdif (f,h)) . n) . x = ((bdif (f,h)) . n) . (x + (n * h)) let f be Function of REAL,REAL; ::_thesis: ((fdif (f,h)) . n) . x = ((bdif (f,h)) . n) . (x + (n * h)) defpred S1[ Nat] means for x being Real holds ((fdif (f,h)) . \$1) . x = ((bdif (f,h)) . \$1) . (x + (\$1 * h)); A1: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A2: for x being Real holds ((fdif (f,h)) . k) . x = ((bdif (f,h)) . k) . (x + (k * h)) ; ::_thesis: S1[k + 1] let x be Real; ::_thesis: ((fdif (f,h)) . (k + 1)) . x = ((bdif (f,h)) . (k + 1)) . (x + ((k + 1) * h)) A3: ((fdif (f,h)) . k) . (x + h) = ((bdif (f,h)) . k) . ((x + h) + (k * h)) by A2; A4: (fdif (f,h)) . k is Function of REAL,REAL by Th2; A5: (bdif (f,h)) . k is Function of REAL,REAL by Th12; ((fdif (f,h)) . (k + 1)) . x = (fD (((fdif (f,h)) . k),h)) . x by Def6 .= (((fdif (f,h)) . k) . (x + h)) - (((fdif (f,h)) . k) . x) by A4, Th3 .= (((bdif (f,h)) . k) . ((x + h) + (k * h))) - (((bdif (f,h)) . k) . (x + (k * h))) by A2, A3 .= (((bdif (f,h)) . k) . (x + ((k + 1) * h))) - (((bdif (f,h)) . k) . ((x + ((k + 1) * h)) - h)) .= (bD (((bdif (f,h)) . k),h)) . (x + ((k + 1) * h)) by A5, Th4 .= ((bdif (f,h)) . (k + 1)) . (x + ((k + 1) * h)) by Def7 ; hence ((fdif (f,h)) . (k + 1)) . x = ((bdif (f,h)) . (k + 1)) . (x + ((k + 1) * h)) ; ::_thesis: verum end; A6: S1[ 0 ] proof let x be Real; ::_thesis: ((fdif (f,h)) . 0) . x = ((bdif (f,h)) . 0) . (x + (0 * h)) ((fdif (f,h)) . 0) . x = f . x by Def6 .= ((bdif (f,h)) . 0) . (x + (0 * h)) by Def7 ; hence ((fdif (f,h)) . 0) . x = ((bdif (f,h)) . 0) . (x + (0 * h)) ; ::_thesis: verum end; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A6, A1); hence ((fdif (f,h)) . n) . x = ((bdif (f,h)) . n) . (x + (n * h)) ; ::_thesis: verum end; theorem :: DIFF_1:27 for n being Element of NAT for h, x being Real for f being Function of REAL,REAL holds ((fdif (f,h)) . (2 * n)) . x = ((cdif (f,h)) . (2 * n)) . (x + (n * h)) proof let n be Element of NAT ; ::_thesis: for h, x being Real for f being Function of REAL,REAL holds ((fdif (f,h)) . (2 * n)) . x = ((cdif (f,h)) . (2 * n)) . (x + (n * h)) let h, x be Real; ::_thesis: for f being Function of REAL,REAL holds ((fdif (f,h)) . (2 * n)) . x = ((cdif (f,h)) . (2 * n)) . (x + (n * h)) let f be Function of REAL,REAL; ::_thesis: ((fdif (f,h)) . (2 * n)) . x = ((cdif (f,h)) . (2 * n)) . (x + (n * h)) defpred S1[ Element of NAT ] means for x being Real holds ((fdif (f,h)) . (2 * \$1)) . x = ((cdif (f,h)) . (2 * \$1)) . (x + (\$1 * h)); A1: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A2: for x being Real holds ((fdif (f,h)) . (2 * k)) . x = ((cdif (f,h)) . (2 * k)) . (x + (k * h)) ; ::_thesis: S1[k + 1] let x be Real; ::_thesis: ((fdif (f,h)) . (2 * (k + 1))) . x = ((cdif (f,h)) . (2 * (k + 1))) . (x + ((k + 1) * h)) A3: ((fdif (f,h)) . (2 * k)) . ((x + h) + h) = ((cdif (f,h)) . (2 * k)) . (((x + h) + h) + (k * h)) by A2 .= ((cdif (f,h)) . (2 * k)) . (x + ((k + 2) * h)) ; A4: ((fdif (f,h)) . (2 * k)) . (x + h) = ((cdif (f,h)) . (2 * k)) . ((x + h) + (k * h)) by A2 .= ((cdif (f,h)) . (2 * k)) . (x + ((k + 1) * h)) ; set r3 = ((cdif (f,h)) . (2 * k)) . (x + (k * h)); set r2 = ((cdif (f,h)) . (2 * k)) . (x + ((k + 1) * h)); set r1 = ((cdif (f,h)) . (2 * k)) . (x + ((k + 2) * h)); A5: (fdif (f,h)) . ((2 * k) + 1) is Function of REAL,REAL by Th2; A6: (cdif (f,h)) . (2 * k) is Function of REAL,REAL by Th19; A7: (cdif (f,h)) . ((2 * k) + 1) is Function of REAL,REAL by Th19; A8: (fdif (f,h)) . (2 * k) is Function of REAL,REAL by Th2; A9: ((cdif (f,h)) . ((2 * k) + 1)) . ((x + ((k + 1) * h)) - (h / 2)) = (cD (((cdif (f,h)) . (2 * k)),h)) . ((x + ((k + 1) * h)) - (h / 2)) by Def8 .= (((cdif (f,h)) . (2 * k)) . (((x + ((k + 1) * h)) - (h / 2)) + (h / 2))) - (((cdif (f,h)) . (2 * k)) . (((x + ((k + 1) * h)) - (h / 2)) - (h / 2))) by A6, Th5 .= (((cdif (f,h)) . (2 * k)) . (x + ((k + 1) * h))) - (((cdif (f,h)) . (2 * k)) . (x + (k * h))) ; A10: ((cdif (f,h)) . ((2 * k) + 1)) . ((x + ((k + 1) * h)) + (h / 2)) = (cD (((cdif (f,h)) . (2 * k)),h)) . ((x + ((k + 1) * h)) + (h / 2)) by Def8 .= (((cdif (f,h)) . (2 * k)) . (((x + ((k + 1) * h)) + (h / 2)) + (h / 2))) - (((cdif (f,h)) . (2 * k)) . (((x + ((k + 1) * h)) + (h / 2)) - (h / 2))) by A6, Th5 .= (((cdif (f,h)) . (2 * k)) . (x + ((k + 2) * h))) - (((cdif (f,h)) . (2 * k)) . (x + ((k + 1) * h))) ; A11: ((cdif (f,h)) . (2 * (k + 1))) . (x + ((k + 1) * h)) = ((cdif (f,h)) . (((2 * k) + 1) + 1)) . (x + ((k + 1) * h)) .= (cD (((cdif (f,h)) . ((2 * k) + 1)),h)) . (x + ((k + 1) * h)) by Def8 .= ((((cdif (f,h)) . (2 * k)) . (x + ((k + 2) * h))) - (((cdif (f,h)) . (2 * k)) . (x + ((k + 1) * h)))) - ((((cdif (f,h)) . (2 * k)) . (x + ((k + 1) * h))) - (((cdif (f,h)) . (2 * k)) . (x + (k * h)))) by A7, A10, A9, Th5 ; ((fdif (f,h)) . (2 * (k + 1))) . x = ((fdif (f,h)) . (((2 * k) + 1) + 1)) . x .= (fD (((fdif (f,h)) . ((2 * k) + 1)),h)) . x by Def6 .= (((fdif (f,h)) . ((2 * k) + 1)) . (x + h)) - (((fdif (f,h)) . ((2 * k) + 1)) . x) by A5, Th3 .= ((fD (((fdif (f,h)) . (2 * k)),h)) . (x + h)) - (((fdif (f,h)) . ((2 * k) + 1)) . x) by Def6 .= ((fD (((fdif (f,h)) . (2 * k)),h)) . (x + h)) - ((fD (((fdif (f,h)) . (2 * k)),h)) . x) by Def6 .= ((((fdif (f,h)) . (2 * k)) . ((x + h) + h)) - (((fdif (f,h)) . (2 * k)) . (x + h))) - ((fD (((fdif (f,h)) . (2 * k)),h)) . x) by A8, Th3 .= ((((fdif (f,h)) . (2 * k)) . ((x + h) + h)) - (((fdif (f,h)) . (2 * k)) . (x + h))) - ((((fdif (f,h)) . (2 * k)) . (x + h)) - (((fdif (f,h)) . (2 * k)) . x)) by A8, Th3 .= ((((cdif (f,h)) . (2 * k)) . (x + ((k + 2) * h))) - (((cdif (f,h)) . (2 * k)) . (x + ((k + 1) * h)))) - ((((cdif (f,h)) . (2 * k)) . (x + ((k + 1) * h))) - (((cdif (f,h)) . (2 * k)) . (x + (k * h)))) by A2, A3, A4 ; hence ((fdif (f,h)) . (2 * (k + 1))) . x = ((cdif (f,h)) . (2 * (k + 1))) . (x + ((k + 1) * h)) by A11; ::_thesis: verum end; A12: S1[ 0 ] proof let x be Real; ::_thesis: ((fdif (f,h)) . (2 * 0)) . x = ((cdif (f,h)) . (2 * 0)) . (x + (0 * h)) ((fdif (f,h)) . (2 * 0)) . x = f . x by Def6 .= ((cdif (f,h)) . (2 * 0)) . (x + (0 * h)) by Def8 ; hence ((fdif (f,h)) . (2 * 0)) . x = ((cdif (f,h)) . (2 * 0)) . (x + (0 * h)) ; ::_thesis: verum end; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A12, A1); hence ((fdif (f,h)) . (2 * n)) . x = ((cdif (f,h)) . (2 * n)) . (x + (n * h)) ; ::_thesis: verum end; theorem :: DIFF_1:28 for n being Element of NAT for h, x being Real for f being Function of REAL,REAL holds ((fdif (f,h)) . ((2 * n) + 1)) . x = ((cdif (f,h)) . ((2 * n) + 1)) . ((x + (n * h)) + (h / 2)) proof let n be Element of NAT ; ::_thesis: for h, x being Real for f being Function of REAL,REAL holds ((fdif (f,h)) . ((2 * n) + 1)) . x = ((cdif (f,h)) . ((2 * n) + 1)) . ((x + (n * h)) + (h / 2)) let h, x be Real; ::_thesis: for f being Function of REAL,REAL holds ((fdif (f,h)) . ((2 * n) + 1)) . x = ((cdif (f,h)) . ((2 * n) + 1)) . ((x + (n * h)) + (h / 2)) let f be Function of REAL,REAL; ::_thesis: ((fdif (f,h)) . ((2 * n) + 1)) . x = ((cdif (f,h)) . ((2 * n) + 1)) . ((x + (n * h)) + (h / 2)) defpred S1[ Element of NAT ] means for x being Real holds ((fdif (f,h)) . ((2 * \$1) + 1)) . x = ((cdif (f,h)) . ((2 * \$1) + 1)) . ((x + (\$1 * h)) + (h / 2)); A1: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A2: for x being Real holds ((fdif (f,h)) . ((2 * k) + 1)) . x = ((cdif (f,h)) . ((2 * k) + 1)) . ((x + (k * h)) + (h / 2)) ; ::_thesis: S1[k + 1] let x be Real; ::_thesis: ((fdif (f,h)) . ((2 * (k + 1)) + 1)) . x = ((cdif (f,h)) . ((2 * (k + 1)) + 1)) . ((x + ((k + 1) * h)) + (h / 2)) A3: ((fdif (f,h)) . ((2 * k) + 1)) . ((x + h) + h) = ((cdif (f,h)) . ((2 * k) + 1)) . ((((x + h) + h) + (k * h)) + (h / 2)) by A2 .= ((cdif (f,h)) . ((2 * k) + 1)) . ((x + ((k + 2) * h)) + (h / 2)) ; A4: ((fdif (f,h)) . ((2 * k) + 1)) . (x + h) = ((cdif (f,h)) . ((2 * k) + 1)) . (((x + h) + (k * h)) + (h / 2)) by A2 .= ((cdif (f,h)) . ((2 * k) + 1)) . ((x + ((k + 1) * h)) + (h / 2)) ; set r3 = ((cdif (f,h)) . ((2 * k) + 1)) . ((x + (k * h)) + (h / 2)); set r2 = ((cdif (f,h)) . ((2 * k) + 1)) . ((x + ((k + 1) * h)) + (h / 2)); set r1 = ((cdif (f,h)) . ((2 * k) + 1)) . ((x + ((k + 2) * h)) + (h / 2)); A5: (fdif (f,h)) . (2 * (k + 1)) is Function of REAL,REAL by Th2; A6: (cdif (f,h)) . ((2 * k) + 1) is Function of REAL,REAL by Th19; A7: (cdif (f,h)) . (2 * (k + 1)) is Function of REAL,REAL by Th19; A8: (fdif (f,h)) . ((2 * k) + 1) is Function of REAL,REAL by Th2; A9: ((cdif (f,h)) . (2 * (k + 1))) . (x + ((k + 1) * h)) = ((cdif (f,h)) . (((2 * k) + 1) + 1)) . (x + ((k + 1) * h)) .= (cD (((cdif (f,h)) . ((2 * k) + 1)),h)) . (x + ((k + 1) * h)) by Def8 .= (((cdif (f,h)) . ((2 * k) + 1)) . ((x + ((k + 1) * h)) + (h / 2))) - (((cdif (f,h)) . ((2 * k) + 1)) . ((x + ((k + 1) * h)) - (h / 2))) by A6, Th5 .= (((cdif (f,h)) . ((2 * k) + 1)) . ((x + ((k + 1) * h)) + (h / 2))) - (((cdif (f,h)) . ((2 * k) + 1)) . ((x + (k * h)) + (h / 2))) ; A10: ((cdif (f,h)) . (2 * (k + 1))) . (x + ((k + 2) * h)) = ((cdif (f,h)) . (((2 * k) + 1) + 1)) . (x + ((k + 2) * h)) .= (cD (((cdif (f,h)) . ((2 * k) + 1)),h)) . (x + ((k + 2) * h)) by Def8 .= (((cdif (f,h)) . ((2 * k) + 1)) . ((x + ((k + 2) * h)) + (h / 2))) - (((cdif (f,h)) . ((2 * k) + 1)) . ((x + ((k + 2) * h)) - (h / 2))) by A6, Th5 .= (((cdif (f,h)) . ((2 * k) + 1)) . ((x + ((k + 2) * h)) + (h / 2))) - (((cdif (f,h)) . ((2 * k) + 1)) . ((x + ((k + 1) * h)) + (h / 2))) ; A11: ((cdif (f,h)) . ((2 * (k + 1)) + 1)) . ((x + ((k + 1) * h)) + (h / 2)) = (cD (((cdif (f,h)) . (2 * (k + 1))),h)) . ((x + ((k + 1) * h)) + (h / 2)) by Def8 .= (((cdif (f,h)) . (2 * (k + 1))) . (((x + ((k + 1) * h)) + (h / 2)) + (h / 2))) - (((cdif (f,h)) . (2 * (k + 1))) . (((x + ((k + 1) * h)) + (h / 2)) - (h / 2))) by A7, Th5 .= ((((cdif (f,h)) . ((2 * k) + 1)) . ((x + ((k + 2) * h)) + (h / 2))) - (((cdif (f,h)) . ((2 * k) + 1)) . ((x + ((k + 1) * h)) + (h / 2)))) - ((((cdif (f,h)) . ((2 * k) + 1)) . ((x + ((k + 1) * h)) + (h / 2))) - (((cdif (f,h)) . ((2 * k) + 1)) . ((x + (k * h)) + (h / 2)))) by A10, A9 ; ((fdif (f,h)) . ((2 * (k + 1)) + 1)) . x = (fD (((fdif (f,h)) . (2 * (k + 1))),h)) . x by Def6 .= (((fdif (f,h)) . (2 * (k + 1))) . (x + h)) - (((fdif (f,h)) . (2 * (k + 1))) . x) by A5, Th3 .= ((fD (((fdif (f,h)) . ((2 * k) + 1)),h)) . (x + h)) - (((fdif (f,h)) . (((2 * k) + 1) + 1)) . x) by Def6 .= ((fD (((fdif (f,h)) . ((2 * k) + 1)),h)) . (x + h)) - ((fD (((fdif (f,h)) . ((2 * k) + 1)),h)) . x) by Def6 .= ((((fdif (f,h)) . ((2 * k) + 1)) . ((x + h) + h)) - (((fdif (f,h)) . ((2 * k) + 1)) . (x + h))) - ((fD (((fdif (f,h)) . ((2 * k) + 1)),h)) . x) by A8, Th3 .= ((((fdif (f,h)) . ((2 * k) + 1)) . ((x + h) + h)) - (((fdif (f,h)) . ((2 * k) + 1)) . (x + h))) - ((((fdif (f,h)) . ((2 * k) + 1)) . (x + h)) - (((fdif (f,h)) . ((2 * k) + 1)) . x)) by A8, Th3 .= ((((cdif (f,h)) . ((2 * k) + 1)) . ((x + ((k + 2) * h)) + (h / 2))) - (((cdif (f,h)) . ((2 * k) + 1)) . ((x + ((k + 1) * h)) + (h / 2)))) - ((((cdif (f,h)) . ((2 * k) + 1)) . ((x + ((k + 1) * h)) + (h / 2))) - (((cdif (f,h)) . ((2 * k) + 1)) . ((x + (k * h)) + (h / 2)))) by A2, A3, A4 ; hence ((fdif (f,h)) . ((2 * (k + 1)) + 1)) . x = ((cdif (f,h)) . ((2 * (k + 1)) + 1)) . ((x + ((k + 1) * h)) + (h / 2)) by A11; ::_thesis: verum end; A12: S1[ 0 ] proof let x be Real; ::_thesis: ((fdif (f,h)) . ((2 * 0) + 1)) . x = ((cdif (f,h)) . ((2 * 0) + 1)) . ((x + (0 * h)) + (h / 2)) ((fdif (f,h)) . ((2 * 0) + 1)) . x = (fD (((fdif (f,h)) . 0),h)) . x by Def6 .= (fD (f,h)) . x by Def6 .= (f . (x + h)) - (f . x) by Th3 .= (f . ((x + (h / 2)) + (h / 2))) - (f . ((x + (h / 2)) - (h / 2))) .= (cD (f,h)) . (x + (h / 2)) by Th5 .= (cD (((cdif (f,h)) . 0),h)) . (x + (h / 2)) by Def8 .= ((cdif (f,h)) . ((2 * 0) + 1)) . ((x + (0 * h)) + (h / 2)) by Def8 ; hence ((fdif (f,h)) . ((2 * 0) + 1)) . x = ((cdif (f,h)) . ((2 * 0) + 1)) . ((x + (0 * h)) + (h / 2)) ; ::_thesis: verum end; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A12, A1); hence ((fdif (f,h)) . ((2 * n) + 1)) . x = ((cdif (f,h)) . ((2 * n) + 1)) . ((x + (n * h)) + (h / 2)) ; ::_thesis: verum end; definition let f be real-valued Function; let x0, x1 be real number ; func[!f,x0,x1!] -> Real equals :: DIFF_1:def 9 ((f . x0) - (f . x1)) / (x0 - x1); correctness coherence ((f . x0) - (f . x1)) / (x0 - x1) is Real; ; end; :: deftheorem defines [! DIFF_1:def_9_:_ for f being real-valued Function for x0, x1 being real number holds [!f,x0,x1!] = ((f . x0) - (f . x1)) / (x0 - x1); definition let f be real-valued Function; let x0, x1, x2 be real number ; func[!f,x0,x1,x2!] -> Real equals :: DIFF_1:def 10 ([!f,x0,x1!] - [!f,x1,x2!]) / (x0 - x2); correctness coherence ([!f,x0,x1!] - [!f,x1,x2!]) / (x0 - x2) is Real; ; end; :: deftheorem defines [! DIFF_1:def_10_:_ for f being real-valued Function for x0, x1, x2 being real number holds [!f,x0,x1,x2!] = ([!f,x0,x1!] - [!f,x1,x2!]) / (x0 - x2); definition let f be real-valued Function; let x0, x1, x2, x3 be real number ; func[!f,x0,x1,x2,x3!] -> Real equals :: DIFF_1:def 11 ([!f,x0,x1,x2!] - [!f,x1,x2,x3!]) / (x0 - x3); correctness coherence ([!f,x0,x1,x2!] - [!f,x1,x2,x3!]) / (x0 - x3) is Real; ; end; :: deftheorem defines [! DIFF_1:def_11_:_ for f being real-valued Function for x0, x1, x2, x3 being real number holds [!f,x0,x1,x2,x3!] = ([!f,x0,x1,x2!] - [!f,x1,x2,x3!]) / (x0 - x3); theorem :: DIFF_1:29 for x0, x1 being Real for f being Function of REAL,REAL holds [!f,x0,x1!] = [!f,x1,x0!] proof let x0, x1 be Real; ::_thesis: for f being Function of REAL,REAL holds [!f,x0,x1!] = [!f,x1,x0!] let f be Function of REAL,REAL; ::_thesis: [!f,x0,x1!] = [!f,x1,x0!] thus [!f,x0,x1!] = (- ((f . x1) - (f . x0))) / (- (x1 - x0)) .= [!f,x1,x0!] by XCMPLX_1:191 ; ::_thesis: verum end; theorem :: DIFF_1:30 for x0, x1 being Real for f being Function of REAL,REAL st f is constant holds [!f,x0,x1!] = 0 proof let x0, x1 be Real; ::_thesis: for f being Function of REAL,REAL st f is constant holds [!f,x0,x1!] = 0 let f be Function of REAL,REAL; ::_thesis: ( f is constant implies [!f,x0,x1!] = 0 ) x0 in REAL ; then A1: x0 in dom f by FUNCT_2:def_1; x1 in REAL ; then A2: x1 in dom f by FUNCT_2:def_1; assume f is constant ; ::_thesis: [!f,x0,x1!] = 0 then f . x0 = f . x1 by A1, A2, FUNCT_1:def_10; hence [!f,x0,x1!] = 0 ; ::_thesis: verum end; theorem Th31: :: DIFF_1:31 for r, x0, x1 being Real for f being Function of REAL,REAL holds [!(r (#) f),x0,x1!] = r * [!f,x0,x1!] proof let r, x0, x1 be Real; ::_thesis: for f being Function of REAL,REAL holds [!(r (#) f),x0,x1!] = r * [!f,x0,x1!] let f be Function of REAL,REAL; ::_thesis: [!(r (#) f),x0,x1!] = r * [!f,x0,x1!] x1 in REAL ; then A1: x1 in dom (r (#) f) by FUNCT_2:def_1; x0 in REAL ; then x0 in dom (r (#) f) by FUNCT_2:def_1; then [!(r (#) f),x0,x1!] = ((r * (f . x0)) - ((r (#) f) . x1)) / (x0 - x1) by VALUED_1:def_5 .= ((r * (f . x0)) - (r * (f . x1))) / (x0 - x1) by A1, VALUED_1:def_5 .= (r * ((f . x0) - (f . x1))) / (x0 - x1) .= r * [!f,x0,x1!] by XCMPLX_1:74 ; hence [!(r (#) f),x0,x1!] = r * [!f,x0,x1!] ; ::_thesis: verum end; theorem Th32: :: DIFF_1:32 for x0, x1 being Real for f1, f2 being Function of REAL,REAL holds [!(f1 + f2),x0,x1!] = [!f1,x0,x1!] + [!f2,x0,x1!] proof let x0, x1 be Real; ::_thesis: for f1, f2 being Function of REAL,REAL holds [!(f1 + f2),x0,x1!] = [!f1,x0,x1!] + [!f2,x0,x1!] let f1, f2 be Function of REAL,REAL; ::_thesis: [!(f1 + f2),x0,x1!] = [!f1,x0,x1!] + [!f2,x0,x1!] [!(f1 + f2),x0,x1!] = (((f1 . x0) + (f2 . x0)) - ((f1 + f2) . x1)) / (x0 - x1) by VALUED_1:1 .= (((f1 . x0) + (f2 . x0)) - ((f1 . x1) + (f2 . x1))) / (x0 - x1) by VALUED_1:1 .= (((f1 . x0) - (f1 . x1)) + ((f2 . x0) - (f2 . x1))) / (x0 - x1) .= [!f1,x0,x1!] + [!f2,x0,x1!] by XCMPLX_1:62 ; hence [!(f1 + f2),x0,x1!] = [!f1,x0,x1!] + [!f2,x0,x1!] ; ::_thesis: verum end; theorem :: DIFF_1:33 for r1, r2, x0, x1 being Real for f1, f2 being Function of REAL,REAL holds [!((r1 (#) f1) + (r2 (#) f2)),x0,x1!] = (r1 * [!f1,x0,x1!]) + (r2 * [!f2,x0,x1!]) proof let r1, r2, x0, x1 be Real; ::_thesis: for f1, f2 being Function of REAL,REAL holds [!((r1 (#) f1) + (r2 (#) f2)),x0,x1!] = (r1 * [!f1,x0,x1!]) + (r2 * [!f2,x0,x1!]) let f1, f2 be Function of REAL,REAL; ::_thesis: [!((r1 (#) f1) + (r2 (#) f2)),x0,x1!] = (r1 * [!f1,x0,x1!]) + (r2 * [!f2,x0,x1!]) [!((r1 (#) f1) + (r2 (#) f2)),x0,x1!] = [!(r1 (#) f1),x0,x1!] + [!(r2 (#) f2),x0,x1!] by Th32 .= (r1 * [!f1,x0,x1!]) + [!(r2 (#) f2),x0,x1!] by Th31 .= (r1 * [!f1,x0,x1!]) + (r2 * [!f2,x0,x1!]) by Th31 ; hence [!((r1 (#) f1) + (r2 (#) f2)),x0,x1!] = (r1 * [!f1,x0,x1!]) + (r2 * [!f2,x0,x1!]) ; ::_thesis: verum end; theorem Th34: :: DIFF_1:34 for x0, x1, x2 being Real for f being Function of REAL,REAL st x0,x1,x2 are_mutually_different holds ( [!f,x0,x1,x2!] = [!f,x1,x2,x0!] & [!f,x0,x1,x2!] = [!f,x2,x1,x0!] ) proof let x0, x1, x2 be Real; ::_thesis: for f being Function of REAL,REAL st x0,x1,x2 are_mutually_different holds ( [!f,x0,x1,x2!] = [!f,x1,x2,x0!] & [!f,x0,x1,x2!] = [!f,x2,x1,x0!] ) let f be Function of REAL,REAL; ::_thesis: ( x0,x1,x2 are_mutually_different implies ( [!f,x0,x1,x2!] = [!f,x1,x2,x0!] & [!f,x0,x1,x2!] = [!f,x2,x1,x0!] ) ) set x10 = x1 - x0; set x20 = x2 - x0; set x12 = x1 - x2; assume A1: x0,x1,x2 are_mutually_different ; ::_thesis: ( [!f,x0,x1,x2!] = [!f,x1,x2,x0!] & [!f,x0,x1,x2!] = [!f,x2,x1,x0!] ) then A2: x1 - x2 <> 0 by ZFMISC_1:def_5; A3: x1 - x0 <> 0 by A1, ZFMISC_1:def_5; A4: [!f,x0,x1,x2!] = ((((f . x0) - (f . x1)) / (- (x1 - x0))) - (((f . x1) - (f . x2)) / (x1 - x2))) / (- (x2 - x0)) .= ((- (((f . x0) - (f . x1)) / (x1 - x0))) - (((f . x1) - (f . x2)) / (x1 - x2))) / (- (x2 - x0)) by XCMPLX_1:188 .= (- ((((f . x0) - (f . x1)) / (x1 - x0)) + (((f . x1) - (f . x2)) / (x1 - x2)))) / (- (x2 - x0)) .= ((((f . x0) - (f . x1)) / (x1 - x0)) + (((f . x1) - (f . x2)) / (x1 - x2))) / (x2 - x0) by XCMPLX_1:191 .= (((((f . x0) - (f . x1)) * (x1 - x2)) + (((f . x1) - (f . x2)) * (x1 - x0))) / ((x1 - x0) * (x1 - x2))) / (x2 - x0) by A2, A3, XCMPLX_1:116 .= ((((f . x0) * (x1 - x2)) + ((f . x1) * (x2 - x0))) - ((f . x2) * (x1 - x0))) / (((x1 - x0) * (x1 - x2)) * (x2 - x0)) by XCMPLX_1:78 ; A5: [!f,x2,x1,x0!] = (((- ((f . x1) - (f . x2))) / (- (x1 - x2))) - (((f . x1) - (f . x0)) / (x1 - x0))) / (x2 - x0) .= ((((f . x1) - (f . x2)) / (x1 - x2)) - (((f . x1) - (f . x0)) / (x1 - x0))) / (x2 - x0) by XCMPLX_1:191 .= (((((f . x1) - (f . x2)) * (x1 - x0)) - (((f . x1) - (f . x0)) * (x1 - x2))) / ((x1 - x2) * (x1 - x0))) / (x2 - x0) by A2, A3, XCMPLX_1:130 .= [!f,x0,x1,x2!] by A4, XCMPLX_1:78 ; x2 - x0 <> 0 by A1, ZFMISC_1:def_5; then [!f,x1,x2,x0!] = (((((f . x1) - (f . x2)) * (x2 - x0)) - (((f . x2) - (f . x0)) * (x1 - x2))) / ((x1 - x2) * (x2 - x0))) / (x1 - x0) by A2, XCMPLX_1:130 .= ((((f . x0) * (x1 - x2)) + ((f . x1) * (x2 - x0))) - ((f . x2) * (x1 - x0))) / (((x1 - x2) * (x2 - x0)) * (x1 - x0)) by XCMPLX_1:78 .= [!f,x0,x1,x2!] by A4 ; hence ( [!f,x0,x1,x2!] = [!f,x1,x2,x0!] & [!f,x0,x1,x2!] = [!f,x2,x1,x0!] ) by A5; ::_thesis: verum end; theorem :: DIFF_1:35 for x0, x1, x2 being Real for f being Function of REAL,REAL st x0,x1,x2 are_mutually_different holds ( [!f,x0,x1,x2!] = [!f,x2,x0,x1!] & [!f,x0,x1,x2!] = [!f,x1,x0,x2!] ) proof let x0, x1, x2 be Real; ::_thesis: for f being Function of REAL,REAL st x0,x1,x2 are_mutually_different holds ( [!f,x0,x1,x2!] = [!f,x2,x0,x1!] & [!f,x0,x1,x2!] = [!f,x1,x0,x2!] ) let f be Function of REAL,REAL; ::_thesis: ( x0,x1,x2 are_mutually_different implies ( [!f,x0,x1,x2!] = [!f,x2,x0,x1!] & [!f,x0,x1,x2!] = [!f,x1,x0,x2!] ) ) assume A1: x0,x1,x2 are_mutually_different ; ::_thesis: ( [!f,x0,x1,x2!] = [!f,x2,x0,x1!] & [!f,x0,x1,x2!] = [!f,x1,x0,x2!] ) then A2: x1 <> x2 by ZFMISC_1:def_5; ( x0 <> x1 & x0 <> x2 ) by A1, ZFMISC_1:def_5; then A3: x2,x0,x1 are_mutually_different by A2, ZFMISC_1:def_5; then [!f,x0,x1,x2!] = [!f,x2,x0,x1!] by Th34; hence ( [!f,x0,x1,x2!] = [!f,x2,x0,x1!] & [!f,x0,x1,x2!] = [!f,x1,x0,x2!] ) by A3, Th34; ::_thesis: verum end; theorem :: DIFF_1:36 for m, n being Element of NAT for h, x being Real for f being Function of REAL,REAL holds ((fdif (((fdif (f,h)) . m),h)) . n) . x = ((fdif (f,h)) . (m + n)) . x proof let m, n be Element of NAT ; ::_thesis: for h, x being Real for f being Function of REAL,REAL holds ((fdif (((fdif (f,h)) . m),h)) . n) . x = ((fdif (f,h)) . (m + n)) . x let h, x be Real; ::_thesis: for f being Function of REAL,REAL holds ((fdif (((fdif (f,h)) . m),h)) . n) . x = ((fdif (f,h)) . (m + n)) . x let f be Function of REAL,REAL; ::_thesis: ((fdif (((fdif (f,h)) . m),h)) . n) . x = ((fdif (f,h)) . (m + n)) . x defpred S1[ Element of NAT ] means for x being Real holds ((fdif (((fdif (f,h)) . m),h)) . \$1) . x = ((fdif (f,h)) . (m + \$1)) . x; A1: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A2: for x being Real holds ((fdif (((fdif (f,h)) . m),h)) . k) . x = ((fdif (f,h)) . (m + k)) . x ; ::_thesis: S1[k + 1] let x be Real; ::_thesis: ((fdif (((fdif (f,h)) . m),h)) . (k + 1)) . x = ((fdif (f,h)) . (m + (k + 1))) . x A3: (fdif (f,h)) . (m + k) is Function of REAL,REAL by Th2; (fdif (f,h)) . m is Function of REAL,REAL by Th2; then A4: (fdif (((fdif (f,h)) . m),h)) . k is Function of REAL,REAL by Th2; ((fdif (((fdif (f,h)) . m),h)) . (k + 1)) . x = (fD (((fdif (((fdif (f,h)) . m),h)) . k),h)) . x by Def6 .= (((fdif (((fdif (f,h)) . m),h)) . k) . (x + h)) - (((fdif (((fdif (f,h)) . m),h)) . k) . x) by A4, Th3 .= (((fdif (f,h)) . (m + k)) . (x + h)) - (((fdif (((fdif (f,h)) . m),h)) . k) . x) by A2 .= (((fdif (f,h)) . (m + k)) . (x + h)) - (((fdif (f,h)) . (m + k)) . x) by A2 .= (fD (((fdif (f,h)) . (m + k)),h)) . x by A3, Th3 .= ((fdif (f,h)) . ((m + k) + 1)) . x by Def6 ; hence ((fdif (((fdif (f,h)) . m),h)) . (k + 1)) . x = ((fdif (f,h)) . (m + (k + 1))) . x ; ::_thesis: verum end; A5: S1[ 0 ] by Def6; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A5, A1); hence ((fdif (((fdif (f,h)) . m),h)) . n) . x = ((fdif (f,h)) . (m + n)) . x ; ::_thesis: verum end; definition let S be Functional_Sequence of REAL,REAL; attrS is Sequence-yielding means :Def12: :: DIFF_1:def 12 for n being Element of NAT holds S . n is Real_Sequence; end; :: deftheorem Def12 defines Sequence-yielding DIFF_1:def_12_:_ for S being Functional_Sequence of REAL,REAL holds ( S is Sequence-yielding iff for n being Element of NAT holds S . n is Real_Sequence ); Lm1: ex S being Functional_Sequence of REAL,REAL st for n being Element of NAT holds S . n is Real_Sequence proof set s1 = NAT --> 1; set S = NAT --> (NAT --> 1); NAT --> 1 is PartFunc of REAL,REAL by RELSET_1:7; then ( dom (NAT --> (NAT --> 1)) = NAT & ( for n being Element of NAT holds (NAT --> (NAT --> 1)) . n is PartFunc of REAL,REAL ) ) by FUNCOP_1:7, FUNCOP_1:13; then reconsider S = NAT --> (NAT --> 1) as Functional_Sequence of REAL,REAL by SEQFUNC:1; ( dom (NAT --> 1) = NAT & ( for n being Element of NAT holds (NAT --> 1) . n is real ) ) by FUNCOP_1:13; then NAT --> 1 is Real_Sequence by SEQ_1:2; then for n being Element of NAT holds S . n is Real_Sequence by FUNCOP_1:7; hence ex S being Functional_Sequence of REAL,REAL st for n being Element of NAT holds S . n is Real_Sequence ; ::_thesis: verum end; registration cluster non empty V13() V16( NAT ) V17( PFuncs (REAL,REAL)) Function-like total quasi_total Sequence-yielding for Element of bool [:NAT,(PFuncs (REAL,REAL)):]; existence ex b1 being Functional_Sequence of REAL,REAL st b1 is Sequence-yielding proof consider S being Functional_Sequence of REAL,REAL such that A1: for n being Element of NAT holds S . n is Real_Sequence by Lm1; take S ; ::_thesis: S is Sequence-yielding thus S is Sequence-yielding by A1, Def12; ::_thesis: verum end; end; definition mode Seq_Sequence is Sequence-yielding Functional_Sequence of REAL,REAL; end; definition let S be Seq_Sequence; let n be Element of NAT ; :: original: . redefine funcS . n -> Real_Sequence; coherence S . n is Real_Sequence by Def12; end; Lm2: for h, x being Real for f1, f2 being Function of REAL,REAL holds ((fdif ((f1 (#) f2),h)) . 1) . x = ((f1 . x) * (((fdif (f2,h)) . 1) . x)) + ((((fdif (f1,h)) . 1) . x) * (f2 . (x + h))) proof let h, x be Real; ::_thesis: for f1, f2 being Function of REAL,REAL holds ((fdif ((f1 (#) f2),h)) . 1) . x = ((f1 . x) * (((fdif (f2,h)) . 1) . x)) + ((((fdif (f1,h)) . 1) . x) * (f2 . (x + h))) let f1, f2 be Function of REAL,REAL; ::_thesis: ((fdif ((f1 (#) f2),h)) . 1) . x = ((f1 . x) * (((fdif (f2,h)) . 1) . x)) + ((((fdif (f1,h)) . 1) . x) * (f2 . (x + h))) ((fdif ((f1 (#) f2),h)) . 1) . x = ((fdif ((f1 (#) f2),h)) . (0 + 1)) . x .= (fD (((fdif ((f1 (#) f2),h)) . 0),h)) . x by Def6 .= (fD ((f1 (#) f2),h)) . x by Def6 .= ((f1 (#) f2) . (x + h)) - ((f1 (#) f2) . x) by Th3 .= ((f1 . (x + h)) * (f2 . (x + h))) - ((f1 (#) f2) . x) by VALUED_1:5 .= ((f1 . (x + h)) * (f2 . (x + h))) - ((f1 . x) * (f2 . x)) by VALUED_1:5 .= ((f1 . x) * ((f2 . (x + h)) - (f2 . x))) + (((f1 . (x + h)) - (f1 . x)) * (f2 . (x + h))) .= ((f1 . x) * ((fD (f2,h)) . x)) + (((f1 . (x + h)) - (f1 . x)) * (f2 . (x + h))) by Th3 .= ((f1 . x) * ((fD (f2,h)) . x)) + (((fD (f1,h)) . x) * (f2 . (x + h))) by Th3 .= ((f1 . x) * ((fD (((fdif (f2,h)) . 0),h)) . x)) + (((fD (f1,h)) . x) * (f2 . (x + h))) by Def6 .= ((f1 . x) * ((fD (((fdif (f2,h)) . 0),h)) . x)) + (((fD (((fdif (f1,h)) . 0),h)) . x) * (f2 . (x + h))) by Def6 .= ((f1 . x) * (((fdif (f2,h)) . (0 + 1)) . x)) + (((fD (((fdif (f1,h)) . 0),h)) . x) * (f2 . (x + h))) by Def6 .= ((f1 . x) * (((fdif (f2,h)) . 1) . x)) + ((((fdif (f1,h)) . 1) . x) * (f2 . (x + h))) by Def6 ; hence ((fdif ((f1 (#) f2),h)) . 1) . x = ((f1 . x) * (((fdif (f2,h)) . 1) . x)) + ((((fdif (f1,h)) . 1) . x) * (f2 . (x + h))) ; ::_thesis: verum end; theorem :: DIFF_1:37 for h, x being Real for f1, f2 being Function of REAL,REAL for S being Seq_Sequence st ( for n, i being Element of NAT st i <= n holds (S . n) . i = ((n choose i) * (((fdif (f1,h)) . i) . x)) * (((fdif (f2,h)) . (n -' i)) . (x + (i * h))) ) holds ( ((fdif ((f1 (#) f2),h)) . 1) . x = Sum ((S . 1),1) & ((fdif ((f1 (#) f2),h)) . 2) . x = Sum ((S . 2),2) ) proof let h, x be Real; ::_thesis: for f1, f2 being Function of REAL,REAL for S being Seq_Sequence st ( for n, i being Element of NAT st i <= n holds (S . n) . i = ((n choose i) * (((fdif (f1,h)) . i) . x)) * (((fdif (f2,h)) . (n -' i)) . (x + (i * h))) ) holds ( ((fdif ((f1 (#) f2),h)) . 1) . x = Sum ((S . 1),1) & ((fdif ((f1 (#) f2),h)) . 2) . x = Sum ((S . 2),2) ) let f1, f2 be Function of REAL,REAL; ::_thesis: for S being Seq_Sequence st ( for n, i being Element of NAT st i <= n holds (S . n) . i = ((n choose i) * (((fdif (f1,h)) . i) . x)) * (((fdif (f2,h)) . (n -' i)) . (x + (i * h))) ) holds ( ((fdif ((f1 (#) f2),h)) . 1) . x = Sum ((S . 1),1) & ((fdif ((f1 (#) f2),h)) . 2) . x = Sum ((S . 2),2) ) let S be Seq_Sequence; ::_thesis: ( ( for n, i being Element of NAT st i <= n holds (S . n) . i = ((n choose i) * (((fdif (f1,h)) . i) . x)) * (((fdif (f2,h)) . (n -' i)) . (x + (i * h))) ) implies ( ((fdif ((f1 (#) f2),h)) . 1) . x = Sum ((S . 1),1) & ((fdif ((f1 (#) f2),h)) . 2) . x = Sum ((S . 2),2) ) ) A1: 1 -' 0 = 1 - 0 by XREAL_1:233 .= 1 ; A2: 1 -' 1 = 1 - 1 by XREAL_1:233 .= 0 ; A3: (fdif ((f1 (#) f2),h)) . 1 is Function of REAL,REAL by Th2; A4: 2 -' 1 = 2 - 1 by XREAL_1:233 .= 1 ; A5: (fdif (f2,h)) . 1 is Function of REAL,REAL by Th2; A6: 2 -' 2 = 2 - 2 by XREAL_1:233 .= 0 ; assume A7: for n, i being Element of NAT st i <= n holds (S . n) . i = ((n choose i) * (((fdif (f1,h)) . i) . x)) * (((fdif (f2,h)) . (n -' i)) . (x + (i * h))) ; ::_thesis: ( ((fdif ((f1 (#) f2),h)) . 1) . x = Sum ((S . 1),1) & ((fdif ((f1 (#) f2),h)) . 2) . x = Sum ((S . 2),2) ) then A8: (S . 2) . 1 = ((2 choose 1) * (((fdif (f1,h)) . 1) . x)) * (((fdif (f2,h)) . (2 -' 1)) . (x + (1 * h))) .= (2 * (((fdif (f1,h)) . 1) . x)) * (((fdif (f2,h)) . 1) . (x + h)) by A4, NEWTON:23 ; A9: (S . 1) . 1 = ((1 choose 1) * (((fdif (f1,h)) . 1) . x)) * (((fdif (f2,h)) . (1 -' 1)) . (x + (1 * h))) by A7 .= (1 * (((fdif (f1,h)) . 1) . x)) * (((fdif (f2,h)) . (1 -' 1)) . (x + (1 * h))) by NEWTON:21 .= (((fdif (f1,h)) . 1) . x) * (f2 . (x + h)) by A2, Def6 ; A10: (S . 1) . 0 = ((1 choose 0) * (((fdif (f1,h)) . 0) . x)) * (((fdif (f2,h)) . (1 -' 0)) . (x + (0 * h))) by A7 .= (1 * (((fdif (f1,h)) . 0) . x)) * (((fdif (f2,h)) . (1 -' 0)) . (x + (0 * h))) by NEWTON:19 .= (f1 . x) * (((fdif (f2,h)) . 1) . x) by A1, Def6 ; A11: Sum ((S . 1),1) = (Partial_Sums (S . 1)) . (0 + 1) by SERIES_1:def_5 .= ((Partial_Sums (S . 1)) . 0) + ((S . 1) . 1) by SERIES_1:def_1 .= ((S . 1) . 0) + ((S . 1) . 1) by SERIES_1:def_1 .= ((fdif ((f1 (#) f2),h)) . 1) . x by A10, A9, Lm2 ; A12: (fdif (f1,h)) . 1 is Function of REAL,REAL by Th2; A13: ((fdif ((f1 (#) f2),h)) . 2) . x = ((fdif ((f1 (#) f2),h)) . (1 + 1)) . x .= (fD (((fdif ((f1 (#) f2),h)) . 1),h)) . x by Def6 .= (((fdif ((f1 (#) f2),h)) . 1) . (x + h)) - (((fdif ((f1 (#) f2),h)) . 1) . x) by A3, Th3 .= (((f1 . (x + h)) * (((fdif (f2,h)) . 1) . (x + h))) + ((((fdif (f1,h)) . 1) . (x + h)) * (f2 . ((x + h) + h)))) - (((fdif ((f1 (#) f2),h)) . 1) . x) by Lm2 .= (((f1 . (x + h)) * (((fdif (f2,h)) . 1) . (x + h))) + ((((fdif (f1,h)) . 1) . (x + h)) * (f2 . ((x + h) + h)))) - (((f1 . x) * (((fdif (f2,h)) . 1) . x)) + ((((fdif (f1,h)) . 1) . x) * (f2 . (x + h)))) by Lm2 .= ((((f1 . x) * ((((fdif (f2,h)) . 1) . (x + h)) - (((fdif (f2,h)) . 1) . x))) + (((f1 . (x + h)) - (f1 . x)) * (((fdif (f2,h)) . 1) . (x + h)))) + (((((fdif (f1,h)) . 1) . (x + h)) - (((fdif (f1,h)) . 1) . x)) * (f2 . ((x + h) + h)))) + ((((fdif (f1,h)) . 1) . x) * ((f2 . ((x + h) + h)) - (f2 . (x + h)))) .= ((((f1 . x) * ((fD (((fdif (f2,h)) . 1),h)) . x)) + (((f1 . (x + h)) - (f1 . x)) * (((fdif (f2,h)) . 1) . (x + h)))) + (((((fdif (f1,h)) . 1) . (x + h)) - (((fdif (f1,h)) . 1) . x)) * (f2 . ((x + h) + h)))) + ((((fdif (f1,h)) . 1) . x) * ((f2 . ((x + h) + h)) - (f2 . (x + h)))) by A5, Th3 .= ((((f1 . x) * ((fD (((fdif (f2,h)) . 1),h)) . x)) + (((fD (f1,h)) . x) * (((fdif (f2,h)) . 1) . (x + h)))) + (((((fdif (f1,h)) . 1) . (x + h)) - (((fdif (f1,h)) . 1) . x)) * (f2 . ((x + h) + h)))) + ((((fdif (f1,h)) . 1) . x) * ((f2 . ((x + h) + h)) - (f2 . (x + h)))) by Th3 .= ((((f1 . x) * ((fD (((fdif (f2,h)) . 1),h)) . x)) + (((fD (f1,h)) . x) * (((fdif (f2,h)) . 1) . (x + h)))) + (((fD (((fdif (f1,h)) . 1),h)) . x) * (f2 . ((x + h) + h)))) + ((((fdif (f1,h)) . 1) . x) * ((f2 . ((x + h) + h)) - (f2 . (x + h)))) by A12, Th3 .= ((((f1 . x) * ((fD (((fdif (f2,h)) . 1),h)) . x)) + (((fD (f1,h)) . x) * (((fdif (f2,h)) . 1) . (x + h)))) + (((fD (((fdif (f1,h)) . 1),h)) . x) * (f2 . ((x + h) + h)))) + ((((fdif (f1,h)) . 1) . x) * ((fD (f2,h)) . (x + h))) by Th3 .= ((((f1 . x) * (((fdif (f2,h)) . (1 + 1)) . x)) + (((fD (f1,h)) . x) * (((fdif (f2,h)) . 1) . (x + h)))) + (((fD (((fdif (f1,h)) . 1),h)) . x) * (f2 . ((x + h) + h)))) + ((((fdif (f1,h)) . 1) . x) * ((fD (f2,h)) . (x + h))) by Def6 .= ((((f1 . x) * (((fdif (f2,h)) . (1 + 1)) . x)) + (((fD (((fdif (f1,h)) . 0),h)) . x) * (((fdif (f2,h)) . 1) . (x + h)))) + (((fD (((fdif (f1,h)) . 1),h)) . x) * (f2 . ((x + h) + h)))) + ((((fdif (f1,h)) . 1) . x) * ((fD (f2,h)) . (x + h))) by Def6 .= ((((f1 . x) * (((fdif (f2,h)) . 2) . x)) + (((fD (((fdif (f1,h)) . 0),h)) . x) * (((fdif (f2,h)) . 1) . (x + h)))) + ((((fdif (f1,h)) . 2) . x) * (f2 . (x + (2 * h))))) + ((((fdif (f1,h)) . 1) . x) * ((fD (f2,h)) . (x + h))) by Def6 .= ((((f1 . x) * (((fdif (f2,h)) . 2) . x)) + ((((fdif (f1,h)) . (0 + 1)) . x) * (((fdif (f2,h)) . 1) . (x + h)))) + ((((fdif (f1,h)) . 2) . x) * (f2 . (x + (2 * h))))) + ((((fdif (f1,h)) . 1) . x) * ((fD (f2,h)) . (x + h))) by Def6 .= ((((f1 . x) * (((fdif (f2,h)) . 2) . x)) + ((((fdif (f1,h)) . 1) . x) * (((fdif (f2,h)) . 1) . (x + h)))) + ((((fdif (f1,h)) . 2) . x) * (f2 . (x + (2 * h))))) + ((((fdif (f1,h)) . 1) . x) * ((fD (((fdif (f2,h)) . 0),h)) . (x + h))) by Def6 .= ((((f1 . x) * (((fdif (f2,h)) . 2) . x)) + ((((fdif (f1,h)) . 1) . x) * (((fdif (f2,h)) . 1) . (x + h)))) + ((((fdif (f1,h)) . 2) . x) * (f2 . (x + (2 * h))))) + ((((fdif (f1,h)) . 1) . x) * (((fdif (f2,h)) . (0 + 1)) . (x + h))) by Def6 .= (((f1 . x) * (((fdif (f2,h)) . 2) . x)) + (2 * ((((fdif (f1,h)) . 1) . x) * (((fdif (f2,h)) . 1) . (x + h))))) + ((((fdif (f1,h)) . 2) . x) * (f2 . (x + (2 * h)))) ; A14: 2 -' 0 = 2 - 0 by XREAL_1:233 .= 2 ; A15: (S . 2) . 2 = ((2 choose 2) * (((fdif (f1,h)) . 2) . x)) * (((fdif (f2,h)) . (2 -' 2)) . (x + (2 * h))) by A7 .= (1 * (((fdif (f1,h)) . 2) . x)) * (((fdif (f2,h)) . (2 -' 2)) . (x + (2 * h))) by NEWTON:21 .= (((fdif (f1,h)) . 2) . x) * (f2 . (x + (2 * h))) by A6, Def6 ; A16: (S . 2) . 0 = ((2 choose 0) * (((fdif (f1,h)) . 0) . x)) * (((fdif (f2,h)) . (2 -' 0)) . (x + (0 * h))) by A7 .= (1 * (((fdif (f1,h)) . 0) . x)) * (((fdif (f2,h)) . (2 -' 0)) . (x + (0 * h))) by NEWTON:19 .= (f1 . x) * (((fdif (f2,h)) . 2) . x) by A14, Def6 ; Sum ((S . 2),2) = (Partial_Sums (S . 2)) . (1 + 1) by SERIES_1:def_5 .= ((Partial_Sums (S . 2)) . (0 + 1)) + ((S . 2) . 2) by SERIES_1:def_1 .= (((Partial_Sums (S . 2)) . 0) + ((S . 2) . 1)) + ((S . 2) . 2) by SERIES_1:def_1 .= ((fdif ((f1 (#) f2),h)) . 2) . x by A13, A16, A8, A15, SERIES_1:def_1 ; hence ( ((fdif ((f1 (#) f2),h)) . 1) . x = Sum ((S . 1),1) & ((fdif ((f1 (#) f2),h)) . 2) . x = Sum ((S . 2),2) ) by A11; ::_thesis: verum end; theorem :: DIFF_1:38 for x, h being Real for f being PartFunc of REAL,REAL st x in dom f & x - h in dom f holds (bD (f,h)) . x = (f . x) - (f . (x - h)) proof let x, h be Real; ::_thesis: for f being PartFunc of REAL,REAL st x in dom f & x - h in dom f holds (bD (f,h)) . x = (f . x) - (f . (x - h)) let f be PartFunc of REAL,REAL; ::_thesis: ( x in dom f & x - h in dom f implies (bD (f,h)) . x = (f . x) - (f . (x - h)) ) assume A1: ( x in dom f & x - h in dom f ) ; ::_thesis: (bD (f,h)) . x = (f . x) - (f . (x - h)) A2: dom (Shift (f,(- h))) = (- (- h)) ++ (dom f) by Def1; A3: h + (x - (- (- h))) in (- (- h)) ++ (dom f) by A1, MEASURE6:46; then A4: (Shift (f,(- h))) . x = f . (x + (- h)) by Def1; x in (dom (Shift (f,(- h)))) /\ (dom f) by A3, A2, A1, XBOOLE_0:def_4; then x in dom (bD (f,h)) by VALUED_1:12; hence (bD (f,h)) . x = (f . x) - (f . (x - h)) by A4, VALUED_1:13; ::_thesis: verum end; theorem :: DIFF_1:39 for x, h being Real for f being PartFunc of REAL,REAL st x + (h / 2) in dom f & x - (h / 2) in dom f holds (cD (f,h)) . x = (f . (x + (h / 2))) - (f . (x - (h / 2))) proof let x, h be Real; ::_thesis: for f being PartFunc of REAL,REAL st x + (h / 2) in dom f & x - (h / 2) in dom f holds (cD (f,h)) . x = (f . (x + (h / 2))) - (f . (x - (h / 2))) let f be PartFunc of REAL,REAL; ::_thesis: ( x + (h / 2) in dom f & x - (h / 2) in dom f implies (cD (f,h)) . x = (f . (x + (h / 2))) - (f . (x - (h / 2))) ) assume A1: ( x + (h / 2) in dom f & x - (h / 2) in dom f ) ; ::_thesis: (cD (f,h)) . x = (f . (x + (h / 2))) - (f . (x - (h / 2))) A2: dom (Shift (f,(- (h / 2)))) = (- (- (h / 2))) ++ (dom f) by Def1; A3: dom (Shift (f,(h / 2))) = (- (h / 2)) ++ (dom f) by Def1; A4: (- (h / 2)) + (x + (h / 2)) in (- (h / 2)) ++ (dom f) by A1, MEASURE6:46; then A5: (Shift (f,(h / 2))) . x = f . (x + (h / 2)) by Def1; A6: (h / 2) + (x - (h / 2)) in (- (- (h / 2))) ++ (dom f) by A1, MEASURE6:46; then A7: (Shift (f,(- (h / 2)))) . x = f . (x + (- (h / 2))) by Def1; x in (dom (Shift (f,(h / 2)))) /\ (dom (Shift (f,(- (h / 2))))) by A4, A6, A3, A2, XBOOLE_0:def_4; then x in dom (cD (f,h)) by VALUED_1:12; hence (cD (f,h)) . x = (f . (x + (h / 2))) - (f . (x - (h / 2))) by A7, A5, VALUED_1:13; ::_thesis: verum end;