:: SEQ_1 semantic presentation begin definition mode Real_Sequence is sequence of REAL; end; theorem Th1: :: SEQ_1:1 for f being Function holds ( f is Real_Sequence iff ( dom f = NAT & ( for x being set st x in NAT holds f . x is real ) ) ) proof let f be Function; ::_thesis: ( f is Real_Sequence iff ( dom f = NAT & ( for x being set st x in NAT holds f . x is real ) ) ) thus ( f is Real_Sequence implies ( dom f = NAT & ( for x being set st x in NAT holds f . x is real ) ) ) by FUNCT_2:def_1; ::_thesis: ( dom f = NAT & ( for x being set st x in NAT holds f . x is real ) implies f is Real_Sequence ) assume that A1: dom f = NAT and A2: for x being set st x in NAT holds f . x is real ; ::_thesis: f is Real_Sequence now__::_thesis:_for_y_being_set_st_y_in_rng_f_holds_ y_in_REAL let y be set ; ::_thesis: ( y in rng f implies y in REAL ) assume y in rng f ; ::_thesis: y in REAL then consider x being set such that A3: x in dom f and A4: y = f . x by FUNCT_1:def_3; f . x is real by A1, A2, A3; hence y in REAL by A4, XREAL_0:def_1; ::_thesis: verum end; then rng f c= REAL by TARSKI:def_3; hence f is Real_Sequence by A1, FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum end; theorem Th2: :: SEQ_1:2 for f being Function holds ( f is Real_Sequence iff ( dom f = NAT & ( for n being Element of NAT holds f . n is real ) ) ) proof let f be Function; ::_thesis: ( f is Real_Sequence iff ( dom f = NAT & ( for n being Element of NAT holds f . n is real ) ) ) thus ( f is Real_Sequence implies ( dom f = NAT & ( for n being Element of NAT holds f . n is real ) ) ) by Th1; ::_thesis: ( dom f = NAT & ( for n being Element of NAT holds f . n is real ) implies f is Real_Sequence ) assume that A1: dom f = NAT and A2: for n being Element of NAT holds f . n is real ; ::_thesis: f is Real_Sequence for x being set st x in NAT holds f . x is real by A2; hence f is Real_Sequence by A1, Th1; ::_thesis: verum end; definition let f be real-valued Function; let x be set ; :: original: . redefine funcf . x -> Real; coherence f . x is Real by XREAL_0:def_1; end; registration cluster Relation-like non-zero NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued for Element of K19(K20(NAT,REAL)); existence ex b1 being PartFunc of NAT,REAL st b1 is non-zero proof reconsider p = NAT --> 1 as PartFunc of NAT,REAL by FUNCOP_1:46; take p ; ::_thesis: p is non-zero rng p = {1} by FUNCOP_1:8; hence not 0 in rng p by TARSKI:def_1; :: according to RELAT_1:def_9 ::_thesis: verum end; end; theorem :: SEQ_1:3 for f being non-zero PartFunc of NAT,REAL holds rng f c= REAL \ {0} proof let f be non-zero PartFunc of NAT,REAL; ::_thesis: rng f c= REAL \ {0} not {} in rng f by RELAT_1:def_9; hence rng f c= REAL \ {0} by ZFMISC_1:34; ::_thesis: verum end; theorem Th4: :: SEQ_1:4 for seq being Real_Sequence holds ( seq is non-zero iff for x being set st x in NAT holds seq . x <> 0 ) proof let seq be Real_Sequence; ::_thesis: ( seq is non-zero iff for x being set st x in NAT holds seq . x <> 0 ) thus ( seq is non-zero implies for x being set st x in NAT holds seq . x <> 0 ) ::_thesis: ( ( for x being set st x in NAT holds seq . x <> 0 ) implies seq is non-zero ) proof assume A1: seq is non-zero ; ::_thesis: for x being set st x in NAT holds seq . x <> 0 let x be set ; ::_thesis: ( x in NAT implies seq . x <> 0 ) assume x in NAT ; ::_thesis: seq . x <> 0 then x in dom seq by Th2; then seq . x in rng seq by FUNCT_1:def_3; hence seq . x <> 0 by A1, RELAT_1:def_9; ::_thesis: verum end; assume A2: for x being set st x in NAT holds seq . x <> 0 ; ::_thesis: seq is non-zero assume 0 in rng seq ; :: according to RELAT_1:def_9 ::_thesis: contradiction then ex x being set st ( x in dom seq & seq . x = 0 ) by FUNCT_1:def_3; hence contradiction by A2; ::_thesis: verum end; theorem Th5: :: SEQ_1:5 for seq being Real_Sequence holds ( seq is non-zero iff for n being Element of NAT holds seq . n <> 0 ) proof let seq be Real_Sequence; ::_thesis: ( seq is non-zero iff for n being Element of NAT holds seq . n <> 0 ) thus ( seq is non-zero implies for n being Element of NAT holds seq . n <> 0 ) by Th4; ::_thesis: ( ( for n being Element of NAT holds seq . n <> 0 ) implies seq is non-zero ) assume for n being Element of NAT holds seq . n <> 0 ; ::_thesis: seq is non-zero then for x being set st x in NAT holds seq . x <> 0 ; hence seq is non-zero by Th4; ::_thesis: verum end; theorem :: SEQ_1:6 for r being real number ex seq being Real_Sequence st rng seq = {r} proof let r be real number ; ::_thesis: ex seq being Real_Sequence st rng seq = {r} consider f being Function such that A1: dom f = NAT and A2: rng f = {r} by FUNCT_1:5; for x being set st x in {r} holds x in REAL by XREAL_0:def_1; then rng f c= REAL by A2, TARSKI:def_3; then reconsider f = f as Real_Sequence by A1, FUNCT_2:def_1, RELSET_1:4; take f ; ::_thesis: rng f = {r} thus rng f = {r} by A2; ::_thesis: verum end; scheme :: SEQ_1:sch 1 ExRealSeq{ F1( set ) -> real number } : ex seq being Real_Sequence st for n being Element of NAT holds seq . n = F1(n) proof defpred S1[ set , set ] means ex n being Element of NAT st ( n = \$1 & \$2 = F1(n) ); A1: now__::_thesis:_for_x_being_set_st_x_in_NAT_holds_ ex_y_being_set_st_S1[x,y] let x be set ; ::_thesis: ( x in NAT implies ex y being set st S1[x,y] ) assume x in NAT ; ::_thesis: ex y being set st S1[x,y] then consider n being Element of NAT such that A2: n = x ; reconsider r2 = F1(n) as set ; take y = r2; ::_thesis: S1[x,y] thus S1[x,y] by A2; ::_thesis: verum end; consider f being Function such that A3: dom f = NAT and A4: for x being set st x in NAT holds S1[x,f . x] from CLASSES1:sch_1(A1); now__::_thesis:_for_x_being_set_st_x_in_NAT_holds_ f_._x_is_real let x be set ; ::_thesis: ( x in NAT implies f . x is real ) assume x in NAT ; ::_thesis: f . x is real then ex n being Element of NAT st ( n = x & f . x = F1(n) ) by A4; hence f . x is real ; ::_thesis: verum end; then reconsider f = f as Real_Sequence by A3, Th1; take seq = f; ::_thesis: for n being Element of NAT holds seq . n = F1(n) let n be Element of NAT ; ::_thesis: seq . n = F1(n) ex k being Element of NAT st ( k = n & seq . n = F1(k) ) by A4; hence seq . n = F1(n) ; ::_thesis: verum end; scheme :: SEQ_1:sch 2 PartFuncExD9{ F1() -> non empty set , F2() -> non empty set , P1[ set , set ] } : ex f being PartFunc of F1(),F2() st ( ( for d being Element of F1() holds ( d in dom f iff ex c being Element of F2() st P1[d,c] ) ) & ( for d being Element of F1() st d in dom f holds P1[d,f . d] ) ) proof defpred S1[ set ] means ex c being Element of F2() st P1[\$1,c]; set x = the Element of F2(); defpred S2[ Element of F1(), Element of F2()] means ( ( ex c being Element of F2() st P1[\$1,c] implies P1[\$1,\$2] ) & ( ( for c being Element of F2() holds P1[\$1,c] ) implies \$2 = the Element of F2() ) ); consider X being set such that A1: for x being set holds ( x in X iff ( x in F1() & S1[x] ) ) from XBOOLE_0:sch_1(); for x being set st x in X holds x in F1() by A1; then reconsider X = X as Subset of F1() by TARSKI:def_3; A2: for d being Element of F1() ex z being Element of F2() st S2[d,z] proof let d be Element of F1(); ::_thesis: ex z being Element of F2() st S2[d,z] ( ( for c being Element of F2() holds P1[d,c] ) implies ex z being set st ( ( ex c being Element of F2() st P1[d,c] implies P1[d,z] ) & ( ( for c being Element of F2() holds P1[d,c] ) implies z = the Element of F2() ) ) ) ; hence ex z being Element of F2() st S2[d,z] ; ::_thesis: verum end; consider g being Function of F1(),F2() such that A3: for d being Element of F1() holds S2[d,g . d] from FUNCT_2:sch_3(A2); reconsider f = g | X as PartFunc of F1(),F2() ; take f ; ::_thesis: ( ( for d being Element of F1() holds ( d in dom f iff ex c being Element of F2() st P1[d,c] ) ) & ( for d being Element of F1() st d in dom f holds P1[d,f . d] ) ) A4: dom g = F1() by FUNCT_2:def_1; thus for d being Element of F1() holds ( d in dom f iff ex c being Element of F2() st P1[d,c] ) ::_thesis: for d being Element of F1() st d in dom f holds P1[d,f . d] proof let d be Element of F1(); ::_thesis: ( d in dom f iff ex c being Element of F2() st P1[d,c] ) dom f c= X by RELAT_1:58; hence ( d in dom f implies ex c being Element of F2() st P1[d,c] ) by A1; ::_thesis: ( ex c being Element of F2() st P1[d,c] implies d in dom f ) assume ex c being Element of F2() st P1[d,c] ; ::_thesis: d in dom f then d in X by A1; then d in (dom g) /\ X by A4, XBOOLE_0:def_4; hence d in dom f by RELAT_1:61; ::_thesis: verum end; let d be Element of F1(); ::_thesis: ( d in dom f implies P1[d,f . d] ) assume A5: d in dom f ; ::_thesis: P1[d,f . d] dom f c= X by RELAT_1:58; then ex c being Element of F2() st P1[d,c] by A1, A5; then P1[d,g . d] by A3; hence P1[d,f . d] by A5, FUNCT_1:47; ::_thesis: verum end; scheme :: SEQ_1:sch 3 LambdaPFD9{ F1() -> non empty set , F2() -> non empty set , F3( set ) -> Element of F2(), P1[ set ] } : ex f being PartFunc of F1(),F2() st ( ( for d being Element of F1() holds ( d in dom f iff P1[d] ) ) & ( for d being Element of F1() st d in dom f holds f . d = F3(d) ) ) proof defpred S1[ Element of F1(), set ] means ( P1[\$1] & \$2 = F3(\$1) ); consider f being PartFunc of F1(),F2() such that A1: for d being Element of F1() holds ( d in dom f iff ex c being Element of F2() st S1[d,c] ) and A2: for d being Element of F1() st d in dom f holds S1[d,f . d] from SEQ_1:sch_2(); take f ; ::_thesis: ( ( for d being Element of F1() holds ( d in dom f iff P1[d] ) ) & ( for d being Element of F1() st d in dom f holds f . d = F3(d) ) ) thus for d being Element of F1() holds ( d in dom f iff P1[d] ) ::_thesis: for d being Element of F1() st d in dom f holds f . d = F3(d) proof let d be Element of F1(); ::_thesis: ( d in dom f iff P1[d] ) thus ( d in dom f implies P1[d] ) ::_thesis: ( P1[d] implies d in dom f ) proof assume d in dom f ; ::_thesis: P1[d] then ex c being Element of F2() st ( P1[d] & c = F3(d) ) by A1; hence P1[d] ; ::_thesis: verum end; assume P1[d] ; ::_thesis: d in dom f then ex c being Element of F2() st ( P1[d] & c = F3(d) ) ; hence d in dom f by A1; ::_thesis: verum end; thus for d being Element of F1() st d in dom f holds f . d = F3(d) by A2; ::_thesis: verum end; scheme :: SEQ_1:sch 4 UnPartFuncD9{ F1() -> set , F2() -> set , F3() -> set , F4( set ) -> set } : for f, g being PartFunc of F1(),F2() st dom f = F3() & ( for c being Element of F1() st c in dom f holds f . c = F4(c) ) & dom g = F3() & ( for c being Element of F1() st c in dom g holds g . c = F4(c) ) holds f = g proof let f, g be PartFunc of F1(),F2(); ::_thesis: ( dom f = F3() & ( for c being Element of F1() st c in dom f holds f . c = F4(c) ) & dom g = F3() & ( for c being Element of F1() st c in dom g holds g . c = F4(c) ) implies f = g ) assume that A1: dom f = F3() and A2: for c being Element of F1() st c in dom f holds f . c = F4(c) and A3: dom g = F3() and A4: for c being Element of F1() st c in dom g holds g . c = F4(c) ; ::_thesis: f = g now__::_thesis:_for_c_being_Element_of_F1()_st_c_in_dom_f_holds_ f_._c_=_g_._c let c be Element of F1(); ::_thesis: ( c in dom f implies f . c = g . c ) assume A5: c in dom f ; ::_thesis: f . c = g . c hence f . c = F4(c) by A2 .= g . c by A1, A3, A4, A5 ; ::_thesis: verum end; hence f = g by A1, A3, PARTFUN1:5; ::_thesis: verum end; theorem Th7: :: SEQ_1:7 for seq, seq1, seq2 being Real_Sequence holds ( seq = seq1 + seq2 iff for n being Element of NAT holds seq . n = (seq1 . n) + (seq2 . n) ) proof let seq, seq1, seq2 be Real_Sequence; ::_thesis: ( seq = seq1 + seq2 iff for n being Element of NAT holds seq . n = (seq1 . n) + (seq2 . n) ) thus ( seq = seq1 + seq2 implies for n being Element of NAT holds seq . n = (seq1 . n) + (seq2 . n) ) ::_thesis: ( ( for n being Element of NAT holds seq . n = (seq1 . n) + (seq2 . n) ) implies seq = seq1 + seq2 ) proof assume A1: seq = seq1 + seq2 ; ::_thesis: for n being Element of NAT holds seq . n = (seq1 . n) + (seq2 . n) let n be Element of NAT ; ::_thesis: seq . n = (seq1 . n) + (seq2 . n) dom seq = NAT by FUNCT_2:def_1; hence seq . n = (seq1 . n) + (seq2 . n) by A1, VALUED_1:def_1; ::_thesis: verum end; assume for n being Element of NAT holds seq . n = (seq1 . n) + (seq2 . n) ; ::_thesis: seq = seq1 + seq2 then A2: for n being set st n in dom seq holds seq . n = (seq1 . n) + (seq2 . n) ; dom seq = NAT /\ NAT by FUNCT_2:def_1 .= NAT /\ (dom seq2) by FUNCT_2:def_1 .= (dom seq1) /\ (dom seq2) by FUNCT_2:def_1 ; hence seq = seq1 + seq2 by A2, VALUED_1:def_1; ::_thesis: verum end; theorem Th8: :: SEQ_1:8 for seq, seq1, seq2 being Real_Sequence holds ( seq = seq1 (#) seq2 iff for n being Element of NAT holds seq . n = (seq1 . n) * (seq2 . n) ) proof let seq, seq1, seq2 be Real_Sequence; ::_thesis: ( seq = seq1 (#) seq2 iff for n being Element of NAT holds seq . n = (seq1 . n) * (seq2 . n) ) thus ( seq = seq1 (#) seq2 implies for n being Element of NAT holds seq . n = (seq1 . n) * (seq2 . n) ) ::_thesis: ( ( for n being Element of NAT holds seq . n = (seq1 . n) * (seq2 . n) ) implies seq = seq1 (#) seq2 ) proof assume A1: seq = seq1 (#) seq2 ; ::_thesis: for n being Element of NAT holds seq . n = (seq1 . n) * (seq2 . n) let n be Element of NAT ; ::_thesis: seq . n = (seq1 . n) * (seq2 . n) dom seq = NAT by FUNCT_2:def_1; hence seq . n = (seq1 . n) * (seq2 . n) by A1, VALUED_1:def_4; ::_thesis: verum end; assume for n being Element of NAT holds seq . n = (seq1 . n) * (seq2 . n) ; ::_thesis: seq = seq1 (#) seq2 then A2: for n being set st n in dom seq holds seq . n = (seq1 . n) * (seq2 . n) ; dom seq = NAT /\ NAT by FUNCT_2:def_1 .= NAT /\ (dom seq2) by FUNCT_2:def_1 .= (dom seq1) /\ (dom seq2) by FUNCT_2:def_1 ; hence seq = seq1 (#) seq2 by A2, VALUED_1:def_4; ::_thesis: verum end; theorem Th9: :: SEQ_1:9 for r being real number for seq1, seq2 being Real_Sequence holds ( seq1 = r (#) seq2 iff for n being Element of NAT holds seq1 . n = r * (seq2 . n) ) proof let r be real number ; ::_thesis: for seq1, seq2 being Real_Sequence holds ( seq1 = r (#) seq2 iff for n being Element of NAT holds seq1 . n = r * (seq2 . n) ) let seq1, seq2 be Real_Sequence; ::_thesis: ( seq1 = r (#) seq2 iff for n being Element of NAT holds seq1 . n = r * (seq2 . n) ) thus ( seq1 = r (#) seq2 implies for n being Element of NAT holds seq1 . n = r * (seq2 . n) ) by VALUED_1:6; ::_thesis: ( ( for n being Element of NAT holds seq1 . n = r * (seq2 . n) ) implies seq1 = r (#) seq2 ) assume for n being Element of NAT holds seq1 . n = r * (seq2 . n) ; ::_thesis: seq1 = r (#) seq2 then A1: for n being set st n in dom seq1 holds seq1 . n = r * (seq2 . n) ; dom seq1 = NAT by FUNCT_2:def_1 .= dom seq2 by FUNCT_2:def_1 ; hence seq1 = r (#) seq2 by A1, VALUED_1:def_5; ::_thesis: verum end; theorem :: SEQ_1:10 for seq1, seq2 being Real_Sequence holds ( seq1 = - seq2 iff for n being Element of NAT holds seq1 . n = - (seq2 . n) ) proof let seq1, seq2 be Real_Sequence; ::_thesis: ( seq1 = - seq2 iff for n being Element of NAT holds seq1 . n = - (seq2 . n) ) thus ( seq1 = - seq2 implies for n being Element of NAT holds seq1 . n = - (seq2 . n) ) by VALUED_1:8; ::_thesis: ( ( for n being Element of NAT holds seq1 . n = - (seq2 . n) ) implies seq1 = - seq2 ) assume for n being Element of NAT holds seq1 . n = - (seq2 . n) ; ::_thesis: seq1 = - seq2 then A1: for n being set st n in dom seq1 holds seq1 . n = - (seq2 . n) ; dom seq1 = NAT by FUNCT_2:def_1 .= dom seq2 by FUNCT_2:def_1 ; hence seq1 = - seq2 by A1, VALUED_1:9; ::_thesis: verum end; theorem :: SEQ_1:11 for seq1, seq2 being Real_Sequence holds seq1 - seq2 = seq1 + (- seq2) ; theorem Th12: :: SEQ_1:12 for seq1, seq being Real_Sequence holds ( seq1 = abs seq iff for n being Element of NAT holds seq1 . n = abs (seq . n) ) proof let seq1, seq be Real_Sequence; ::_thesis: ( seq1 = abs seq iff for n being Element of NAT holds seq1 . n = abs (seq . n) ) thus ( seq1 = abs seq implies for n being Element of NAT holds seq1 . n = abs (seq . n) ) by VALUED_1:18; ::_thesis: ( ( for n being Element of NAT holds seq1 . n = abs (seq . n) ) implies seq1 = abs seq ) assume for n being Element of NAT holds seq1 . n = abs (seq . n) ; ::_thesis: seq1 = abs seq then A1: for n being set st n in dom seq1 holds seq1 . n = abs (seq . n) ; dom seq1 = NAT by FUNCT_2:def_1 .= dom seq by FUNCT_2:def_1 ; hence seq1 = abs seq by A1, VALUED_1:def_11; ::_thesis: verum end; theorem Th13: :: SEQ_1:13 for seq1, seq2, seq3 being Real_Sequence holds (seq1 + seq2) + seq3 = seq1 + (seq2 + seq3) proof let seq1, seq2, seq3 be Real_Sequence; ::_thesis: (seq1 + seq2) + seq3 = seq1 + (seq2 + seq3) now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq1_+_seq2)_+_seq3)_._n_=_(seq1_+_(seq2_+_seq3))_._n let n be Element of NAT ; ::_thesis: ((seq1 + seq2) + seq3) . n = (seq1 + (seq2 + seq3)) . n thus ((seq1 + seq2) + seq3) . n = ((seq1 + seq2) . n) + (seq3 . n) by Th7 .= ((seq1 . n) + (seq2 . n)) + (seq3 . n) by Th7 .= (seq1 . n) + ((seq2 . n) + (seq3 . n)) .= (seq1 . n) + ((seq2 + seq3) . n) by Th7 .= (seq1 + (seq2 + seq3)) . n by Th7 ; ::_thesis: verum end; hence (seq1 + seq2) + seq3 = seq1 + (seq2 + seq3) by FUNCT_2:63; ::_thesis: verum end; theorem Th14: :: SEQ_1:14 for seq1, seq2, seq3 being Real_Sequence holds (seq1 (#) seq2) (#) seq3 = seq1 (#) (seq2 (#) seq3) proof let seq1, seq2, seq3 be Real_Sequence; ::_thesis: (seq1 (#) seq2) (#) seq3 = seq1 (#) (seq2 (#) seq3) now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq1_(#)_seq2)_(#)_seq3)_._n_=_(seq1_(#)_(seq2_(#)_seq3))_._n let n be Element of NAT ; ::_thesis: ((seq1 (#) seq2) (#) seq3) . n = (seq1 (#) (seq2 (#) seq3)) . n thus ((seq1 (#) seq2) (#) seq3) . n = ((seq1 (#) seq2) . n) * (seq3 . n) by Th8 .= ((seq1 . n) * (seq2 . n)) * (seq3 . n) by Th8 .= (seq1 . n) * ((seq2 . n) * (seq3 . n)) .= (seq1 . n) * ((seq2 (#) seq3) . n) by Th8 .= (seq1 (#) (seq2 (#) seq3)) . n by Th8 ; ::_thesis: verum end; hence (seq1 (#) seq2) (#) seq3 = seq1 (#) (seq2 (#) seq3) by FUNCT_2:63; ::_thesis: verum end; theorem Th15: :: SEQ_1:15 for seq1, seq2, seq3 being Real_Sequence holds (seq1 + seq2) (#) seq3 = (seq1 (#) seq3) + (seq2 (#) seq3) proof let seq1, seq2, seq3 be Real_Sequence; ::_thesis: (seq1 + seq2) (#) seq3 = (seq1 (#) seq3) + (seq2 (#) seq3) now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq1_+_seq2)_(#)_seq3)_._n_=_((seq1_(#)_seq3)_+_(seq2_(#)_seq3))_._n let n be Element of NAT ; ::_thesis: ((seq1 + seq2) (#) seq3) . n = ((seq1 (#) seq3) + (seq2 (#) seq3)) . n thus ((seq1 + seq2) (#) seq3) . n = ((seq1 + seq2) . n) * (seq3 . n) by Th8 .= ((seq1 . n) + (seq2 . n)) * (seq3 . n) by Th7 .= ((seq1 . n) * (seq3 . n)) + ((seq2 . n) * (seq3 . n)) .= ((seq1 (#) seq3) . n) + ((seq2 . n) * (seq3 . n)) by Th8 .= ((seq1 (#) seq3) . n) + ((seq2 (#) seq3) . n) by Th8 .= ((seq1 (#) seq3) + (seq2 (#) seq3)) . n by Th7 ; ::_thesis: verum end; hence (seq1 + seq2) (#) seq3 = (seq1 (#) seq3) + (seq2 (#) seq3) by FUNCT_2:63; ::_thesis: verum end; theorem :: SEQ_1:16 for seq3, seq1, seq2 being Real_Sequence holds seq3 (#) (seq1 + seq2) = (seq3 (#) seq1) + (seq3 (#) seq2) by Th15; theorem :: SEQ_1:17 for seq being Real_Sequence holds - seq = (- 1) (#) seq ; theorem Th18: :: SEQ_1:18 for r being real number for seq1, seq2 being Real_Sequence holds r (#) (seq1 (#) seq2) = (r (#) seq1) (#) seq2 proof let r be real number ; ::_thesis: for seq1, seq2 being Real_Sequence holds r (#) (seq1 (#) seq2) = (r (#) seq1) (#) seq2 let seq1, seq2 be Real_Sequence; ::_thesis: r (#) (seq1 (#) seq2) = (r (#) seq1) (#) seq2 now__::_thesis:_for_n_being_Element_of_NAT_holds_(r_(#)_(seq1_(#)_seq2))_._n_=_((r_(#)_seq1)_(#)_seq2)_._n let n be Element of NAT ; ::_thesis: (r (#) (seq1 (#) seq2)) . n = ((r (#) seq1) (#) seq2) . n thus (r (#) (seq1 (#) seq2)) . n = r * ((seq1 (#) seq2) . n) by Th9 .= r * ((seq1 . n) * (seq2 . n)) by Th8 .= (r * (seq1 . n)) * (seq2 . n) .= ((r (#) seq1) . n) * (seq2 . n) by Th9 .= ((r (#) seq1) (#) seq2) . n by Th8 ; ::_thesis: verum end; hence r (#) (seq1 (#) seq2) = (r (#) seq1) (#) seq2 by FUNCT_2:63; ::_thesis: verum end; theorem Th19: :: SEQ_1:19 for r being real number for seq1, seq2 being Real_Sequence holds r (#) (seq1 (#) seq2) = seq1 (#) (r (#) seq2) proof let r be real number ; ::_thesis: for seq1, seq2 being Real_Sequence holds r (#) (seq1 (#) seq2) = seq1 (#) (r (#) seq2) let seq1, seq2 be Real_Sequence; ::_thesis: r (#) (seq1 (#) seq2) = seq1 (#) (r (#) seq2) now__::_thesis:_for_n_being_Element_of_NAT_holds_(r_(#)_(seq1_(#)_seq2))_._n_=_(seq1_(#)_(r_(#)_seq2))_._n let n be Element of NAT ; ::_thesis: (r (#) (seq1 (#) seq2)) . n = (seq1 (#) (r (#) seq2)) . n thus (r (#) (seq1 (#) seq2)) . n = r * ((seq1 (#) seq2) . n) by Th9 .= r * ((seq1 . n) * (seq2 . n)) by Th8 .= (seq1 . n) * (r * (seq2 . n)) .= (seq1 . n) * ((r (#) seq2) . n) by Th9 .= (seq1 (#) (r (#) seq2)) . n by Th8 ; ::_thesis: verum end; hence r (#) (seq1 (#) seq2) = seq1 (#) (r (#) seq2) by FUNCT_2:63; ::_thesis: verum end; theorem Th20: :: SEQ_1:20 for seq1, seq2, seq3 being Real_Sequence holds (seq1 - seq2) (#) seq3 = (seq1 (#) seq3) - (seq2 (#) seq3) proof let seq1, seq2, seq3 be Real_Sequence; ::_thesis: (seq1 - seq2) (#) seq3 = (seq1 (#) seq3) - (seq2 (#) seq3) thus (seq1 - seq2) (#) seq3 = (seq1 (#) seq3) + ((- seq2) (#) seq3) by Th15 .= (seq1 (#) seq3) - (seq2 (#) seq3) by Th18 ; ::_thesis: verum end; theorem :: SEQ_1:21 for seq3, seq1, seq2 being Real_Sequence holds (seq3 (#) seq1) - (seq3 (#) seq2) = seq3 (#) (seq1 - seq2) by Th20; theorem Th22: :: SEQ_1:22 for r being real number for seq1, seq2 being Real_Sequence holds r (#) (seq1 + seq2) = (r (#) seq1) + (r (#) seq2) proof let r be real number ; ::_thesis: for seq1, seq2 being Real_Sequence holds r (#) (seq1 + seq2) = (r (#) seq1) + (r (#) seq2) let seq1, seq2 be Real_Sequence; ::_thesis: r (#) (seq1 + seq2) = (r (#) seq1) + (r (#) seq2) now__::_thesis:_for_n_being_Element_of_NAT_holds_(r_(#)_(seq1_+_seq2))_._n_=_((r_(#)_seq1)_+_(r_(#)_seq2))_._n let n be Element of NAT ; ::_thesis: (r (#) (seq1 + seq2)) . n = ((r (#) seq1) + (r (#) seq2)) . n thus (r (#) (seq1 + seq2)) . n = r * ((seq1 + seq2) . n) by Th9 .= r * ((seq1 . n) + (seq2 . n)) by Th7 .= (r * (seq1 . n)) + (r * (seq2 . n)) .= ((r (#) seq1) . n) + (r * (seq2 . n)) by Th9 .= ((r (#) seq1) . n) + ((r (#) seq2) . n) by Th9 .= ((r (#) seq1) + (r (#) seq2)) . n by Th7 ; ::_thesis: verum end; hence r (#) (seq1 + seq2) = (r (#) seq1) + (r (#) seq2) by FUNCT_2:63; ::_thesis: verum end; theorem Th23: :: SEQ_1:23 for r, p being real number for seq being Real_Sequence holds (r * p) (#) seq = r (#) (p (#) seq) proof let r, p be real number ; ::_thesis: for seq being Real_Sequence holds (r * p) (#) seq = r (#) (p (#) seq) let seq be Real_Sequence; ::_thesis: (r * p) (#) seq = r (#) (p (#) seq) now__::_thesis:_for_n_being_Element_of_NAT_holds_((r_*_p)_(#)_seq)_._n_=_(r_(#)_(p_(#)_seq))_._n let n be Element of NAT ; ::_thesis: ((r * p) (#) seq) . n = (r (#) (p (#) seq)) . n thus ((r * p) (#) seq) . n = (r * p) * (seq . n) by Th9 .= r * (p * (seq . n)) .= r * ((p (#) seq) . n) by Th9 .= (r (#) (p (#) seq)) . n by Th9 ; ::_thesis: verum end; hence (r * p) (#) seq = r (#) (p (#) seq) by FUNCT_2:63; ::_thesis: verum end; theorem Th24: :: SEQ_1:24 for r being real number for seq1, seq2 being Real_Sequence holds r (#) (seq1 - seq2) = (r (#) seq1) - (r (#) seq2) proof let r be real number ; ::_thesis: for seq1, seq2 being Real_Sequence holds r (#) (seq1 - seq2) = (r (#) seq1) - (r (#) seq2) let seq1, seq2 be Real_Sequence; ::_thesis: r (#) (seq1 - seq2) = (r (#) seq1) - (r (#) seq2) thus r (#) (seq1 - seq2) = (r (#) seq1) + (r (#) (- seq2)) by Th22 .= (r (#) seq1) + (((- 1) * r) (#) seq2) by Th23 .= (r (#) seq1) - (r (#) seq2) by Th23 ; ::_thesis: verum end; theorem :: SEQ_1:25 for r being real number for seq1, seq being Real_Sequence holds r (#) (seq1 /" seq) = (r (#) seq1) /" seq proof let r be real number ; ::_thesis: for seq1, seq being Real_Sequence holds r (#) (seq1 /" seq) = (r (#) seq1) /" seq let seq1, seq be Real_Sequence; ::_thesis: r (#) (seq1 /" seq) = (r (#) seq1) /" seq thus r (#) (seq1 /" seq) = r (#) (seq1 (#) (seq ")) .= (r (#) seq1) /" seq by Th18 ; ::_thesis: verum end; theorem :: SEQ_1:26 for seq1, seq2, seq3 being Real_Sequence holds seq1 - (seq2 + seq3) = (seq1 - seq2) - seq3 proof let seq1, seq2, seq3 be Real_Sequence; ::_thesis: seq1 - (seq2 + seq3) = (seq1 - seq2) - seq3 thus seq1 - (seq2 + seq3) = seq1 + ((- seq2) + ((- 1) (#) seq3)) by Th22 .= (seq1 - seq2) - seq3 by Th13 ; ::_thesis: verum end; theorem :: SEQ_1:27 for seq being Real_Sequence holds 1 (#) seq = seq proof let seq be Real_Sequence; ::_thesis: 1 (#) seq = seq now__::_thesis:_for_n_being_Element_of_NAT_holds_(1_(#)_seq)_._n_=_seq_._n let n be Element of NAT ; ::_thesis: (1 (#) seq) . n = seq . n thus (1 (#) seq) . n = 1 * (seq . n) by Th9 .= seq . n ; ::_thesis: verum end; hence 1 (#) seq = seq by FUNCT_2:63; ::_thesis: verum end; theorem :: SEQ_1:28 canceled; theorem :: SEQ_1:29 for seq1, seq2 being Real_Sequence holds seq1 - (- seq2) = seq1 + seq2 ; theorem :: SEQ_1:30 for seq1, seq2, seq3 being Real_Sequence holds seq1 - (seq2 - seq3) = (seq1 - seq2) + seq3 proof let seq1, seq2, seq3 be Real_Sequence; ::_thesis: seq1 - (seq2 - seq3) = (seq1 - seq2) + seq3 thus seq1 - (seq2 - seq3) = seq1 + ((- seq2) - (- seq3)) by Th24 .= (seq1 - seq2) + seq3 by Th13 ; ::_thesis: verum end; theorem :: SEQ_1:31 for seq1, seq2, seq3 being Real_Sequence holds seq1 + (seq2 - seq3) = (seq1 + seq2) - seq3 proof let seq1, seq2, seq3 be Real_Sequence; ::_thesis: seq1 + (seq2 - seq3) = (seq1 + seq2) - seq3 thus seq1 + (seq2 - seq3) = (seq1 + seq2) + (- seq3) by Th13 .= (seq1 + seq2) - seq3 ; ::_thesis: verum end; theorem :: SEQ_1:32 for seq1, seq2 being Real_Sequence holds ( (- seq1) (#) seq2 = - (seq1 (#) seq2) & seq1 (#) (- seq2) = - (seq1 (#) seq2) ) by Th18; theorem Th33: :: SEQ_1:33 for seq being Real_Sequence st seq is non-zero holds seq " is non-zero proof let seq be Real_Sequence; ::_thesis: ( seq is non-zero implies seq " is non-zero ) assume that A1: seq is non-zero and A2: not seq " is non-zero ; ::_thesis: contradiction consider n1 being Element of NAT such that A3: (seq ") . n1 = 0 by A2, Th5; (seq . n1) " = (seq ") . n1 by VALUED_1:10; hence contradiction by A1, A3, Th5, XCMPLX_1:202; ::_thesis: verum end; theorem :: SEQ_1:34 canceled; theorem Th35: :: SEQ_1:35 for seq, seq1 being Real_Sequence holds ( ( seq is non-zero & seq1 is non-zero ) iff seq (#) seq1 is non-zero ) proof let seq, seq1 be Real_Sequence; ::_thesis: ( ( seq is non-zero & seq1 is non-zero ) iff seq (#) seq1 is non-zero ) thus ( seq is non-zero & seq1 is non-zero implies seq (#) seq1 is non-zero ) ::_thesis: ( seq (#) seq1 is non-zero implies ( seq is non-zero & seq1 is non-zero ) ) proof assume A1: ( seq is non-zero & seq1 is non-zero ) ; ::_thesis: seq (#) seq1 is non-zero now__::_thesis:_for_n_being_Element_of_NAT_holds_(seq_(#)_seq1)_._n_<>_0 let n be Element of NAT ; ::_thesis: (seq (#) seq1) . n <> 0 A2: (seq (#) seq1) . n = (seq . n) * (seq1 . n) by Th8; ( seq . n <> 0 & seq1 . n <> 0 ) by A1, Th5; hence (seq (#) seq1) . n <> 0 by A2, XCMPLX_1:6; ::_thesis: verum end; hence seq (#) seq1 is non-zero by Th5; ::_thesis: verum end; assume A3: seq (#) seq1 is non-zero ; ::_thesis: ( seq is non-zero & seq1 is non-zero ) now__::_thesis:_for_n_being_Element_of_NAT_holds_seq_._n_<>_0 let n be Element of NAT ; ::_thesis: seq . n <> 0 (seq (#) seq1) . n = (seq . n) * (seq1 . n) by Th8; hence seq . n <> 0 by A3, Th5; ::_thesis: verum end; hence seq is non-zero by Th5; ::_thesis: seq1 is non-zero now__::_thesis:_for_n_being_Element_of_NAT_holds_seq1_._n_<>_0 let n be Element of NAT ; ::_thesis: seq1 . n <> 0 (seq (#) seq1) . n = (seq . n) * (seq1 . n) by Th8; hence seq1 . n <> 0 by A3, Th5; ::_thesis: verum end; hence seq1 is non-zero by Th5; ::_thesis: verum end; theorem Th36: :: SEQ_1:36 for seq, seq1 being Real_Sequence holds (seq ") (#) (seq1 ") = (seq (#) seq1) " proof let seq, seq1 be Real_Sequence; ::_thesis: (seq ") (#) (seq1 ") = (seq (#) seq1) " now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq_")_(#)_(seq1_"))_._n_=_((seq_(#)_seq1)_")_._n let n be Element of NAT ; ::_thesis: ((seq ") (#) (seq1 ")) . n = ((seq (#) seq1) ") . n thus ((seq ") (#) (seq1 ")) . n = ((seq ") . n) * ((seq1 ") . n) by Th8 .= ((seq ") . n) * ((seq1 . n) ") by VALUED_1:10 .= ((seq . n) ") * ((seq1 . n) ") by VALUED_1:10 .= ((seq . n) * (seq1 . n)) " by XCMPLX_1:204 .= ((seq (#) seq1) . n) " by Th8 .= ((seq (#) seq1) ") . n by VALUED_1:10 ; ::_thesis: verum end; hence (seq ") (#) (seq1 ") = (seq (#) seq1) " by FUNCT_2:63; ::_thesis: verum end; theorem :: SEQ_1:37 for seq, seq1 being Real_Sequence st seq is non-zero holds (seq1 /" seq) (#) seq = seq1 proof let seq, seq1 be Real_Sequence; ::_thesis: ( seq is non-zero implies (seq1 /" seq) (#) seq = seq1 ) assume A1: seq is non-zero ; ::_thesis: (seq1 /" seq) (#) seq = seq1 now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq1_/"_seq)_(#)_seq)_._n_=_seq1_._n let n be Element of NAT ; ::_thesis: ((seq1 /" seq) (#) seq) . n = seq1 . n A2: seq . n <> 0 by A1, Th5; thus ((seq1 /" seq) (#) seq) . n = ((seq1 (#) (seq ")) . n) * (seq . n) by Th8 .= ((seq1 . n) * ((seq ") . n)) * (seq . n) by Th8 .= ((seq1 . n) * ((seq . n) ")) * (seq . n) by VALUED_1:10 .= (seq1 . n) * (((seq . n) ") * (seq . n)) .= (seq1 . n) * 1 by A2, XCMPLX_0:def_7 .= seq1 . n ; ::_thesis: verum end; hence (seq1 /" seq) (#) seq = seq1 by FUNCT_2:63; ::_thesis: verum end; theorem :: SEQ_1:38 for seq9, seq, seq19, seq1 being Real_Sequence holds (seq9 /" seq) (#) (seq19 /" seq1) = (seq9 (#) seq19) /" (seq (#) seq1) proof let seq9, seq, seq19, seq1 be Real_Sequence; ::_thesis: (seq9 /" seq) (#) (seq19 /" seq1) = (seq9 (#) seq19) /" (seq (#) seq1) now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq9_/"_seq)_(#)_(seq19_/"_seq1))_._n_=_((seq9_(#)_seq19)_/"_(seq_(#)_seq1))_._n let n be Element of NAT ; ::_thesis: ((seq9 /" seq) (#) (seq19 /" seq1)) . n = ((seq9 (#) seq19) /" (seq (#) seq1)) . n thus ((seq9 /" seq) (#) (seq19 /" seq1)) . n = ((seq9 (#) (seq ")) . n) * ((seq19 /" seq1) . n) by Th8 .= ((seq9 . n) * ((seq ") . n)) * ((seq19 (#) (seq1 ")) . n) by Th8 .= ((seq9 . n) * ((seq ") . n)) * ((seq19 . n) * ((seq1 ") . n)) by Th8 .= (seq9 . n) * ((seq19 . n) * (((seq ") . n) * ((seq1 ") . n))) .= (seq9 . n) * ((seq19 . n) * (((seq ") (#) (seq1 ")) . n)) by Th8 .= ((seq9 . n) * (seq19 . n)) * (((seq ") (#) (seq1 ")) . n) .= ((seq9 . n) * (seq19 . n)) * (((seq (#) seq1) ") . n) by Th36 .= ((seq9 (#) seq19) . n) * (((seq (#) seq1) ") . n) by Th8 .= ((seq9 (#) seq19) /" (seq (#) seq1)) . n by Th8 ; ::_thesis: verum end; hence (seq9 /" seq) (#) (seq19 /" seq1) = (seq9 (#) seq19) /" (seq (#) seq1) by FUNCT_2:63; ::_thesis: verum end; theorem :: SEQ_1:39 for seq, seq1 being Real_Sequence st seq is non-zero & seq1 is non-zero holds seq /" seq1 is non-zero proof let seq, seq1 be Real_Sequence; ::_thesis: ( seq is non-zero & seq1 is non-zero implies seq /" seq1 is non-zero ) assume that A1: seq is non-zero and A2: seq1 is non-zero ; ::_thesis: seq /" seq1 is non-zero seq1 " is non-zero by A2, Th33; hence seq /" seq1 is non-zero by A1, Th35; ::_thesis: verum end; theorem Th40: :: SEQ_1:40 for seq, seq1 being Real_Sequence holds (seq /" seq1) " = seq1 /" seq proof let seq, seq1 be Real_Sequence; ::_thesis: (seq /" seq1) " = seq1 /" seq now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq_/"_seq1)_")_._n_=_(seq1_/"_seq)_._n let n be Element of NAT ; ::_thesis: ((seq /" seq1) ") . n = (seq1 /" seq) . n thus ((seq /" seq1) ") . n = ((seq ") (#) ((seq1 ") ")) . n by Th36 .= (seq1 /" seq) . n ; ::_thesis: verum end; hence (seq /" seq1) " = seq1 /" seq by FUNCT_2:63; ::_thesis: verum end; theorem :: SEQ_1:41 for seq2, seq1, seq being Real_Sequence holds seq2 (#) (seq1 /" seq) = (seq2 (#) seq1) /" seq proof let seq2, seq1, seq be Real_Sequence; ::_thesis: seq2 (#) (seq1 /" seq) = (seq2 (#) seq1) /" seq thus seq2 (#) (seq1 /" seq) = seq2 (#) (seq1 (#) (seq ")) .= (seq2 (#) seq1) /" seq by Th14 ; ::_thesis: verum end; theorem :: SEQ_1:42 for seq2, seq, seq1 being Real_Sequence holds seq2 /" (seq /" seq1) = (seq2 (#) seq1) /" seq proof let seq2, seq, seq1 be Real_Sequence; ::_thesis: seq2 /" (seq /" seq1) = (seq2 (#) seq1) /" seq thus seq2 /" (seq /" seq1) = seq2 (#) (seq1 /" seq) by Th40 .= seq2 (#) (seq1 (#) (seq ")) .= (seq2 (#) seq1) /" seq by Th14 ; ::_thesis: verum end; theorem Th43: :: SEQ_1:43 for seq1, seq2, seq being Real_Sequence st seq1 is non-zero holds seq2 /" seq = (seq2 (#) seq1) /" (seq (#) seq1) proof let seq1, seq2, seq be Real_Sequence; ::_thesis: ( seq1 is non-zero implies seq2 /" seq = (seq2 (#) seq1) /" (seq (#) seq1) ) assume A1: seq1 is non-zero ; ::_thesis: seq2 /" seq = (seq2 (#) seq1) /" (seq (#) seq1) now__::_thesis:_for_n_being_Element_of_NAT_holds_(seq2_/"_seq)_._n_=_((seq2_(#)_seq1)_/"_(seq_(#)_seq1))_._n let n be Element of NAT ; ::_thesis: (seq2 /" seq) . n = ((seq2 (#) seq1) /" (seq (#) seq1)) . n A2: seq1 . n <> 0 by A1, Th5; thus (seq2 /" seq) . n = ((seq2 . n) * 1) * ((seq ") . n) by Th8 .= ((seq2 . n) * ((seq1 . n) * ((seq1 . n) "))) * ((seq ") . n) by A2, XCMPLX_0:def_7 .= ((seq2 . n) * (seq1 . n)) * (((seq1 . n) ") * ((seq ") . n)) .= ((seq2 (#) seq1) . n) * (((seq1 . n) ") * ((seq ") . n)) by Th8 .= ((seq2 (#) seq1) . n) * (((seq1 ") . n) * ((seq ") . n)) by VALUED_1:10 .= ((seq2 (#) seq1) . n) * (((seq ") (#) (seq1 ")) . n) by Th8 .= ((seq2 (#) seq1) . n) * (((seq (#) seq1) ") . n) by Th36 .= ((seq2 (#) seq1) /" (seq (#) seq1)) . n by Th8 ; ::_thesis: verum end; hence seq2 /" seq = (seq2 (#) seq1) /" (seq (#) seq1) by FUNCT_2:63; ::_thesis: verum end; theorem Th44: :: SEQ_1:44 for r being real number for seq being Real_Sequence st r <> 0 & seq is non-zero holds r (#) seq is non-zero proof let r be real number ; ::_thesis: for seq being Real_Sequence st r <> 0 & seq is non-zero holds r (#) seq is non-zero let seq be Real_Sequence; ::_thesis: ( r <> 0 & seq is non-zero implies r (#) seq is non-zero ) assume that A1: r <> 0 and A2: seq is non-zero and A3: not r (#) seq is non-zero ; ::_thesis: contradiction consider n1 being Element of NAT such that A4: (r (#) seq) . n1 = 0 by A3, Th5; A5: seq . n1 <> 0 by A2, Th5; r * (seq . n1) = 0 by A4, Th9; hence contradiction by A1, A5, XCMPLX_1:6; ::_thesis: verum end; theorem :: SEQ_1:45 for seq being Real_Sequence st seq is non-zero holds - seq is non-zero by Th44; theorem Th46: :: SEQ_1:46 for r being real number for seq being Real_Sequence holds (r (#) seq) " = (r ") (#) (seq ") proof let r be real number ; ::_thesis: for seq being Real_Sequence holds (r (#) seq) " = (r ") (#) (seq ") let seq be Real_Sequence; ::_thesis: (r (#) seq) " = (r ") (#) (seq ") now__::_thesis:_for_n_being_Element_of_NAT_holds_((r_(#)_seq)_")_._n_=_((r_")_(#)_(seq_"))_._n let n be Element of NAT ; ::_thesis: ((r (#) seq) ") . n = ((r ") (#) (seq ")) . n thus ((r (#) seq) ") . n = ((r (#) seq) . n) " by VALUED_1:10 .= (r * (seq . n)) " by Th9 .= (r ") * ((seq . n) ") by XCMPLX_1:204 .= (r ") * ((seq ") . n) by VALUED_1:10 .= ((r ") (#) (seq ")) . n by Th9 ; ::_thesis: verum end; hence (r (#) seq) " = (r ") (#) (seq ") by FUNCT_2:63; ::_thesis: verum end; Lm1: (- 1) " = - 1 ; theorem :: SEQ_1:47 for seq being Real_Sequence holds (- seq) " = (- 1) (#) (seq ") by Lm1, Th46; theorem :: SEQ_1:48 for seq1, seq being Real_Sequence holds ( - (seq1 /" seq) = (- seq1) /" seq & seq1 /" (- seq) = - (seq1 /" seq) ) proof let seq1, seq be Real_Sequence; ::_thesis: ( - (seq1 /" seq) = (- seq1) /" seq & seq1 /" (- seq) = - (seq1 /" seq) ) thus - (seq1 /" seq) = (- 1) (#) (seq1 (#) (seq ")) .= (- seq1) /" seq by Th18 ; ::_thesis: seq1 /" (- seq) = - (seq1 /" seq) thus seq1 /" (- seq) = seq1 (#) ((- 1) (#) (seq ")) by Lm1, Th46 .= - (seq1 /" seq) by Th19 ; ::_thesis: verum end; theorem :: SEQ_1:49 for seq1, seq, seq19 being Real_Sequence holds ( (seq1 /" seq) + (seq19 /" seq) = (seq1 + seq19) /" seq & (seq1 /" seq) - (seq19 /" seq) = (seq1 - seq19) /" seq ) proof let seq1, seq, seq19 be Real_Sequence; ::_thesis: ( (seq1 /" seq) + (seq19 /" seq) = (seq1 + seq19) /" seq & (seq1 /" seq) - (seq19 /" seq) = (seq1 - seq19) /" seq ) thus (seq1 /" seq) + (seq19 /" seq) = (seq1 + seq19) (#) (seq ") by Th15 .= (seq1 + seq19) /" seq ; ::_thesis: (seq1 /" seq) - (seq19 /" seq) = (seq1 - seq19) /" seq thus (seq1 /" seq) - (seq19 /" seq) = (seq1 - seq19) (#) (seq ") by Th20 .= (seq1 - seq19) /" seq ; ::_thesis: verum end; theorem :: SEQ_1:50 for seq, seq9, seq1, seq19 being Real_Sequence st seq is non-zero & seq9 is non-zero holds ( (seq1 /" seq) + (seq19 /" seq9) = ((seq1 (#) seq9) + (seq19 (#) seq)) /" (seq (#) seq9) & (seq1 /" seq) - (seq19 /" seq9) = ((seq1 (#) seq9) - (seq19 (#) seq)) /" (seq (#) seq9) ) proof let seq, seq9, seq1, seq19 be Real_Sequence; ::_thesis: ( seq is non-zero & seq9 is non-zero implies ( (seq1 /" seq) + (seq19 /" seq9) = ((seq1 (#) seq9) + (seq19 (#) seq)) /" (seq (#) seq9) & (seq1 /" seq) - (seq19 /" seq9) = ((seq1 (#) seq9) - (seq19 (#) seq)) /" (seq (#) seq9) ) ) assume that A1: seq is non-zero and A2: seq9 is non-zero ; ::_thesis: ( (seq1 /" seq) + (seq19 /" seq9) = ((seq1 (#) seq9) + (seq19 (#) seq)) /" (seq (#) seq9) & (seq1 /" seq) - (seq19 /" seq9) = ((seq1 (#) seq9) - (seq19 (#) seq)) /" (seq (#) seq9) ) thus (seq1 /" seq) + (seq19 /" seq9) = ((seq1 (#) seq9) /" (seq (#) seq9)) + (seq19 /" seq9) by A2, Th43 .= ((seq1 (#) seq9) /" (seq (#) seq9)) + ((seq19 (#) seq) /" (seq (#) seq9)) by A1, Th43 .= ((seq1 (#) seq9) + (seq19 (#) seq)) (#) ((seq (#) seq9) ") by Th15 .= ((seq1 (#) seq9) + (seq19 (#) seq)) /" (seq (#) seq9) ; ::_thesis: (seq1 /" seq) - (seq19 /" seq9) = ((seq1 (#) seq9) - (seq19 (#) seq)) /" (seq (#) seq9) thus (seq1 /" seq) - (seq19 /" seq9) = ((seq1 (#) seq9) /" (seq (#) seq9)) - (seq19 /" seq9) by A2, Th43 .= ((seq1 (#) seq9) /" (seq (#) seq9)) - ((seq19 (#) seq) /" (seq (#) seq9)) by A1, Th43 .= ((seq1 (#) seq9) - (seq19 (#) seq)) (#) ((seq (#) seq9) ") by Th20 .= ((seq1 (#) seq9) - (seq19 (#) seq)) /" (seq (#) seq9) ; ::_thesis: verum end; theorem :: SEQ_1:51 for seq19, seq, seq9, seq1 being Real_Sequence holds (seq19 /" seq) /" (seq9 /" seq1) = (seq19 (#) seq1) /" (seq (#) seq9) proof let seq19, seq, seq9, seq1 be Real_Sequence; ::_thesis: (seq19 /" seq) /" (seq9 /" seq1) = (seq19 (#) seq1) /" (seq (#) seq9) thus (seq19 /" seq) /" (seq9 /" seq1) = (seq19 /" seq) (#) ((seq9 ") (#) ((seq1 ") ")) by Th36 .= ((seq19 (#) (seq ")) (#) seq1) (#) (seq9 ") by Th14 .= (seq19 (#) (seq1 (#) (seq "))) (#) (seq9 ") by Th14 .= seq19 (#) ((seq1 (#) (seq ")) (#) (seq9 ")) by Th14 .= seq19 (#) (seq1 (#) ((seq ") (#) (seq9 "))) by Th14 .= (seq19 (#) seq1) (#) ((seq ") (#) (seq9 ")) by Th14 .= (seq19 (#) seq1) /" (seq (#) seq9) by Th36 ; ::_thesis: verum end; theorem Th52: :: SEQ_1:52 for seq, seq9 being Real_Sequence holds abs (seq (#) seq9) = (abs seq) (#) (abs seq9) proof let seq, seq9 be Real_Sequence; ::_thesis: abs (seq (#) seq9) = (abs seq) (#) (abs seq9) now__::_thesis:_for_n_being_Element_of_NAT_holds_(abs_(seq_(#)_seq9))_._n_=_((abs_seq)_(#)_(abs_seq9))_._n let n be Element of NAT ; ::_thesis: (abs (seq (#) seq9)) . n = ((abs seq) (#) (abs seq9)) . n thus (abs (seq (#) seq9)) . n = abs ((seq (#) seq9) . n) by Th12 .= abs ((seq . n) * (seq9 . n)) by Th8 .= (abs (seq . n)) * (abs (seq9 . n)) by COMPLEX1:65 .= ((abs seq) . n) * (abs (seq9 . n)) by Th12 .= ((abs seq) . n) * ((abs seq9) . n) by Th12 .= ((abs seq) (#) (abs seq9)) . n by Th8 ; ::_thesis: verum end; hence abs (seq (#) seq9) = (abs seq) (#) (abs seq9) by FUNCT_2:63; ::_thesis: verum end; theorem :: SEQ_1:53 for seq being Real_Sequence st seq is non-zero holds abs seq is non-zero proof let seq be Real_Sequence; ::_thesis: ( seq is non-zero implies abs seq is non-zero ) assume A1: seq is non-zero ; ::_thesis: abs seq is non-zero now__::_thesis:_for_n_being_Element_of_NAT_holds_(abs_seq)_._n_<>_0 let n be Element of NAT ; ::_thesis: (abs seq) . n <> 0 seq . n <> 0 by A1, Th5; then abs (seq . n) <> 0 by COMPLEX1:47; hence (abs seq) . n <> 0 by Th12; ::_thesis: verum end; hence abs seq is non-zero by Th5; ::_thesis: verum end; theorem Th54: :: SEQ_1:54 for seq being Real_Sequence holds (abs seq) " = abs (seq ") proof let seq be Real_Sequence; ::_thesis: (abs seq) " = abs (seq ") now__::_thesis:_for_n_being_Element_of_NAT_holds_(abs_(seq_"))_._n_=_((abs_seq)_")_._n let n be Element of NAT ; ::_thesis: (abs (seq ")) . n = ((abs seq) ") . n thus (abs (seq ")) . n = abs ((seq ") . n) by Th12 .= abs ((seq . n) ") by VALUED_1:10 .= abs (1 / (seq . n)) by XCMPLX_1:215 .= 1 / (abs (seq . n)) by ABSVALUE:7 .= (abs (seq . n)) " by XCMPLX_1:215 .= ((abs seq) . n) " by Th12 .= ((abs seq) ") . n by VALUED_1:10 ; ::_thesis: verum end; hence (abs seq) " = abs (seq ") by FUNCT_2:63; ::_thesis: verum end; theorem :: SEQ_1:55 for seq9, seq being Real_Sequence holds abs (seq9 /" seq) = (abs seq9) /" (abs seq) proof let seq9, seq be Real_Sequence; ::_thesis: abs (seq9 /" seq) = (abs seq9) /" (abs seq) thus abs (seq9 /" seq) = (abs seq9) (#) (abs (seq ")) by Th52 .= (abs seq9) /" (abs seq) by Th54 ; ::_thesis: verum end; theorem :: SEQ_1:56 for r being real number for seq being Real_Sequence holds abs (r (#) seq) = (abs r) (#) (abs seq) proof let r be real number ; ::_thesis: for seq being Real_Sequence holds abs (r (#) seq) = (abs r) (#) (abs seq) let seq be Real_Sequence; ::_thesis: abs (r (#) seq) = (abs r) (#) (abs seq) now__::_thesis:_for_n_being_Element_of_NAT_holds_(abs_(r_(#)_seq))_._n_=_((abs_r)_(#)_(abs_seq))_._n let n be Element of NAT ; ::_thesis: (abs (r (#) seq)) . n = ((abs r) (#) (abs seq)) . n thus (abs (r (#) seq)) . n = abs ((r (#) seq) . n) by Th12 .= abs (r * (seq . n)) by Th9 .= (abs r) * (abs (seq . n)) by COMPLEX1:65 .= (abs r) * ((abs seq) . n) by Th12 .= ((abs r) (#) (abs seq)) . n by Th9 ; ::_thesis: verum end; hence abs (r (#) seq) = (abs r) (#) (abs seq) by FUNCT_2:63; ::_thesis: verum end;