:: RVSUM_1 semantic presentation begin registration let n be Nat; cluster Relation-like NAT -defined Function-like natural-valued V60() n -element FinSequence-like FinSubsequence-like for set ; existence ex b1 being FinSequence st ( b1 is n -element & b1 is natural-valued ) proof take n |-> 0 ; ::_thesis: ( n |-> 0 is n -element & n |-> 0 is natural-valued ) thus ( n |-> 0 is n -element & n |-> 0 is natural-valued ) ; ::_thesis: verum end; end; registration cluster Relation-like NAT -defined Function-like real-valued V60() FinSequence-like FinSubsequence-like for set ; existence ex b1 being FinSequence st b1 is real-valued proof the FinSequence of REAL is real-valued ; hence ex b1 being FinSequence st b1 is real-valued ; ::_thesis: verum end; end; definition let F be real-valued Relation; :: original: rng redefine func rng F -> Subset of REAL; coherence rng F is Subset of REAL by VALUED_0:def_3; end; registration let D be non empty set ; let F be Function of REAL,D; let F1 be real-valued FinSequence; clusterF1 (#) F -> FinSequence-like ; coherence F * F1 is FinSequence-like proof consider n1 being Nat such that A1: dom F1 = Seg n1 by FINSEQ_1:def_2; take n1 ; :: according to FINSEQ_1:def_2 ::_thesis: dom (F * F1) = Seg n1 ( dom F = REAL & rng F1 c= REAL ) by FUNCT_2:def_1; hence dom (F * F1) = Seg n1 by A1, RELAT_1:27; ::_thesis: verum end; end; registration let r be real number ; cluster<*r*> -> real-valued ; coherence <*r*> is real-valued proof reconsider p = r as Element of REAL by XREAL_0:def_1; <*p*> is FinSequence-like ; hence <*r*> is real-valued ; ::_thesis: verum end; end; registration let r1, r2 be real number ; cluster<*r1,r2*> -> real-valued ; coherence <*r1,r2*> is real-valued proof reconsider p1 = r1, p2 = r2 as Element of REAL by XREAL_0:def_1; <*p1,p2*> is FinSequence-like ; hence <*r1,r2*> is real-valued ; ::_thesis: verum end; end; registration let r1, r2, r3 be real number ; cluster<*r1,r2,r3*> -> real-valued ; coherence <*r1,r2,r3*> is real-valued proof reconsider p1 = r1, p2 = r2, p3 = r3 as Element of REAL by XREAL_0:def_1; <*p1,p2,p3*> is FinSequence-like ; hence <*r1,r2,r3*> is real-valued ; ::_thesis: verum end; end; registration let r1, r2, r3, r4 be real number ; cluster<*r1,r2,r3,r4*> -> real-valued ; coherence <*r1,r2,r3,r4*> is real-valued proof reconsider p1 = r1, p2 = r2, p3 = r3, p4 = r4 as Element of REAL by XREAL_0:def_1; <*p1,p2,p3,p4*> is FinSequence-like ; hence <*r1,r2,r3,r4*> is real-valued ; ::_thesis: verum end; end; registration let j be Nat; let r be real number ; clusterj |-> r -> real-valued ; coherence j |-> r is real-valued ; end; registration let f, g be real-valued FinSequence; clusterf ^ g -> real-valued ; coherence f ^ g is real-valued proof rng (f ^ g) = (rng f) \/ (rng g) by FINSEQ_1:31; then rng (f ^ g) c= REAL by XBOOLE_1:8; hence f ^ g is real-valued by VALUED_0:def_3; ::_thesis: verum end; end; theorem :: RVSUM_1:1 0 is_a_unity_wrt addreal by BINOP_2:2, SETWISEO:14; definition redefine func diffreal equals :: RVSUM_1:def 1 addreal * ((id REAL),compreal); compatibility for b1 being Element of bool [:[:REAL,REAL:],REAL:] holds ( b1 = diffreal iff b1 = addreal * ((id REAL),compreal) ) proof let b be BinOp of REAL; ::_thesis: ( b = diffreal iff b = addreal * ((id REAL),compreal) ) now__::_thesis:_for_r1,_r2_being_Element_of_REAL_holds_diffreal_._(r1,r2)_=_(addreal_*_((id_REAL),compreal))_._(r1,r2) let r1, r2 be Element of REAL ; ::_thesis: diffreal . (r1,r2) = (addreal * ((id REAL),compreal)) . (r1,r2) thus diffreal . (r1,r2) = r1 - r2 by BINOP_2:def_10 .= r1 + (- r2) .= addreal . (r1,(- r2)) by BINOP_2:def_9 .= addreal . (r1,(compreal . r2)) by BINOP_2:def_7 .= (addreal * ((id REAL),compreal)) . (r1,r2) by FINSEQOP:82 ; ::_thesis: verum end; hence ( b = diffreal iff b = addreal * ((id REAL),compreal) ) by BINOP_1:2; ::_thesis: verum end; correctness ; end; :: deftheorem defines diffreal RVSUM_1:def_1_:_ diffreal = addreal * ((id REAL),compreal); definition func sqrreal -> UnOp of REAL means :Def2: :: RVSUM_1:def 2 for r being real number holds it . r = r ^2 ; existence ex b1 being UnOp of REAL st for r being real number holds b1 . r = r ^2 proof deffunc H1( Element of REAL ) -> Element of REAL = $1 ^2 ; consider G being Function of REAL,REAL such that A1: for x being Element of REAL holds G . x = H1(x) from FUNCT_2:sch_4(); take G ; ::_thesis: for r being real number holds G . r = r ^2 let r be real number ; ::_thesis: G . r = r ^2 r in REAL by XREAL_0:def_1; hence G . r = r ^2 by A1; ::_thesis: verum end; uniqueness for b1, b2 being UnOp of REAL st ( for r being real number holds b1 . r = r ^2 ) & ( for r being real number holds b2 . r = r ^2 ) holds b1 = b2 proof let G1, G2 be UnOp of REAL; ::_thesis: ( ( for r being real number holds G1 . r = r ^2 ) & ( for r being real number holds G2 . r = r ^2 ) implies G1 = G2 ) assume that A2: for r being real number holds G1 . r = r ^2 and A3: for r being real number holds G2 . r = r ^2 ; ::_thesis: G1 = G2 now__::_thesis:_for_x_being_Element_of_REAL_holds_G1_._x_=_G2_._x let x be Element of REAL ; ::_thesis: G1 . x = G2 . x G1 . x = x ^2 by A2; hence G1 . x = G2 . x by A3; ::_thesis: verum end; hence G1 = G2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def2 defines sqrreal RVSUM_1:def_2_:_ for b1 being UnOp of REAL holds ( b1 = sqrreal iff for r being real number holds b1 . r = r ^2 ); theorem :: RVSUM_1:2 1 is_a_unity_wrt multreal by BINOP_2:7, SETWISEO:14; theorem Th3: :: RVSUM_1:3 multreal is_distributive_wrt addreal proof now__::_thesis:_for_x1,_x2,_x3_being_Element_of_REAL_holds_ (_multreal_._(x1,(addreal_._(x2,x3)))_=_addreal_._((multreal_._(x1,x2)),(multreal_._(x1,x3)))_&_multreal_._((addreal_._(x1,x2)),x3)_=_addreal_._((multreal_._(x1,x3)),(multreal_._(x2,x3)))_) let x1, x2, x3 be Element of REAL ; ::_thesis: ( multreal . (x1,(addreal . (x2,x3))) = addreal . ((multreal . (x1,x2)),(multreal . (x1,x3))) & multreal . ((addreal . (x1,x2)),x3) = addreal . ((multreal . (x1,x3)),(multreal . (x2,x3))) ) thus multreal . (x1,(addreal . (x2,x3))) = multreal . (x1,(x2 + x3)) by BINOP_2:def_9 .= x1 * (x2 + x3) by BINOP_2:def_11 .= (x1 * x2) + (x1 * x3) .= addreal . ((x1 * x2),(x1 * x3)) by BINOP_2:def_9 .= addreal . ((multreal . (x1,x2)),(x1 * x3)) by BINOP_2:def_11 .= addreal . ((multreal . (x1,x2)),(multreal . (x1,x3))) by BINOP_2:def_11 ; ::_thesis: multreal . ((addreal . (x1,x2)),x3) = addreal . ((multreal . (x1,x3)),(multreal . (x2,x3))) thus multreal . ((addreal . (x1,x2)),x3) = multreal . ((x1 + x2),x3) by BINOP_2:def_9 .= (x1 + x2) * x3 by BINOP_2:def_11 .= (x1 * x3) + (x2 * x3) .= addreal . ((x1 * x3),(x2 * x3)) by BINOP_2:def_9 .= addreal . ((multreal . (x1,x3)),(x2 * x3)) by BINOP_2:def_11 .= addreal . ((multreal . (x1,x3)),(multreal . (x2,x3))) by BINOP_2:def_11 ; ::_thesis: verum end; hence multreal is_distributive_wrt addreal by BINOP_1:11; ::_thesis: verum end; theorem :: RVSUM_1:4 sqrreal is_distributive_wrt multreal proof let x1 be Element of REAL ; :: according to BINOP_1:def_20 ::_thesis: for b1 being Element of REAL holds sqrreal . (multreal . (x1,b1)) = multreal . ((sqrreal . x1),(sqrreal . b1)) let x2 be Element of REAL ; ::_thesis: sqrreal . (multreal . (x1,x2)) = multreal . ((sqrreal . x1),(sqrreal . x2)) thus sqrreal . (multreal . (x1,x2)) = sqrreal . (x1 * x2) by BINOP_2:def_11 .= (x1 * x2) ^2 by Def2 .= (x1 ^2) * (x2 ^2) .= multreal . ((x1 ^2),(x2 ^2)) by BINOP_2:def_11 .= multreal . ((sqrreal . x1),(x2 ^2)) by Def2 .= multreal . ((sqrreal . x1),(sqrreal . x2)) by Def2 ; ::_thesis: verum end; definition let x be real number ; funcx multreal -> UnOp of REAL equals :: RVSUM_1:def 3 multreal [;] (x,(id REAL)); coherence multreal [;] (x,(id REAL)) is UnOp of REAL proof reconsider y = x as Real by XREAL_0:def_1; multreal [;] (y,(id REAL)) is UnOp of REAL ; hence multreal [;] (x,(id REAL)) is UnOp of REAL ; ::_thesis: verum end; end; :: deftheorem defines multreal RVSUM_1:def_3_:_ for x being real number holds x multreal = multreal [;] (x,(id REAL)); Lm1: for r, r1 being real number holds (multreal [;] (r,(id REAL))) . r1 = r * r1 proof let r, r1 be real number ; ::_thesis: (multreal [;] (r,(id REAL))) . r1 = r * r1 reconsider a = r, s = r1 as Element of REAL by XREAL_0:def_1; thus (multreal [;] (r,(id REAL))) . r1 = multreal . (a,((id REAL) . s)) by FUNCOP_1:53 .= multreal . (a,s) by FUNCT_1:18 .= r * r1 by BINOP_2:def_11 ; ::_thesis: verum end; theorem :: RVSUM_1:5 for r, r1 being real number holds (r multreal) . r1 = r * r1 by Lm1; theorem :: RVSUM_1:6 for r being real number holds r multreal is_distributive_wrt addreal proof let r be real number ; ::_thesis: r multreal is_distributive_wrt addreal r in REAL by XREAL_0:def_1; hence r multreal is_distributive_wrt addreal by Th3, FINSEQOP:54; ::_thesis: verum end; theorem Th7: :: RVSUM_1:7 compreal is_an_inverseOp_wrt addreal proof let x be Element of REAL ; :: according to FINSEQOP:def_1 ::_thesis: ( addreal . (x,(compreal . x)) = the_unity_wrt addreal & addreal . ((compreal . x),x) = the_unity_wrt addreal ) thus addreal . (x,(compreal . x)) = x + (compreal . x) by BINOP_2:def_9 .= x + (- x) by BINOP_2:def_7 .= the_unity_wrt addreal by BINOP_2:2 ; ::_thesis: addreal . ((compreal . x),x) = the_unity_wrt addreal thus addreal . ((compreal . x),x) = (compreal . x) + x by BINOP_2:def_9 .= (- x) + x by BINOP_2:def_7 .= the_unity_wrt addreal by BINOP_2:2 ; ::_thesis: verum end; theorem Th8: :: RVSUM_1:8 addreal is having_an_inverseOp by Th7, FINSEQOP:def_2; theorem Th9: :: RVSUM_1:9 the_inverseOp_wrt addreal = compreal by Th7, Th8, FINSEQOP:def_3; theorem :: RVSUM_1:10 compreal is_distributive_wrt addreal by Th8, Th9, FINSEQOP:63; Lm2: for F being real-valued FinSequence holds F is FinSequence of REAL proof let F be real-valued FinSequence; ::_thesis: F is FinSequence of REAL thus rng F c= REAL ; :: according to FINSEQ_1:def_4 ::_thesis: verum end; definition let F1, F2 be real-valued FinSequence; :: original: + redefine funcF1 + F2 -> FinSequence of REAL equals :: RVSUM_1:def 4 addreal .: (F1,F2); coherence F1 + F2 is FinSequence of REAL by Lm2; compatibility for b1 being FinSequence of REAL holds ( b1 = F1 + F2 iff b1 = addreal .: (F1,F2) ) proof reconsider F3 = F1, F4 = F2 as FinSequence of REAL by Lm2; let F be FinSequence of REAL ; ::_thesis: ( F = F1 + F2 iff F = addreal .: (F1,F2) ) dom addreal = [:REAL,REAL:] by FUNCT_2:def_1; then [:(rng F3),(rng F4):] c= dom addreal by ZFMISC_1:96; then A1: dom (addreal .: (F1,F2)) = (dom F1) /\ (dom F2) by FUNCOP_1:69; A2: dom (F1 + F2) = (dom F1) /\ (dom F2) by VALUED_1:def_1; thus ( F = F1 + F2 implies F = addreal .: (F1,F2) ) ::_thesis: ( F = addreal .: (F1,F2) implies F = F1 + F2 ) proof assume A3: F = F1 + F2 ; ::_thesis: F = addreal .: (F1,F2) for z being set st z in dom (addreal .: (F1,F2)) holds F . z = addreal . ((F1 . z),(F2 . z)) proof let z be set ; ::_thesis: ( z in dom (addreal .: (F1,F2)) implies F . z = addreal . ((F1 . z),(F2 . z)) ) assume z in dom (addreal .: (F1,F2)) ; ::_thesis: F . z = addreal . ((F1 . z),(F2 . z)) hence F . z = (F1 . z) + (F2 . z) by A2, A1, A3, VALUED_1:def_1 .= addreal . ((F1 . z),(F2 . z)) by BINOP_2:def_9 ; ::_thesis: verum end; hence F = addreal .: (F1,F2) by A2, A1, A3, FUNCOP_1:21; ::_thesis: verum end; assume A4: F = addreal .: (F1,F2) ; ::_thesis: F = F1 + F2 now__::_thesis:_for_c_being_set_st_c_in_dom_F_holds_ F_._c_=_(F1_._c)_+_(F2_._c) let c be set ; ::_thesis: ( c in dom F implies F . c = (F1 . c) + (F2 . c) ) assume c in dom F ; ::_thesis: F . c = (F1 . c) + (F2 . c) hence F . c = addreal . ((F1 . c),(F2 . c)) by A4, FUNCOP_1:22 .= (F1 . c) + (F2 . c) by BINOP_2:def_9 ; ::_thesis: verum end; hence F = F1 + F2 by A1, A4, VALUED_1:def_1; ::_thesis: verum end; commutativity for b1 being FinSequence of REAL for F1, F2 being real-valued FinSequence st b1 = addreal .: (F1,F2) holds b1 = addreal .: (F2,F1) proof let F be FinSequence of REAL ; ::_thesis: for F1, F2 being real-valued FinSequence st F = addreal .: (F1,F2) holds F = addreal .: (F2,F1) let F1, F2 be real-valued FinSequence; ::_thesis: ( F = addreal .: (F1,F2) implies F = addreal .: (F2,F1) ) assume A5: F = addreal .: (F1,F2) ; ::_thesis: F = addreal .: (F2,F1) reconsider F1 = F1, F2 = F2 as FinSequence of REAL by Lm2; A6: dom addreal = [:REAL,REAL:] by FUNCT_2:def_1; then A7: [:(rng F2),(rng F1):] c= dom addreal by ZFMISC_1:96; [:(rng F1),(rng F2):] c= dom addreal by A6, ZFMISC_1:96; then A8: dom (addreal .: (F1,F2)) = (dom F1) /\ (dom F2) by FUNCOP_1:69 .= dom (addreal .: (F2,F1)) by A7, FUNCOP_1:69 ; for z being set st z in dom (addreal .: (F2,F1)) holds F . z = addreal . ((F2 . z),(F1 . z)) proof let z be set ; ::_thesis: ( z in dom (addreal .: (F2,F1)) implies F . z = addreal . ((F2 . z),(F1 . z)) ) assume z in dom (addreal .: (F2,F1)) ; ::_thesis: F . z = addreal . ((F2 . z),(F1 . z)) hence F . z = addreal . ((F1 . z),(F2 . z)) by A5, A8, FUNCOP_1:22 .= (F1 . z) + (F2 . z) by BINOP_2:def_9 .= addreal . ((F2 . z),(F1 . z)) by BINOP_2:def_9 ; ::_thesis: verum end; hence F = addreal .: (F2,F1) by A5, A8, FUNCOP_1:21; ::_thesis: verum end; end; :: deftheorem defines + RVSUM_1:def_4_:_ for F1, F2 being real-valued FinSequence holds F1 + F2 = addreal .: (F1,F2); definition let i be Nat; let R1, R2 be Element of i -tuples_on REAL; :: original: + redefine funcR1 + R2 -> Element of i -tuples_on REAL; coherence R1 + R2 is Element of i -tuples_on REAL by FINSEQ_2:120; end; theorem :: RVSUM_1:11 for s being set for i being Nat for R1, R2 being Element of i -tuples_on REAL holds (R1 + R2) . s = (R1 . s) + (R2 . s) proof let s be set ; ::_thesis: for i being Nat for R1, R2 being Element of i -tuples_on REAL holds (R1 + R2) . s = (R1 . s) + (R2 . s) let i be Nat; ::_thesis: for R1, R2 being Element of i -tuples_on REAL holds (R1 + R2) . s = (R1 . s) + (R2 . s) let R1, R2 be Element of i -tuples_on REAL; ::_thesis: (R1 + R2) . s = (R1 . s) + (R2 . s) percases ( not s in Seg i or s in Seg i ) ; supposeA1: not s in Seg i ; ::_thesis: (R1 + R2) . s = (R1 . s) + (R2 . s) then A2: not s in dom R2 by FINSEQ_2:124; A3: not s in dom R1 by A1, FINSEQ_2:124; not s in dom (R1 + R2) by A1, FINSEQ_2:124; hence (R1 + R2) . s = 0 + 0 by FUNCT_1:def_2 .= (R1 . s) + 0 by A3, FUNCT_1:def_2 .= (R1 . s) + (R2 . s) by A2, FUNCT_1:def_2 ; ::_thesis: verum end; suppose s in Seg i ; ::_thesis: (R1 + R2) . s = (R1 . s) + (R2 . s) then s in dom (R1 + R2) by FINSEQ_2:124; hence (R1 + R2) . s = (R1 . s) + (R2 . s) by VALUED_1:def_1; ::_thesis: verum end; end; end; theorem :: RVSUM_1:12 for F being real-valued FinSequence holds (<*> REAL) + F = <*> REAL proof let F be real-valued FinSequence; ::_thesis: (<*> REAL) + F = <*> REAL F is FinSequence of REAL by Lm2; hence (<*> REAL) + F = <*> REAL by FINSEQ_2:73; ::_thesis: verum end; theorem :: RVSUM_1:13 for r1, r2 being real number holds <*r1*> + <*r2*> = <*(r1 + r2)*> proof let r1, r2 be real number ; ::_thesis: <*r1*> + <*r2*> = <*(r1 + r2)*> reconsider s1 = r1, s2 = r2 as Element of REAL by XREAL_0:def_1; <*s1*> + <*s2*> = <*(addreal . (s1,s2))*> by FINSEQ_2:74 .= <*(r1 + r2)*> by BINOP_2:def_9 ; hence <*r1*> + <*r2*> = <*(r1 + r2)*> ; ::_thesis: verum end; theorem :: RVSUM_1:14 for i being Nat for r1, r2 being real number holds (i |-> r1) + (i |-> r2) = i |-> (r1 + r2) proof let i be Nat; ::_thesis: for r1, r2 being real number holds (i |-> r1) + (i |-> r2) = i |-> (r1 + r2) let r1, r2 be real number ; ::_thesis: (i |-> r1) + (i |-> r2) = i |-> (r1 + r2) reconsider s1 = r1, s2 = r2 as Element of REAL by XREAL_0:def_1; (i |-> s1) + (i |-> s2) = i |-> (addreal . (s1,s2)) by FINSEQOP:17 .= i |-> (r1 + r2) by BINOP_2:def_9 ; hence (i |-> r1) + (i |-> r2) = i |-> (r1 + r2) ; ::_thesis: verum end; theorem :: RVSUM_1:15 for F1, F2, F3 being real-valued FinSequence holds F1 + (F2 + F3) = (F1 + F2) + F3 by RFUNCT_1:8; theorem :: RVSUM_1:16 for i being Nat for R being Element of i -tuples_on REAL holds R + (i |-> 0) = R by BINOP_2:2, FINSEQOP:56; theorem :: RVSUM_1:17 for s being set for F being real-valued FinSequence holds (- F) . s = - (F . s) by VALUED_1:8; definition let F be real-valued FinSequence; :: original: - redefine func - F -> FinSequence of REAL equals :: RVSUM_1:def 5 compreal * F; coherence - F is FinSequence of REAL by Lm2; compatibility for b1 being FinSequence of REAL holds ( b1 = - F iff b1 = compreal * F ) proof let F1 be FinSequence of REAL ; ::_thesis: ( F1 = - F iff F1 = compreal * F ) A1: dom (- F) = dom F by VALUED_1:8; A2: ( rng F c= REAL & dom compreal = REAL ) by FUNCT_2:def_1; then A3: dom (compreal * F) = dom F by RELAT_1:27; thus ( F1 = - F implies F1 = compreal * F ) ::_thesis: ( F1 = compreal * F implies F1 = - F ) proof assume A4: F1 = - F ; ::_thesis: F1 = compreal * F now__::_thesis:_for_c_being_set_st_c_in_dom_F1_holds_ F1_._c_=_(compreal_*_F)_._c let c be set ; ::_thesis: ( c in dom F1 implies F1 . c = (compreal * F) . c ) assume A5: c in dom F1 ; ::_thesis: F1 . c = (compreal * F) . c thus F1 . c = - (F . c) by A4, VALUED_1:8 .= compreal . (F . c) by BINOP_2:def_7 .= (compreal * F) . c by A1, A4, A5, FUNCT_1:13 ; ::_thesis: verum end; hence F1 = compreal * F by A3, A4, FUNCT_1:2, VALUED_1:8; ::_thesis: verum end; assume A6: F1 = compreal * F ; ::_thesis: F1 = - F now__::_thesis:_for_c_being_set_st_c_in_dom_F1_holds_ (-_F)_._c_=_(compreal_*_F)_._c let c be set ; ::_thesis: ( c in dom F1 implies (- F) . c = (compreal * F) . c ) assume A7: c in dom F1 ; ::_thesis: (- F) . c = (compreal * F) . c thus (- F) . c = - (F . c) by VALUED_1:8 .= compreal . (F . c) by BINOP_2:def_7 .= (compreal * F) . c by A6, A7, FUNCT_1:12 ; ::_thesis: verum end; hence F1 = - F by A1, A2, A6, FUNCT_1:2, RELAT_1:27; ::_thesis: verum end; end; :: deftheorem defines - RVSUM_1:def_5_:_ for F being real-valued FinSequence holds - F = compreal * F; definition let i be Nat; let R be Element of i -tuples_on REAL; :: original: - redefine func - R -> Element of i -tuples_on REAL; coherence - R is Element of i -tuples_on REAL by FINSEQ_2:113; end; theorem :: RVSUM_1:18 for s being set for F being real-valued FinSequence holds (- F) . s = - (F . s) by VALUED_1:8; theorem :: RVSUM_1:19 - (<*> REAL) = <*> REAL ; theorem :: RVSUM_1:20 for r being real number holds - <*r*> = <*(- r)*> proof let r be real number ; ::_thesis: - <*r*> = <*(- r)*> reconsider s = r as Element of REAL by XREAL_0:def_1; - <*s*> = <*(compreal . s)*> by FINSEQ_2:35 .= <*(- r)*> by BINOP_2:def_7 ; hence - <*r*> = <*(- r)*> ; ::_thesis: verum end; theorem Th21: :: RVSUM_1:21 for i being Nat for r being real number holds - (i |-> r) = i |-> (- r) proof let i be Nat; ::_thesis: for r being real number holds - (i |-> r) = i |-> (- r) let r be real number ; ::_thesis: - (i |-> r) = i |-> (- r) reconsider s = r as Element of REAL by XREAL_0:def_1; - (i |-> s) = i |-> (compreal . s) by FINSEQOP:16 .= i |-> (- r) by BINOP_2:def_7 ; hence - (i |-> r) = i |-> (- r) ; ::_thesis: verum end; theorem :: RVSUM_1:22 for i being Nat for R being Element of i -tuples_on REAL holds R + (- R) = i |-> 0 by Th8, Th9, BINOP_2:2, FINSEQOP:73; theorem :: RVSUM_1:23 for i being Nat for R1, R2 being Element of i -tuples_on REAL st R1 + R2 = i |-> 0 holds R1 = - R2 by Th8, Th9, BINOP_2:2, FINSEQOP:74; theorem :: RVSUM_1:24 for R1, R2 being complex-valued Function st - R1 = - R2 holds R1 = R2 proof let R1, R2 be complex-valued Function; ::_thesis: ( - R1 = - R2 implies R1 = R2 ) assume - R1 = - R2 ; ::_thesis: R1 = R2 hence R1 = - (- R2) .= R2 ; ::_thesis: verum end; theorem :: RVSUM_1:25 for i being Nat for R1, R, R2 being Element of i -tuples_on REAL st R1 + R = R2 + R holds R1 = R2 proof let i be Nat; ::_thesis: for R1, R, R2 being Element of i -tuples_on REAL st R1 + R = R2 + R holds R1 = R2 let R1, R, R2 be Element of i -tuples_on REAL; ::_thesis: ( R1 + R = R2 + R implies R1 = R2 ) assume R1 + R = R2 + R ; ::_thesis: R1 = R2 then R1 + (R + (- R)) = (R2 + R) + (- R) by FINSEQOP:28; then A1: R1 + (R + (- R)) = R2 + (R + (- R)) by FINSEQOP:28; R + (- R) = i |-> 0 by Th8, Th9, BINOP_2:2, FINSEQOP:73; then R1 = R2 + (i |-> 0) by A1, BINOP_2:2, FINSEQOP:56; hence R1 = R2 by BINOP_2:2, FINSEQOP:56; ::_thesis: verum end; theorem Th26: :: RVSUM_1:26 for F1, F2 being real-valued FinSequence holds - (F1 + F2) = (- F1) + (- F2) proof let F1, F2 be real-valued FinSequence; ::_thesis: - (F1 + F2) = (- F1) + (- F2) A1: dom (- (F1 + F2)) = dom (F1 + F2) by VALUED_1:8; A2: dom (F1 + F2) = (dom F1) /\ (dom F2) by VALUED_1:def_1; A3: dom ((- F1) + (- F2)) = (dom (- F1)) /\ (dom (- F2)) by VALUED_1:def_1 .= (dom F1) /\ (dom (- F2)) by VALUED_1:8 .= (dom F1) /\ (dom F2) by VALUED_1:8 ; now__::_thesis:_for_i_being_Nat_st_i_in_dom_(-_(F1_+_F2))_holds_ (-_(F1_+_F2))_._i_=_((-_F1)_+_(-_F2))_._i let i be Nat; ::_thesis: ( i in dom (- (F1 + F2)) implies (- (F1 + F2)) . i = ((- F1) + (- F2)) . i ) assume A4: i in dom (- (F1 + F2)) ; ::_thesis: (- (F1 + F2)) . i = ((- F1) + (- F2)) . i thus (- (F1 + F2)) . i = - ((F1 + F2) . i) by VALUED_1:8 .= - ((F1 . i) + (F2 . i)) by A1, A4, VALUED_1:def_1 .= (- (F1 . i)) + (- (F2 . i)) .= (- (F1 . i)) + ((- F2) . i) by VALUED_1:8 .= ((- F1) . i) + ((- F2) . i) by VALUED_1:8 .= ((- F1) + (- F2)) . i by A1, A2, A3, A4, VALUED_1:def_1 ; ::_thesis: verum end; hence - (F1 + F2) = (- F1) + (- F2) by A2, A3, FINSEQ_1:13, VALUED_1:8; ::_thesis: verum end; definition let F1, F2 be real-valued FinSequence; :: original: - redefine funcF1 - F2 -> FinSequence of REAL equals :: RVSUM_1:def 6 diffreal .: (F1,F2); coherence F1 - F2 is FinSequence of REAL by Lm2; compatibility for b1 being FinSequence of REAL holds ( b1 = F1 - F2 iff b1 = diffreal .: (F1,F2) ) proof reconsider F3 = F1, F4 = F2 as FinSequence of REAL by Lm2; let F be FinSequence of REAL ; ::_thesis: ( F = F1 - F2 iff F = diffreal .: (F1,F2) ) A1: dom (F1 - F2) = (dom F1) /\ (dom F2) by VALUED_1:12; dom diffreal = [:REAL,REAL:] by FUNCT_2:def_1; then A2: [:(rng F3),(rng F4):] c= dom diffreal by ZFMISC_1:96; then A3: dom (diffreal .: (F1,F2)) = (dom F1) /\ (dom F2) by FUNCOP_1:69; thus ( F = F1 - F2 implies F = diffreal .: (F1,F2) ) ::_thesis: ( F = diffreal .: (F1,F2) implies F = F1 - F2 ) proof assume A4: F = F1 - F2 ; ::_thesis: F = diffreal .: (F1,F2) for z being set st z in dom (diffreal .: (F1,F2)) holds F . z = diffreal . ((F1 . z),(F2 . z)) proof let z be set ; ::_thesis: ( z in dom (diffreal .: (F1,F2)) implies F . z = diffreal . ((F1 . z),(F2 . z)) ) assume z in dom (diffreal .: (F1,F2)) ; ::_thesis: F . z = diffreal . ((F1 . z),(F2 . z)) hence F . z = (F1 . z) - (F2 . z) by A1, A3, A4, VALUED_1:13 .= diffreal . ((F1 . z),(F2 . z)) by BINOP_2:def_10 ; ::_thesis: verum end; hence F = diffreal .: (F1,F2) by A1, A3, A4, FUNCOP_1:21; ::_thesis: verum end; assume A5: F = diffreal .: (F1,F2) ; ::_thesis: F = F1 - F2 now__::_thesis:_for_c_being_set_st_c_in_dom_F_holds_ F_._c_=_(F1_._c)_-_(F2_._c) let c be set ; ::_thesis: ( c in dom F implies F . c = (F1 . c) - (F2 . c) ) assume c in dom F ; ::_thesis: F . c = (F1 . c) - (F2 . c) hence F . c = diffreal . ((F1 . c),(F2 . c)) by A5, FUNCOP_1:22 .= (F1 . c) - (F2 . c) by BINOP_2:def_10 ; ::_thesis: verum end; hence F = F1 - F2 by A1, A2, A5, FUNCOP_1:69, VALUED_1:14; ::_thesis: verum end; end; :: deftheorem defines - RVSUM_1:def_6_:_ for F1, F2 being real-valued FinSequence holds F1 - F2 = diffreal .: (F1,F2); definition let i be Nat; let R1, R2 be Element of i -tuples_on REAL; :: original: - redefine funcR1 - R2 -> Element of i -tuples_on REAL; coherence R1 - R2 is Element of i -tuples_on REAL by FINSEQ_2:120; end; theorem :: RVSUM_1:27 for s being set for i being Nat for R1, R2 being Element of i -tuples_on REAL holds (R1 - R2) . s = (R1 . s) - (R2 . s) proof let s be set ; ::_thesis: for i being Nat for R1, R2 being Element of i -tuples_on REAL holds (R1 - R2) . s = (R1 . s) - (R2 . s) let i be Nat; ::_thesis: for R1, R2 being Element of i -tuples_on REAL holds (R1 - R2) . s = (R1 . s) - (R2 . s) let R1, R2 be Element of i -tuples_on REAL; ::_thesis: (R1 - R2) . s = (R1 . s) - (R2 . s) percases ( not s in Seg i or s in Seg i ) ; supposeA1: not s in Seg i ; ::_thesis: (R1 - R2) . s = (R1 . s) - (R2 . s) then A2: not s in dom R2 by FINSEQ_2:124; A3: not s in dom R1 by A1, FINSEQ_2:124; not s in dom (R1 - R2) by A1, FINSEQ_2:124; hence (R1 - R2) . s = 0 - 0 by FUNCT_1:def_2 .= (R1 . s) - 0 by A3, FUNCT_1:def_2 .= (R1 . s) - (R2 . s) by A2, FUNCT_1:def_2 ; ::_thesis: verum end; suppose s in Seg i ; ::_thesis: (R1 - R2) . s = (R1 . s) - (R2 . s) then s in dom (R1 - R2) by FINSEQ_2:124; hence (R1 - R2) . s = (R1 . s) - (R2 . s) by VALUED_1:13; ::_thesis: verum end; end; end; theorem :: RVSUM_1:28 for F being real-valued FinSequence holds ( (<*> REAL) - F = <*> REAL & F - (<*> REAL) = <*> REAL ) proof let F be real-valued FinSequence; ::_thesis: ( (<*> REAL) - F = <*> REAL & F - (<*> REAL) = <*> REAL ) F is FinSequence of REAL by Lm2; hence ( (<*> REAL) - F = <*> REAL & F - (<*> REAL) = <*> REAL ) by FINSEQ_2:73; ::_thesis: verum end; theorem :: RVSUM_1:29 for r1, r2 being real number holds <*r1*> - <*r2*> = <*(r1 - r2)*> proof let r1, r2 be real number ; ::_thesis: <*r1*> - <*r2*> = <*(r1 - r2)*> reconsider s1 = r1, s2 = r2 as Element of REAL by XREAL_0:def_1; <*s1*> - <*s2*> = <*(diffreal . (s1,s2))*> by FINSEQ_2:74 .= <*(r1 - r2)*> by BINOP_2:def_10 ; hence <*r1*> - <*r2*> = <*(r1 - r2)*> ; ::_thesis: verum end; theorem :: RVSUM_1:30 for i being Nat for r1, r2 being real number holds (i |-> r1) - (i |-> r2) = i |-> (r1 - r2) proof let i be Nat; ::_thesis: for r1, r2 being real number holds (i |-> r1) - (i |-> r2) = i |-> (r1 - r2) let r1, r2 be real number ; ::_thesis: (i |-> r1) - (i |-> r2) = i |-> (r1 - r2) reconsider s1 = r1, s2 = r2 as Element of REAL by XREAL_0:def_1; (i |-> s1) - (i |-> s2) = i |-> (diffreal . (s1,s2)) by FINSEQOP:17 .= i |-> (r1 - r2) by BINOP_2:def_10 ; hence (i |-> r1) - (i |-> r2) = i |-> (r1 - r2) ; ::_thesis: verum end; theorem :: RVSUM_1:31 for F1, F2 being real-valued FinSequence holds F1 - F2 = F1 + (- F2) ; theorem :: RVSUM_1:32 for i being Nat for R being Element of i -tuples_on REAL holds R - (i |-> 0) = R proof let i be Nat; ::_thesis: for R being Element of i -tuples_on REAL holds R - (i |-> 0) = R let R be Element of i -tuples_on REAL; ::_thesis: R - (i |-> 0) = R thus R - (i |-> 0) = R + (i |-> (- 0)) by Th21 .= R by BINOP_2:2, FINSEQOP:56 ; ::_thesis: verum end; theorem :: RVSUM_1:33 for i being Nat for R being Element of i -tuples_on REAL holds (i |-> 0) - R = - R by BINOP_2:2, FINSEQOP:56; theorem :: RVSUM_1:34 for F1, F2 being real-valued FinSequence holds F1 - (- F2) = F1 + F2 ; theorem :: RVSUM_1:35 for F1, F2 being real-valued FinSequence holds - (F1 - F2) = F2 - F1 proof let F1, F2 be real-valued FinSequence; ::_thesis: - (F1 - F2) = F2 - F1 thus - (F1 - F2) = (- F1) + (- (- F2)) by Th26 .= F2 - F1 ; ::_thesis: verum end; theorem :: RVSUM_1:36 for F1, F2 being real-valued FinSequence holds - (F1 - F2) = (- F1) + F2 proof let F1, F2 be real-valued FinSequence; ::_thesis: - (F1 - F2) = (- F1) + F2 thus - (F1 - F2) = (- F1) + (- (- F2)) by Th26 .= (- F1) + F2 ; ::_thesis: verum end; theorem :: RVSUM_1:37 for i being Nat for R being Element of i -tuples_on REAL holds R - R = i |-> 0 by Th8, Th9, BINOP_2:2, FINSEQOP:73; theorem :: RVSUM_1:38 for i being Nat for R1, R2 being Element of i -tuples_on REAL st R1 - R2 = i |-> 0 holds R1 = R2 proof let i be Nat; ::_thesis: for R1, R2 being Element of i -tuples_on REAL st R1 - R2 = i |-> 0 holds R1 = R2 let R1, R2 be Element of i -tuples_on REAL; ::_thesis: ( R1 - R2 = i |-> 0 implies R1 = R2 ) assume R1 - R2 = i |-> 0 ; ::_thesis: R1 = R2 then R1 = - (- R2) by Th8, Th9, BINOP_2:2, FINSEQOP:74; hence R1 = R2 ; ::_thesis: verum end; theorem :: RVSUM_1:39 for F1, F2, F3 being real-valued FinSequence holds (F1 - F2) - F3 = F1 - (F2 + F3) by RFUNCT_1:20; theorem :: RVSUM_1:40 for F1, F2, F3 being real-valued FinSequence holds F1 + (F2 - F3) = (F1 + F2) - F3 by RFUNCT_1:23; theorem :: RVSUM_1:41 for F1, F2, F3 being real-valued FinSequence holds F1 - (F2 - F3) = (F1 - F2) + F3 by RFUNCT_1:22; theorem :: RVSUM_1:42 for i being Nat for R1, R being Element of i -tuples_on REAL holds R1 = (R1 + R) - R proof let i be Nat; ::_thesis: for R1, R being Element of i -tuples_on REAL holds R1 = (R1 + R) - R let R1, R be Element of i -tuples_on REAL; ::_thesis: R1 = (R1 + R) - R thus R1 = R1 + (i |-> 0) by BINOP_2:2, FINSEQOP:56 .= R1 + (R - R) by Th8, Th9, BINOP_2:2, FINSEQOP:73 .= (R1 + R) - R by RFUNCT_1:23 ; ::_thesis: verum end; theorem :: RVSUM_1:43 for i being Nat for R1, R being Element of i -tuples_on REAL holds R1 = (R1 - R) + R proof let i be Nat; ::_thesis: for R1, R being Element of i -tuples_on REAL holds R1 = (R1 - R) + R let R1, R be Element of i -tuples_on REAL; ::_thesis: R1 = (R1 - R) + R thus R1 = R1 + (i |-> 0) by BINOP_2:2, FINSEQOP:56 .= R1 + ((- R) + R) by Th8, Th9, BINOP_2:2, FINSEQOP:73 .= (R1 - R) + R by FINSEQOP:28 ; ::_thesis: verum end; notation let F be real-valued FinSequence; let r be real number ; synonym r * F for r (#) F; end; theorem :: RVSUM_1:44 for s being set for r being real number for F being real-valued FinSequence holds (r * F) . s = r * (F . s) by VALUED_1:6; definition let F be real-valued FinSequence; let r be real number ; :: original: * redefine funcr * F -> FinSequence of REAL equals :: RVSUM_1:def 7 (r multreal) * F; coherence r * F is FinSequence of REAL by Lm2; compatibility for b1 being FinSequence of REAL holds ( b1 = r * F iff b1 = (r multreal) * F ) proof let F1 be FinSequence of REAL ; ::_thesis: ( F1 = r * F iff F1 = (r multreal) * F ) A1: dom (r * F) = dom F by VALUED_1:def_5; A2: ( rng F c= REAL & dom (r multreal) = REAL ) by FUNCT_2:def_1; then A3: dom ((r multreal) * F) = dom F by RELAT_1:27; thus ( F1 = r * F implies F1 = (r multreal) * F ) ::_thesis: ( F1 = (r multreal) * F implies F1 = r * F ) proof assume A4: F1 = r * F ; ::_thesis: F1 = (r multreal) * F now__::_thesis:_for_c_being_set_st_c_in_dom_F1_holds_ F1_._c_=_((r_multreal)_*_F)_._c let c be set ; ::_thesis: ( c in dom F1 implies F1 . c = ((r multreal) * F) . c ) assume A5: c in dom F1 ; ::_thesis: F1 . c = ((r multreal) * F) . c hence F1 . c = r * (F . c) by A4, VALUED_1:def_5 .= (r multreal) . (F . c) by Lm1 .= ((r multreal) * F) . c by A1, A4, A5, FUNCT_1:13 ; ::_thesis: verum end; hence F1 = (r multreal) * F by A1, A3, A4, FUNCT_1:2; ::_thesis: verum end; assume A6: F1 = (r multreal) * F ; ::_thesis: F1 = r * F now__::_thesis:_for_c_being_set_st_c_in_dom_F1_holds_ (r_*_F)_._c_=_((r_multreal)_*_F)_._c let c be set ; ::_thesis: ( c in dom F1 implies (r * F) . c = ((r multreal) * F) . c ) assume A7: c in dom F1 ; ::_thesis: (r * F) . c = ((r multreal) * F) . c thus (r * F) . c = r * (F . c) by VALUED_1:6 .= (r multreal) . (F . c) by Lm1 .= ((r multreal) * F) . c by A6, A7, FUNCT_1:12 ; ::_thesis: verum end; hence F1 = r * F by A1, A2, A6, FUNCT_1:2, RELAT_1:27; ::_thesis: verum end; end; :: deftheorem defines * RVSUM_1:def_7_:_ for F being real-valued FinSequence for r being real number holds r * F = (r multreal) * F; definition let i be Nat; let R be Element of i -tuples_on REAL; let r be real number ; :: original: * redefine funcr * R -> Element of i -tuples_on REAL; coherence r * R is Element of i -tuples_on REAL by FINSEQ_2:113; end; theorem :: RVSUM_1:45 for s being set for r being real number for F being real-valued FinSequence holds (r * F) . s = r * (F . s) by VALUED_1:6; theorem :: RVSUM_1:46 for r being real number holds r * (<*> REAL) = <*> REAL ; theorem :: RVSUM_1:47 for r, r1 being real number holds r * <*r1*> = <*(r * r1)*> proof let r, r1 be real number ; ::_thesis: r * <*r1*> = <*(r * r1)*> reconsider s = r, s1 = r1 as Element of REAL by XREAL_0:def_1; s * <*s1*> = <*((multreal [;] (s,(id REAL))) . s1)*> by FINSEQ_2:35 .= <*(r * r1)*> by Lm1 ; hence r * <*r1*> = <*(r * r1)*> ; ::_thesis: verum end; theorem Th48: :: RVSUM_1:48 for i being Nat for r1, r2 being real number holds r1 * (i |-> r2) = i |-> (r1 * r2) proof let i be Nat; ::_thesis: for r1, r2 being real number holds r1 * (i |-> r2) = i |-> (r1 * r2) let r1, r2 be real number ; ::_thesis: r1 * (i |-> r2) = i |-> (r1 * r2) reconsider s1 = r1, s2 = r2 as Element of REAL by XREAL_0:def_1; s1 * (i |-> s2) = i |-> ((multreal [;] (s1,(id REAL))) . s2) by FINSEQOP:16 .= i |-> (r1 * r2) by Lm1 ; hence r1 * (i |-> r2) = i |-> (r1 * r2) ; ::_thesis: verum end; theorem :: RVSUM_1:49 for r1, r2 being real number for F being real-valued FinSequence holds (r1 * r2) * F = r1 * (r2 * F) by RFUNCT_1:17; theorem :: RVSUM_1:50 for r1, r2 being real number for F being real-valued FinSequence holds (r1 + r2) * F = (r1 * F) + (r2 * F) proof let r1, r2 be real number ; ::_thesis: for F being real-valued FinSequence holds (r1 + r2) * F = (r1 * F) + (r2 * F) let F be real-valued FinSequence; ::_thesis: (r1 + r2) * F = (r1 * F) + (r2 * F) A1: dom ((r1 + r2) * F) = dom F by VALUED_1:def_5; A2: dom ((r1 * F) + (r2 * F)) = (dom (r1 * F)) /\ (dom (r2 * F)) by VALUED_1:def_1; A3: dom (r1 * F) = dom F by VALUED_1:def_5; A4: dom (r2 * F) = dom F by VALUED_1:def_5; now__::_thesis:_for_i_being_Nat_st_i_in_dom_((r1_+_r2)_*_F)_holds_ ((r1_+_r2)_*_F)_._i_=_((r1_*_F)_+_(r2_*_F))_._i let i be Nat; ::_thesis: ( i in dom ((r1 + r2) * F) implies ((r1 + r2) * F) . i = ((r1 * F) + (r2 * F)) . i ) assume A5: i in dom ((r1 + r2) * F) ; ::_thesis: ((r1 + r2) * F) . i = ((r1 * F) + (r2 * F)) . i thus ((r1 + r2) * F) . i = (r1 + r2) * (F . i) by VALUED_1:6 .= (r1 * (F . i)) + (r2 * (F . i)) .= (r1 * (F . i)) + ((r2 * F) . i) by VALUED_1:6 .= ((r1 * F) . i) + ((r2 * F) . i) by VALUED_1:6 .= ((r1 * F) + (r2 * F)) . i by A1, A2, A3, A4, A5, VALUED_1:def_1 ; ::_thesis: verum end; hence (r1 + r2) * F = (r1 * F) + (r2 * F) by A1, A2, A3, A4, FINSEQ_1:13; ::_thesis: verum end; theorem :: RVSUM_1:51 for r being real number for F1, F2 being real-valued FinSequence holds r * (F1 + F2) = (r * F1) + (r * F2) by RFUNCT_1:16; theorem :: RVSUM_1:52 for F being real-valued FinSequence holds 1 * F = F by RFUNCT_1:21; theorem :: RVSUM_1:53 for i being Nat for R being Element of i -tuples_on REAL holds 0 * R = i |-> 0 proof let i be Nat; ::_thesis: for R being Element of i -tuples_on REAL holds 0 * R = i |-> 0 let R be Element of i -tuples_on REAL; ::_thesis: 0 * R = i |-> 0 A1: rng R c= REAL ; thus 0 * R = multreal [;] (0,((id REAL) * R)) by FUNCOP_1:34 .= multreal [;] (0,R) by A1, RELAT_1:53 .= i |-> 0 by Th3, Th8, BINOP_2:2, FINSEQOP:76 ; ::_thesis: verum end; theorem :: RVSUM_1:54 for F being real-valued FinSequence holds (- 1) * F = - F ; notation let F be real-valued FinSequence; synonym sqr F for F ^2 ; end; definition let F be real-valued FinSequence; :: original: sqr redefine func sqr F -> FinSequence of REAL equals :: RVSUM_1:def 8 sqrreal * F; compatibility for b1 being FinSequence of REAL holds ( b1 = sqr F iff b1 = sqrreal * F ) proof let f be FinSequence of REAL ; ::_thesis: ( f = sqr F iff f = sqrreal * F ) sqr F = sqrreal * F proof dom sqrreal = REAL by FUNCT_2:def_1; then A1: rng F c= dom sqrreal ; A2: dom (sqr F) = dom F by VALUED_1:11 .= dom (sqrreal * F) by A1, RELAT_1:27 ; hence len (sqr F) = len (sqrreal * F) by FINSEQ_3:29; :: according to FINSEQ_1:def_17 ::_thesis: for b1 being set holds ( not 1 <= b1 or not b1 <= len (sqr F) or (sqr F) . b1 = (sqrreal * F) . b1 ) let k be Nat; ::_thesis: ( not 1 <= k or not k <= len (sqr F) or (sqr F) . k = (sqrreal * F) . k ) assume ( 1 <= k & k <= len (sqr F) ) ; ::_thesis: (sqr F) . k = (sqrreal * F) . k then A3: k in dom (sqr F) by FINSEQ_3:25; thus (sqr F) . k = (F . k) ^2 by VALUED_1:11 .= sqrreal . (F . k) by Def2 .= (sqrreal * F) . k by A2, A3, FUNCT_1:12 ; ::_thesis: verum end; hence ( f = sqr F iff f = sqrreal * F ) ; ::_thesis: verum end; coherence sqr F is FinSequence of REAL by Lm2; end; :: deftheorem defines sqr RVSUM_1:def_8_:_ for F being real-valued FinSequence holds sqr F = sqrreal * F; definition let i be Nat; let R be Element of i -tuples_on REAL; :: original: sqr redefine func sqr R -> Element of i -tuples_on REAL; coherence sqr R is Element of i -tuples_on REAL by FINSEQ_2:113; end; theorem :: RVSUM_1:55 for r being real number holds sqr <*r*> = <*(r ^2)*> proof let r be real number ; ::_thesis: sqr <*r*> = <*(r ^2)*> reconsider s = r as Element of REAL by XREAL_0:def_1; sqr <*s*> = <*(sqrreal . s)*> by FINSEQ_2:35 .= <*(r ^2)*> by Def2 ; hence sqr <*r*> = <*(r ^2)*> ; ::_thesis: verum end; theorem :: RVSUM_1:56 for i being Nat for r being real number holds sqr (i |-> r) = i |-> (r ^2) proof let i be Nat; ::_thesis: for r being real number holds sqr (i |-> r) = i |-> (r ^2) let r be real number ; ::_thesis: sqr (i |-> r) = i |-> (r ^2) reconsider s = r as Element of REAL by XREAL_0:def_1; sqr (i |-> s) = i |-> (sqrreal . s) by FINSEQOP:16 .= i |-> (r ^2) by Def2 ; hence sqr (i |-> r) = i |-> (r ^2) ; ::_thesis: verum end; theorem Th57: :: RVSUM_1:57 for F being real-valued FinSequence holds sqr (- F) = sqr F proof let F be real-valued FinSequence; ::_thesis: sqr (- F) = sqr F A1: dom (sqr (- F)) = dom (- F) by VALUED_1:11 .= dom F by VALUED_1:8 ; A2: dom (sqr F) = dom F by VALUED_1:11; now__::_thesis:_for_j_being_Nat_st_j_in_dom_(sqr_(-_F))_holds_ (sqr_(-_F))_._j_=_(sqr_F)_._j let j be Nat; ::_thesis: ( j in dom (sqr (- F)) implies (sqr (- F)) . j = (sqr F) . j ) assume j in dom (sqr (- F)) ; ::_thesis: (sqr (- F)) . j = (sqr F) . j set r = F . j; set r9 = (- F) . j; thus (sqr (- F)) . j = ((- F) . j) ^2 by VALUED_1:11 .= (- (F . j)) ^2 by VALUED_1:8 .= (F . j) ^2 .= (sqr F) . j by VALUED_1:11 ; ::_thesis: verum end; hence sqr (- F) = sqr F by A1, A2, FINSEQ_1:13; ::_thesis: verum end; theorem Th58: :: RVSUM_1:58 for r being real number for F being real-valued FinSequence holds sqr (r * F) = (r ^2) * (sqr F) proof let r be real number ; ::_thesis: for F being real-valued FinSequence holds sqr (r * F) = (r ^2) * (sqr F) let F be real-valued FinSequence; ::_thesis: sqr (r * F) = (r ^2) * (sqr F) A1: dom (r * F) = dom F by VALUED_1:def_5; A2: dom ((r ^2) * (sqr F)) = dom (sqr F) by VALUED_1:def_5; A3: dom (sqr F) = dom F by VALUED_1:11; now__::_thesis:_for_i_being_Nat_st_i_in_dom_(sqr_(r_*_F))_holds_ (sqr_(r_*_F))_._i_=_((r_^2)_*_(sqr_F))_._i let i be Nat; ::_thesis: ( i in dom (sqr (r * F)) implies (sqr (r * F)) . i = ((r ^2) * (sqr F)) . i ) assume i in dom (sqr (r * F)) ; ::_thesis: (sqr (r * F)) . i = ((r ^2) * (sqr F)) . i thus (sqr (r * F)) . i = ((r * F) . i) ^2 by VALUED_1:11 .= (r * (F . i)) ^2 by VALUED_1:6 .= (r ^2) * ((F . i) ^2) .= (r ^2) * ((sqr F) . i) by VALUED_1:11 .= ((r ^2) * (sqr F)) . i by VALUED_1:6 ; ::_thesis: verum end; hence sqr (r * F) = (r ^2) * (sqr F) by A1, A2, A3, FINSEQ_1:13, VALUED_1:11; ::_thesis: verum end; notation let F1, F2 be real-valued FinSequence; synonym mlt (F1,F2) for F1 (#) F2; end; definition let F1, F2 be real-valued FinSequence; :: original: mlt redefine func mlt (F1,F2) -> FinSequence of REAL equals :: RVSUM_1:def 9 multreal .: (F1,F2); coherence mlt (F1,F2) is FinSequence of REAL by Lm2; compatibility for b1 being FinSequence of REAL holds ( b1 = mlt (F1,F2) iff b1 = multreal .: (F1,F2) ) proof reconsider F3 = F1, F4 = F2 as FinSequence of REAL by Lm2; let F be FinSequence of REAL ; ::_thesis: ( F = mlt (F1,F2) iff F = multreal .: (F1,F2) ) dom multreal = [:REAL,REAL:] by FUNCT_2:def_1; then [:(rng F3),(rng F4):] c= dom multreal by ZFMISC_1:96; then A1: dom (multreal .: (F1,F2)) = (dom F1) /\ (dom F2) by FUNCOP_1:69; A2: dom (mlt (F1,F2)) = (dom F1) /\ (dom F2) by VALUED_1:def_4; thus ( F = mlt (F1,F2) implies F = multreal .: (F1,F2) ) ::_thesis: ( F = multreal .: (F1,F2) implies F = mlt (F1,F2) ) proof assume A3: F = mlt (F1,F2) ; ::_thesis: F = multreal .: (F1,F2) for z being set st z in dom (multreal .: (F1,F2)) holds F . z = multreal . ((F1 . z),(F2 . z)) proof let z be set ; ::_thesis: ( z in dom (multreal .: (F1,F2)) implies F . z = multreal . ((F1 . z),(F2 . z)) ) assume z in dom (multreal .: (F1,F2)) ; ::_thesis: F . z = multreal . ((F1 . z),(F2 . z)) thus F . z = (F1 . z) * (F2 . z) by A3, VALUED_1:5 .= multreal . ((F1 . z),(F2 . z)) by BINOP_2:def_11 ; ::_thesis: verum end; hence F = multreal .: (F1,F2) by A2, A1, A3, FUNCOP_1:21; ::_thesis: verum end; assume A4: F = multreal .: (F1,F2) ; ::_thesis: F = mlt (F1,F2) now__::_thesis:_for_c_being_set_st_c_in_dom_F_holds_ F_._c_=_(F1_._c)_*_(F2_._c) let c be set ; ::_thesis: ( c in dom F implies F . c = (F1 . c) * (F2 . c) ) assume c in dom F ; ::_thesis: F . c = (F1 . c) * (F2 . c) hence F . c = multreal . ((F1 . c),(F2 . c)) by A4, FUNCOP_1:22 .= (F1 . c) * (F2 . c) by BINOP_2:def_11 ; ::_thesis: verum end; hence F = mlt (F1,F2) by A1, A4, VALUED_1:def_4; ::_thesis: verum end; commutativity for b1 being FinSequence of REAL for F1, F2 being real-valued FinSequence st b1 = multreal .: (F1,F2) holds b1 = multreal .: (F2,F1) proof let F be FinSequence of REAL ; ::_thesis: for F1, F2 being real-valued FinSequence st F = multreal .: (F1,F2) holds F = multreal .: (F2,F1) let F1, F2 be real-valued FinSequence; ::_thesis: ( F = multreal .: (F1,F2) implies F = multreal .: (F2,F1) ) reconsider F3 = F1, F4 = F2 as FinSequence of REAL by Lm2; A5: dom multreal = [:REAL,REAL:] by FUNCT_2:def_1; then A6: [:(rng F4),(rng F3):] c= dom multreal by ZFMISC_1:96; [:(rng F3),(rng F4):] c= dom multreal by A5, ZFMISC_1:96; then A7: dom (multreal .: (F1,F2)) = (dom F1) /\ (dom F2) by FUNCOP_1:69 .= dom (multreal .: (F2,F1)) by A6, FUNCOP_1:69 ; assume A8: F = multreal .: (F1,F2) ; ::_thesis: F = multreal .: (F2,F1) for z being set st z in dom (multreal .: (F2,F1)) holds F . z = multreal . ((F2 . z),(F1 . z)) proof let z be set ; ::_thesis: ( z in dom (multreal .: (F2,F1)) implies F . z = multreal . ((F2 . z),(F1 . z)) ) assume A9: z in dom (multreal .: (F2,F1)) ; ::_thesis: F . z = multreal . ((F2 . z),(F1 . z)) set F1z = F1 . z; set F2z = F2 . z; thus F . z = multreal . ((F1 . z),(F2 . z)) by A8, A7, A9, FUNCOP_1:22 .= (F1 . z) * (F2 . z) by BINOP_2:def_11 .= multreal . ((F2 . z),(F1 . z)) by BINOP_2:def_11 ; ::_thesis: verum end; hence F = multreal .: (F2,F1) by A8, A7, FUNCOP_1:21; ::_thesis: verum end; end; :: deftheorem defines mlt RVSUM_1:def_9_:_ for F1, F2 being real-valued FinSequence holds mlt (F1,F2) = multreal .: (F1,F2); theorem :: RVSUM_1:59 for s being set for F1, F2 being real-valued FinSequence holds (mlt (F1,F2)) . s = (F1 . s) * (F2 . s) by VALUED_1:5; definition let i be Nat; let R1, R2 be Element of i -tuples_on REAL; :: original: mlt redefine func mlt (R1,R2) -> Element of i -tuples_on REAL; coherence mlt (R1,R2) is Element of i -tuples_on REAL by FINSEQ_2:120; end; theorem :: RVSUM_1:60 for s being set for F1, F2 being real-valued FinSequence holds (mlt (F1,F2)) . s = (F1 . s) * (F2 . s) by VALUED_1:5; theorem :: RVSUM_1:61 for F being real-valued FinSequence holds mlt ((<*> REAL),F) = <*> REAL proof let F be real-valued FinSequence; ::_thesis: mlt ((<*> REAL),F) = <*> REAL F is FinSequence of REAL by Lm2; hence mlt ((<*> REAL),F) = <*> REAL by FINSEQ_2:73; ::_thesis: verum end; theorem :: RVSUM_1:62 for r1, r2 being real number holds mlt (<*r1*>,<*r2*>) = <*(r1 * r2)*> proof let r1, r2 be real number ; ::_thesis: mlt (<*r1*>,<*r2*>) = <*(r1 * r2)*> reconsider s1 = r1, s2 = r2 as Element of REAL by XREAL_0:def_1; mlt (<*s1*>,<*s2*>) = <*(multreal . (s1,s2))*> by FINSEQ_2:74 .= <*(r1 * r2)*> by BINOP_2:def_11 ; hence mlt (<*r1*>,<*r2*>) = <*(r1 * r2)*> ; ::_thesis: verum end; theorem Th63: :: RVSUM_1:63 for i being Nat for r being real number for R being Element of i -tuples_on REAL holds mlt ((i |-> r),R) = r * R proof let i be Nat; ::_thesis: for r being real number for R being Element of i -tuples_on REAL holds mlt ((i |-> r),R) = r * R let r be real number ; ::_thesis: for R being Element of i -tuples_on REAL holds mlt ((i |-> r),R) = r * R let R be Element of i -tuples_on REAL; ::_thesis: mlt ((i |-> r),R) = r * R reconsider s = r as Element of REAL by XREAL_0:def_1; mlt ((i |-> s),R) = multreal [;] (s,R) by FINSEQOP:20 .= r * R by FINSEQOP:22 ; hence mlt ((i |-> r),R) = r * R ; ::_thesis: verum end; theorem :: RVSUM_1:64 for i being Nat for r1, r2 being real number holds mlt ((i |-> r1),(i |-> r2)) = i |-> (r1 * r2) proof let i be Nat; ::_thesis: for r1, r2 being real number holds mlt ((i |-> r1),(i |-> r2)) = i |-> (r1 * r2) let r1, r2 be real number ; ::_thesis: mlt ((i |-> r1),(i |-> r2)) = i |-> (r1 * r2) reconsider s1 = r1, s2 = r2 as Element of REAL by XREAL_0:def_1; mlt ((i |-> s1),(i |-> s2)) = s1 * (i |-> s2) by Th63 .= i |-> (r1 * r2) by Th48 ; hence mlt ((i |-> r1),(i |-> r2)) = i |-> (r1 * r2) ; ::_thesis: verum end; theorem :: RVSUM_1:65 for r being real number for F1, F2 being real-valued FinSequence holds r * (mlt (F1,F2)) = mlt ((r * F1),F2) by RFUNCT_1:12; theorem :: RVSUM_1:66 for i being Nat for r being real number for R being Element of i -tuples_on REAL holds r * R = mlt ((i |-> r),R) by Th63; theorem :: RVSUM_1:67 for F being real-valued FinSequence holds sqr F = mlt (F,F) ; theorem Th68: :: RVSUM_1:68 for F1, F2 being real-valued FinSequence holds sqr (F1 + F2) = ((sqr F1) + (2 * (mlt (F1,F2)))) + (sqr F2) proof let F1, F2 be real-valued FinSequence; ::_thesis: sqr (F1 + F2) = ((sqr F1) + (2 * (mlt (F1,F2)))) + (sqr F2) A1: dom (sqr (F1 + F2)) = dom (F1 + F2) by VALUED_1:11; A2: dom (F1 + F2) = (dom F1) /\ (dom F2) by VALUED_1:def_1; A3: dom ((sqr F1) + (2 * (mlt (F1,F2)))) = (dom (sqr F1)) /\ (dom (2 * (mlt (F1,F2)))) by VALUED_1:def_1 .= (dom F1) /\ (dom (2 * (mlt (F1,F2)))) by VALUED_1:11 .= (dom F1) /\ (dom (mlt (F1,F2))) by VALUED_1:def_5 .= (dom F1) /\ ((dom F1) /\ (dom F2)) by VALUED_1:def_4 .= ((dom F1) /\ (dom F1)) /\ (dom F2) by XBOOLE_1:16 .= (dom F1) /\ (dom F2) ; then A4: dom (((sqr F1) + (2 * (mlt (F1,F2)))) + (sqr F2)) = ((dom F1) /\ (dom F2)) /\ (dom (sqr F2)) by VALUED_1:def_1 .= ((dom F1) /\ (dom F2)) /\ (dom F2) by VALUED_1:11 .= (dom F1) /\ ((dom F2) /\ (dom F2)) by XBOOLE_1:16 ; now__::_thesis:_for_j_being_Nat_st_j_in_dom_(sqr_(F1_+_F2))_holds_ (sqr_(F1_+_F2))_._j_=_(((sqr_F1)_+_(2_*_(mlt_(F1,F2))))_+_(sqr_F2))_._j let j be Nat; ::_thesis: ( j in dom (sqr (F1 + F2)) implies (sqr (F1 + F2)) . j = (((sqr F1) + (2 * (mlt (F1,F2)))) + (sqr F2)) . j ) assume A5: j in dom (sqr (F1 + F2)) ; ::_thesis: (sqr (F1 + F2)) . j = (((sqr F1) + (2 * (mlt (F1,F2)))) + (sqr F2)) . j set r1r2 = (F1 + F2) . j; set r1 = F1 . j; set r2 = F2 . j; set r192 = (sqr F1) . j; set r292 = (sqr F2) . j; set r1r2a = (mlt (F1,F2)) . j; set 2r1r2 = (2 * (mlt (F1,F2))) . j; set r1922r1r2 = ((sqr F1) + (2 * (mlt (F1,F2)))) . j; thus (sqr (F1 + F2)) . j = ((F1 + F2) . j) ^2 by VALUED_1:11 .= ((F1 . j) + (F2 . j)) ^2 by A1, A5, VALUED_1:def_1 .= (((F1 . j) ^2) + ((2 * (F1 . j)) * (F2 . j))) + ((F2 . j) ^2) .= (((sqr F1) . j) + (2 * ((F1 . j) * (F2 . j)))) + ((F2 . j) ^2) by VALUED_1:11 .= (((sqr F1) . j) + (2 * ((F1 . j) * (F2 . j)))) + ((sqr F2) . j) by VALUED_1:11 .= (((sqr F1) . j) + (2 * ((mlt (F1,F2)) . j))) + ((sqr F2) . j) by VALUED_1:5 .= (((sqr F1) . j) + ((2 * (mlt (F1,F2))) . j)) + ((sqr F2) . j) by VALUED_1:6 .= (((sqr F1) + (2 * (mlt (F1,F2)))) . j) + ((sqr F2) . j) by A1, A2, A3, A5, VALUED_1:def_1 .= (((sqr F1) + (2 * (mlt (F1,F2)))) + (sqr F2)) . j by A1, A2, A4, A5, VALUED_1:def_1 ; ::_thesis: verum end; hence sqr (F1 + F2) = ((sqr F1) + (2 * (mlt (F1,F2)))) + (sqr F2) by A2, A4, FINSEQ_1:13, VALUED_1:11; ::_thesis: verum end; theorem Th69: :: RVSUM_1:69 for F1, F2 being real-valued FinSequence holds sqr (F1 - F2) = ((sqr F1) - (2 * (mlt (F1,F2)))) + (sqr F2) proof let F1, F2 be real-valued FinSequence; ::_thesis: sqr (F1 - F2) = ((sqr F1) - (2 * (mlt (F1,F2)))) + (sqr F2) thus sqr (F1 - F2) = ((sqr F1) + (2 * (mlt (F1,(- F2))))) + (sqr (- F2)) by Th68 .= ((sqr F1) + (2 * (mlt (F1,(- F2))))) + (sqr F2) by Th57 .= ((sqr F1) + (2 * ((- 1) * (mlt (F1,F2))))) + (sqr F2) by RFUNCT_1:12 .= ((sqr F1) + (((- 1) * 2) * (mlt (F1,F2)))) + (sqr F2) by RFUNCT_1:17 .= ((sqr F1) - (2 * (mlt (F1,F2)))) + (sqr F2) by RFUNCT_1:17 ; ::_thesis: verum end; theorem :: RVSUM_1:70 for F1, F2 being real-valued FinSequence holds sqr (mlt (F1,F2)) = mlt ((sqr F1),(sqr F2)) proof let F1, F2 be real-valued FinSequence; ::_thesis: sqr (mlt (F1,F2)) = mlt ((sqr F1),(sqr F2)) A1: dom (mlt (F1,F2)) = (dom F1) /\ (dom F2) by VALUED_1:def_4; A2: dom (mlt ((sqr F1),(sqr F2))) = (dom (sqr F1)) /\ (dom (sqr F2)) by VALUED_1:def_4; A3: dom (sqr F1) = dom F1 by VALUED_1:11; A4: dom (sqr F2) = dom F2 by VALUED_1:11; now__::_thesis:_for_i_being_Nat_st_i_in_dom_(sqr_(mlt_(F1,F2)))_holds_ (sqr_(mlt_(F1,F2)))_._i_=_(mlt_((sqr_F1),(sqr_F2)))_._i let i be Nat; ::_thesis: ( i in dom (sqr (mlt (F1,F2))) implies (sqr (mlt (F1,F2))) . i = (mlt ((sqr F1),(sqr F2))) . i ) assume i in dom (sqr (mlt (F1,F2))) ; ::_thesis: (sqr (mlt (F1,F2))) . i = (mlt ((sqr F1),(sqr F2))) . i thus (sqr (mlt (F1,F2))) . i = ((mlt (F1,F2)) . i) ^2 by VALUED_1:11 .= ((F1 . i) * (F2 . i)) ^2 by VALUED_1:5 .= ((F1 . i) ^2) * ((F2 . i) ^2) .= ((sqr F1) . i) * ((F2 . i) ^2) by VALUED_1:11 .= ((sqr F1) . i) * ((sqr F2) . i) by VALUED_1:11 .= (mlt ((sqr F1),(sqr F2))) . i by VALUED_1:5 ; ::_thesis: verum end; hence sqr (mlt (F1,F2)) = mlt ((sqr F1),(sqr F2)) by A1, A2, A3, A4, FINSEQ_1:13, VALUED_1:11; ::_thesis: verum end; notation let F be Relation; synonym complex-yielding F for complex-valued ; end; registration cluster -> complex-valued for FinSequence of COMPLEX ; coherence for b1 being FinSequence of COMPLEX holds b1 is complex-valued ; cluster Relation-like NAT -defined Function-like complex-valued real-valued V60() FinSequence-like FinSubsequence-like for set ; existence ex b1 being FinSequence st ( b1 is real-valued & b1 is complex-valued ) proof <*> REAL is real-valued ; hence ex b1 being FinSequence st ( b1 is real-valued & b1 is complex-valued ) ; ::_thesis: verum end; end; definition let F be complex-valued FinSequence; func Sum F -> complex number means :Def10: :: RVSUM_1:def 10 ex f being FinSequence of COMPLEX st ( f = F & it = addcomplex $$ f ); existence ex b1 being complex number ex f being FinSequence of COMPLEX st ( f = F & b1 = addcomplex $$ f ) proof rng F c= COMPLEX by VALUED_0:def_1; then reconsider f = F as FinSequence of COMPLEX by FINSEQ_1:def_4; take addcomplex $$ f ; ::_thesis: ex f being FinSequence of COMPLEX st ( f = F & addcomplex $$ f = addcomplex $$ f ) thus ex f being FinSequence of COMPLEX st ( f = F & addcomplex $$ f = addcomplex $$ f ) ; ::_thesis: verum end; uniqueness for b1, b2 being complex number st ex f being FinSequence of COMPLEX st ( f = F & b1 = addcomplex $$ f ) & ex f being FinSequence of COMPLEX st ( f = F & b2 = addcomplex $$ f ) holds b1 = b2 ; end; :: deftheorem Def10 defines Sum RVSUM_1:def_10_:_ for F being complex-valued FinSequence for b2 being complex number holds ( b2 = Sum F iff ex f being FinSequence of COMPLEX st ( f = F & b2 = addcomplex $$ f ) ); registration let F be real-valued FinSequence; cluster Sum F -> complex real ; coherence Sum F is real proof set mc = addcomplex ; consider f being FinSequence of COMPLEX such that A1: f = F and A2: Sum F = addcomplex $$ f by Def10; set g = [#] (f,(the_unity_wrt addcomplex)); defpred S1[ Nat] means addcomplex $$ ((finSeg F),([#] (f,(the_unity_wrt addcomplex)))) is real ; A3: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A4: S1[k] ; ::_thesis: S1[k + 1] reconsider k = k as Element of NAT by ORDINAL1:def_12; ([#] (f,(the_unity_wrt addcomplex))) . (k + 1) is real proof percases ( k + 1 in dom f or not k + 1 in dom f ) ; suppose k + 1 in dom f ; ::_thesis: ([#] (f,(the_unity_wrt addcomplex))) . (k + 1) is real then ([#] (f,(the_unity_wrt addcomplex))) . (k + 1) = f . (k + 1) by SETWOP_2:20; hence ([#] (f,(the_unity_wrt addcomplex))) . (k + 1) is real by A1; ::_thesis: verum end; suppose not k + 1 in dom f ; ::_thesis: ([#] (f,(the_unity_wrt addcomplex))) . (k + 1) is real hence ([#] (f,(the_unity_wrt addcomplex))) . (k + 1) is real by BINOP_2:1, SETWOP_2:20; ::_thesis: verum end; end; end; then reconsider a = ([#] (f,(the_unity_wrt addcomplex))) . (k + 1), b = addcomplex $$ ((finSeg k),([#] (f,(the_unity_wrt addcomplex)))) as real number by A4; not k + 1 in Seg k by FINSEQ_3:8; then addcomplex $$ (((finSeg k) \/ {.(k + 1).}),([#] (f,(the_unity_wrt addcomplex)))) = addcomplex . ((addcomplex $$ ((finSeg k),([#] (f,(the_unity_wrt addcomplex))))),(([#] (f,(the_unity_wrt addcomplex))) . (k + 1))) by SETWOP_2:2 .= b + a by BINOP_2:def_3 ; hence S1[k + 1] by FINSEQ_1:9; ::_thesis: verum end; A5: ( addcomplex $$ f = addcomplex $$ ((findom f),([#] (f,(the_unity_wrt addcomplex)))) & ex n being Nat st dom f = Seg n ) by FINSEQ_1:def_2, SETWOP_2:def_2; Seg 0 = {}. NAT ; then A6: S1[ 0 ] by BINOP_2:1, SETWISEO:31; for n being Nat holds S1[n] from NAT_1:sch_2(A6, A3); hence Sum F is real by A2, A5; ::_thesis: verum end; end; theorem Th71: :: RVSUM_1:71 for F being FinSequence of REAL holds Sum F = addreal $$ F proof set g = addreal ; set h = addcomplex ; let F be FinSequence of REAL ; ::_thesis: Sum F = addreal $$ F rng F c= COMPLEX by NUMBERS:11, XBOOLE_1:1; then reconsider f = F as FinSequence of COMPLEX by FINSEQ_1:def_4; defpred S1[ Nat] means addreal $$ ((finSeg $1),([#] (F,(the_unity_wrt addreal)))) = addcomplex $$ ((finSeg $1),([#] (f,(the_unity_wrt addcomplex)))); consider n being Nat such that A1: dom f = Seg n by FINSEQ_1:def_2; A2: ( addreal $$ F = addreal $$ ((finSeg n),([#] (F,(the_unity_wrt addreal)))) & addcomplex $$ f = addcomplex $$ ((finSeg n),([#] (f,(the_unity_wrt addcomplex)))) ) by A1, SETWOP_2:def_2; A3: for k being Nat st S1[k] holds S1[k + 1] proof set j = [#] (f,(the_unity_wrt addcomplex)); set i = [#] (F,(the_unity_wrt addreal)); let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A4: S1[k] ; ::_thesis: S1[k + 1] reconsider k = k as Element of NAT by ORDINAL1:def_12; A5: ([#] (F,(the_unity_wrt addreal))) . (k + 1) = ([#] (f,(the_unity_wrt addcomplex))) . (k + 1) proof percases ( k + 1 in dom f or not k + 1 in dom f ) ; supposeA6: k + 1 in dom f ; ::_thesis: ([#] (F,(the_unity_wrt addreal))) . (k + 1) = ([#] (f,(the_unity_wrt addcomplex))) . (k + 1) then ([#] (f,(the_unity_wrt addcomplex))) . (k + 1) = F . (k + 1) by SETWOP_2:20 .= ([#] (F,(the_unity_wrt addreal))) . (k + 1) by A6, SETWOP_2:20 ; hence ([#] (F,(the_unity_wrt addreal))) . (k + 1) = ([#] (f,(the_unity_wrt addcomplex))) . (k + 1) ; ::_thesis: verum end; supposeA7: not k + 1 in dom f ; ::_thesis: ([#] (F,(the_unity_wrt addreal))) . (k + 1) = ([#] (f,(the_unity_wrt addcomplex))) . (k + 1) then ([#] (f,(the_unity_wrt addcomplex))) . (k + 1) = the_unity_wrt addcomplex by SETWOP_2:20 .= ([#] (F,(the_unity_wrt addreal))) . (k + 1) by A7, BINOP_2:1, BINOP_2:2, SETWOP_2:20 ; hence ([#] (F,(the_unity_wrt addreal))) . (k + 1) = ([#] (f,(the_unity_wrt addcomplex))) . (k + 1) ; ::_thesis: verum end; end; end; A8: not k + 1 in Seg k by FINSEQ_3:8; addreal $$ ((finSeg (k + 1)),([#] (F,(the_unity_wrt addreal)))) = addreal $$ (((finSeg k) \/ {.(k + 1).}),([#] (F,(the_unity_wrt addreal)))) by FINSEQ_1:9 .= addreal . ((addreal $$ ((finSeg k),([#] (F,(the_unity_wrt addreal))))),(([#] (F,(the_unity_wrt addreal))) . (k + 1))) by A8, SETWOP_2:2 .= (addreal $$ ((finSeg k),([#] (F,(the_unity_wrt addreal))))) + (([#] (F,(the_unity_wrt addreal))) . (k + 1)) by BINOP_2:def_9 .= addcomplex . ((addcomplex $$ ((finSeg k),([#] (f,(the_unity_wrt addcomplex))))),(([#] (f,(the_unity_wrt addcomplex))) . (k + 1))) by A4, A5, BINOP_2:def_3 .= addcomplex $$ (((finSeg k) \/ {.(k + 1).}),([#] (f,(the_unity_wrt addcomplex)))) by A8, SETWOP_2:2 .= addcomplex $$ ((finSeg (k + 1)),([#] (f,(the_unity_wrt addcomplex)))) by FINSEQ_1:9 ; hence S1[k + 1] ; ::_thesis: verum end; A9: Seg 0 = {}. NAT ; then addreal $$ ((finSeg 0),([#] (F,(the_unity_wrt addreal)))) = the_unity_wrt addcomplex by BINOP_2:1, BINOP_2:2, SETWISEO:31 .= addcomplex $$ ((finSeg 0),([#] (f,(the_unity_wrt addcomplex)))) by A9, SETWISEO:31 ; then A10: S1[ 0 ] ; for k being Nat holds S1[k] from NAT_1:sch_2(A10, A3); then addreal $$ F = addcomplex $$ f by A2; hence Sum F = addreal $$ F by Def10; ::_thesis: verum end; definition let F be FinSequence of COMPLEX ; :: original: Sum redefine func Sum F -> Element of COMPLEX equals :: RVSUM_1:def 11 addcomplex $$ F; coherence Sum F is Element of COMPLEX by XCMPLX_0:def_2; compatibility for b1 being Element of COMPLEX holds ( b1 = Sum F iff b1 = addcomplex $$ F ) by Def10; end; :: deftheorem defines Sum RVSUM_1:def_11_:_ for F being FinSequence of COMPLEX holds Sum F = addcomplex $$ F; definition let F be FinSequence of REAL ; :: original: Sum redefine func Sum F -> Element of REAL equals :: RVSUM_1:def 12 addreal $$ F; coherence Sum F is Element of REAL by XREAL_0:def_1; compatibility for b1 being Element of REAL holds ( b1 = Sum F iff b1 = addreal $$ F ) by Th71; end; :: deftheorem defines Sum RVSUM_1:def_12_:_ for F being FinSequence of REAL holds Sum F = addreal $$ F; theorem Th72: :: RVSUM_1:72 Sum (<*> REAL) = 0 by BINOP_2:2, FINSOP_1:10; theorem :: RVSUM_1:73 for r being real number holds Sum <*r*> = r proof let r be real number ; ::_thesis: Sum <*r*> = r reconsider r = r as Element of REAL by XREAL_0:def_1; Sum <*r*> = r by FINSOP_1:11; hence Sum <*r*> = r ; ::_thesis: verum end; theorem Th74: :: RVSUM_1:74 for r being real number for F being real-valued FinSequence holds Sum (F ^ <*r*>) = (Sum F) + r proof let r be real number ; ::_thesis: for F being real-valued FinSequence holds Sum (F ^ <*r*>) = (Sum F) + r let F be real-valued FinSequence; ::_thesis: Sum (F ^ <*r*>) = (Sum F) + r reconsider s = r as Element of REAL by XREAL_0:def_1; reconsider F1 = F as FinSequence of REAL by Lm2; thus Sum (F ^ <*r*>) = Sum (F1 ^ <*s*>) .= addreal . ((addreal $$ F1),s) by FINSOP_1:4 .= (Sum F1) + r by BINOP_2:def_9 .= (Sum F) + r ; ::_thesis: verum end; theorem Th75: :: RVSUM_1:75 for F1, F2 being real-valued FinSequence holds Sum (F1 ^ F2) = (Sum F1) + (Sum F2) proof let F1, F2 be real-valued FinSequence; ::_thesis: Sum (F1 ^ F2) = (Sum F1) + (Sum F2) reconsider F3 = F1, F4 = F2 as FinSequence of REAL by Lm2; thus Sum (F1 ^ F2) = Sum (F3 ^ F4) .= addreal . ((addreal $$ F3),(addreal $$ F4)) by FINSOP_1:5 .= (Sum F3) + (Sum F4) by BINOP_2:def_9 .= (Sum F1) + (Sum F2) ; ::_thesis: verum end; theorem :: RVSUM_1:76 for r being real number for F being real-valued FinSequence holds Sum (<*r*> ^ F) = r + (Sum F) proof let r be real number ; ::_thesis: for F being real-valued FinSequence holds Sum (<*r*> ^ F) = r + (Sum F) let F be real-valued FinSequence; ::_thesis: Sum (<*r*> ^ F) = r + (Sum F) reconsider s = r as Element of REAL by XREAL_0:def_1; thus Sum (<*r*> ^ F) = (Sum <*s*>) + (Sum F) by Th75 .= r + (Sum F) by FINSOP_1:11 ; ::_thesis: verum end; theorem Th77: :: RVSUM_1:77 for r1, r2 being real number holds Sum <*r1,r2*> = r1 + r2 proof let r1, r2 be real number ; ::_thesis: Sum <*r1,r2*> = r1 + r2 reconsider s1 = r1 as Element of REAL by XREAL_0:def_1; thus Sum <*r1,r2*> = (Sum <*s1*>) + r2 by Th74 .= r1 + r2 by FINSOP_1:11 ; ::_thesis: verum end; theorem Th78: :: RVSUM_1:78 for r1, r2, r3 being real number holds Sum <*r1,r2,r3*> = (r1 + r2) + r3 proof let r1, r2, r3 be real number ; ::_thesis: Sum <*r1,r2,r3*> = (r1 + r2) + r3 thus Sum <*r1,r2,r3*> = (Sum <*r1,r2*>) + r3 by Th74 .= (r1 + r2) + r3 by Th77 ; ::_thesis: verum end; theorem :: RVSUM_1:79 for R being Element of 0 -tuples_on REAL holds Sum R = 0 by Th72; theorem Th80: :: RVSUM_1:80 for i being Nat for r being real number holds Sum (i |-> r) = i * r proof let i be Nat; ::_thesis: for r being real number holds Sum (i |-> r) = i * r let r be real number ; ::_thesis: Sum (i |-> r) = i * r reconsider r = r as Element of REAL by XREAL_0:def_1; defpred S1[ Nat] means Sum ($1 |-> r) = $1 * r; A1: for i being Nat st S1[i] holds S1[i + 1] proof let i be Nat; ::_thesis: ( S1[i] implies S1[i + 1] ) assume A2: Sum (i |-> r) = i * r ; ::_thesis: S1[i + 1] thus Sum ((i + 1) |-> r) = Sum ((i |-> r) ^ <*r*>) by FINSEQ_2:60 .= (i * r) + (1 * r) by A2, Th74 .= (i + 1) * r ; ::_thesis: verum end; A3: S1[ 0 ] by Th72; for i being Nat holds S1[i] from NAT_1:sch_2(A3, A1); hence Sum (i |-> r) = i * r ; ::_thesis: verum end; theorem Th81: :: RVSUM_1:81 for i being Nat holds Sum (i |-> 0) = 0 proof let i be Nat; ::_thesis: Sum (i |-> 0) = 0 thus Sum (i |-> 0) = i * 0 by Th80 .= 0 ; ::_thesis: verum end; theorem Th82: :: RVSUM_1:82 for i being Nat for R1, R2 being Element of i -tuples_on REAL st ( for j being Nat st j in Seg i holds R1 . j <= R2 . j ) holds Sum R1 <= Sum R2 proof let i be Nat; ::_thesis: for R1, R2 being Element of i -tuples_on REAL st ( for j being Nat st j in Seg i holds R1 . j <= R2 . j ) holds Sum R1 <= Sum R2 let R1, R2 be Element of i -tuples_on REAL; ::_thesis: ( ( for j being Nat st j in Seg i holds R1 . j <= R2 . j ) implies Sum R1 <= Sum R2 ) defpred S1[ Nat] means for R1, R2 being Element of $1 -tuples_on REAL st ( for j being Nat st j in Seg $1 holds R1 . j <= R2 . j ) holds Sum R1 <= Sum R2; A1: for i being Nat st S1[i] holds S1[i + 1] proof let i be Nat; ::_thesis: ( S1[i] implies S1[i + 1] ) assume A2: for R1, R2 being Element of i -tuples_on REAL st ( for j being Nat st j in Seg i holds R1 . j <= R2 . j ) holds Sum R1 <= Sum R2 ; ::_thesis: S1[i + 1] set n = i + 1; let R1, R2 be Element of (i + 1) -tuples_on REAL; ::_thesis: ( ( for j being Nat st j in Seg (i + 1) holds R1 . j <= R2 . j ) implies Sum R1 <= Sum R2 ) assume A3: for j being Nat st j in Seg (i + 1) holds R1 . j <= R2 . j ; ::_thesis: Sum R1 <= Sum R2 consider R19 being Element of i -tuples_on REAL, x1 being Element of REAL such that A4: R1 = R19 ^ <*x1*> by FINSEQ_2:117; consider R29 being Element of i -tuples_on REAL, x2 being Element of REAL such that A5: R2 = R29 ^ <*x2*> by FINSEQ_2:117; for j being Nat st j in Seg i holds R19 . j <= R29 . j proof let j be Nat; ::_thesis: ( j in Seg i implies R19 . j <= R29 . j ) assume A6: j in Seg i ; ::_thesis: R19 . j <= R29 . j ( Seg (len R29) = dom R29 & len R29 = i ) by CARD_1:def_7, FINSEQ_1:def_3; then A7: R29 . j = R2 . j by A5, A6, FINSEQ_1:def_7; ( Seg (len R19) = dom R19 & len R19 = i ) by CARD_1:def_7, FINSEQ_1:def_3; then R19 . j = R1 . j by A4, A6, FINSEQ_1:def_7; hence R19 . j <= R29 . j by A3, A6, A7, FINSEQ_2:8; ::_thesis: verum end; then A8: Sum R19 <= Sum R29 by A2; A9: R2 . (i + 1) = x2 by A5, FINSEQ_2:116; R1 . (i + 1) = x1 by A4, FINSEQ_2:116; then A10: x1 <= x2 by A3, A9, FINSEQ_1:4; A11: Sum R2 = (Sum R29) + x2 by A5, Th74; Sum R1 = (Sum R19) + x1 by A4, Th74; hence Sum R1 <= Sum R2 by A10, A8, A11, XREAL_1:7; ::_thesis: verum end; A12: S1[ 0 ] ; for i being Nat holds S1[i] from NAT_1:sch_2(A12, A1); hence ( ( for j being Nat st j in Seg i holds R1 . j <= R2 . j ) implies Sum R1 <= Sum R2 ) ; ::_thesis: verum end; theorem Th83: :: RVSUM_1:83 for i being Nat for R1, R2 being Element of i -tuples_on REAL st ( for j being Nat st j in Seg i holds R1 . j <= R2 . j ) & ex j being Nat st ( j in Seg i & R1 . j < R2 . j ) holds Sum R1 < Sum R2 proof let i be Nat; ::_thesis: for R1, R2 being Element of i -tuples_on REAL st ( for j being Nat st j in Seg i holds R1 . j <= R2 . j ) & ex j being Nat st ( j in Seg i & R1 . j < R2 . j ) holds Sum R1 < Sum R2 let R1, R2 be Element of i -tuples_on REAL; ::_thesis: ( ( for j being Nat st j in Seg i holds R1 . j <= R2 . j ) & ex j being Nat st ( j in Seg i & R1 . j < R2 . j ) implies Sum R1 < Sum R2 ) defpred S1[ Nat] means for R1, R2 being Element of $1 -tuples_on REAL st ( for j being Nat st j in Seg $1 holds R1 . j <= R2 . j ) & ex j being Nat st ( j in Seg $1 & R1 . j < R2 . j ) holds Sum R1 < Sum R2; now__::_thesis:_for_i_being_Nat_st_S1[i]_holds_ for_R1,_R2_being_Element_of_(i_+_1)_-tuples_on_REAL_st_(_for_j_being_Nat_st_j_in_Seg_(i_+_1)_holds_ R1_._j_<=_R2_._j_)_&_ex_j_being_Nat_st_ (_j_in_Seg_(i_+_1)_&_R1_._j_<_R2_._j_)_holds_ Sum_R1_<_Sum_R2 let i be Nat; ::_thesis: ( S1[i] implies for R1, R2 being Element of (i + 1) -tuples_on REAL st ( for j being Nat st j in Seg (i + 1) holds R1 . j <= R2 . j ) & ex j being Nat st ( j in Seg (i + 1) & R1 . j < R2 . j ) holds Sum R1 < Sum R2 ) assume A1: S1[i] ; ::_thesis: for R1, R2 being Element of (i + 1) -tuples_on REAL st ( for j being Nat st j in Seg (i + 1) holds R1 . j <= R2 . j ) & ex j being Nat st ( j in Seg (i + 1) & R1 . j < R2 . j ) holds Sum R1 < Sum R2 let R1, R2 be Element of (i + 1) -tuples_on REAL; ::_thesis: ( ( for j being Nat st j in Seg (i + 1) holds R1 . j <= R2 . j ) & ex j being Nat st ( j in Seg (i + 1) & R1 . j < R2 . j ) implies Sum R1 < Sum R2 ) assume A2: for j being Nat st j in Seg (i + 1) holds R1 . j <= R2 . j ; ::_thesis: ( ex j being Nat st ( j in Seg (i + 1) & R1 . j < R2 . j ) implies Sum R1 < Sum R2 ) given j being Nat such that A3: j in Seg (i + 1) and A4: R1 . j < R2 . j ; ::_thesis: Sum R1 < Sum R2 consider R19 being Element of i -tuples_on REAL, x1 being Element of REAL such that A5: R1 = R19 ^ <*x1*> by FINSEQ_2:117; consider R29 being Element of i -tuples_on REAL, x2 being Element of REAL such that A6: R2 = R29 ^ <*x2*> by FINSEQ_2:117; A7: for j being Nat st j in Seg i holds R19 . j <= R29 . j proof let j be Nat; ::_thesis: ( j in Seg i implies R19 . j <= R29 . j ) assume A8: j in Seg i ; ::_thesis: R19 . j <= R29 . j ( Seg (len R29) = dom R29 & len R29 = i ) by CARD_1:def_7, FINSEQ_1:def_3; then A9: R29 . j = R2 . j by A6, A8, FINSEQ_1:def_7; ( Seg (len R19) = dom R19 & len R19 = i ) by CARD_1:def_7, FINSEQ_1:def_3; then R19 . j = R1 . j by A5, A8, FINSEQ_1:def_7; hence R19 . j <= R29 . j by A2, A8, A9, FINSEQ_2:8; ::_thesis: verum end; A10: R2 . (i + 1) = x2 by A6, FINSEQ_2:116; A11: R1 . (i + 1) = x1 by A5, FINSEQ_2:116; now__::_thesis:_Sum_R1_<_Sum_R2 percases ( j in Seg i or j = i + 1 ) by A3, FINSEQ_2:7; supposeA12: j in Seg i ; ::_thesis: Sum R1 < Sum R2 ( Seg (len R29) = dom R29 & len R29 = i ) by CARD_1:def_7, FINSEQ_1:def_3; then A13: R29 . j = R2 . j by A6, A12, FINSEQ_1:def_7; A14: ( Sum R1 = (Sum R19) + x1 & Sum R2 = (Sum R29) + x2 ) by A5, A6, Th74; A15: x1 <= x2 by A2, A11, A10, FINSEQ_1:4; ( Seg (len R19) = dom R19 & len R19 = i ) by CARD_1:def_7, FINSEQ_1:def_3; then R19 . j = R1 . j by A5, A12, FINSEQ_1:def_7; then Sum R19 < Sum R29 by A1, A4, A7, A12, A13; hence Sum R1 < Sum R2 by A14, A15, XREAL_1:8; ::_thesis: verum end; supposeA16: j = i + 1 ; ::_thesis: Sum R1 < Sum R2 A17: Sum R2 = (Sum R29) + x2 by A6, Th74; ( Sum R19 <= Sum R29 & Sum R1 = (Sum R19) + x1 ) by A5, A7, Th74, Th82; hence Sum R1 < Sum R2 by A4, A11, A10, A16, A17, XREAL_1:8; ::_thesis: verum end; end; end; hence Sum R1 < Sum R2 ; ::_thesis: verum end; then A18: for i being Nat st S1[i] holds S1[i + 1] ; A19: S1[ 0 ] ; for i being Nat holds S1[i] from NAT_1:sch_2(A19, A18); hence ( ( for j being Nat st j in Seg i holds R1 . j <= R2 . j ) & ex j being Nat st ( j in Seg i & R1 . j < R2 . j ) implies Sum R1 < Sum R2 ) ; ::_thesis: verum end; theorem Th84: :: RVSUM_1:84 for F being real-valued FinSequence st ( for i being Nat st i in dom F holds 0 <= F . i ) holds 0 <= Sum F proof let F be real-valued FinSequence; ::_thesis: ( ( for i being Nat st i in dom F holds 0 <= F . i ) implies 0 <= Sum F ) reconsider F1 = F as FinSequence of REAL by Lm2; set i = len F; set R1 = (len F) |-> 0; reconsider R2 = F1 as Element of (len F) -tuples_on REAL by FINSEQ_2:92; A1: Seg (len F) = dom F by FINSEQ_1:def_3; assume A2: for i being Nat st i in dom F holds 0 <= F . i ; ::_thesis: 0 <= Sum F for j being Nat st j in Seg (len F) holds ((len F) |-> 0) . j <= R2 . j by A2, A1; then Sum ((len F) |-> 0) <= Sum R2 by Th82; hence 0 <= Sum F by Th81; ::_thesis: verum end; theorem Th85: :: RVSUM_1:85 for F being real-valued FinSequence st ( for i being Nat st i in dom F holds 0 <= F . i ) & ex i being Nat st ( i in dom F & 0 < F . i ) holds 0 < Sum F proof let F be real-valued FinSequence; ::_thesis: ( ( for i being Nat st i in dom F holds 0 <= F . i ) & ex i being Nat st ( i in dom F & 0 < F . i ) implies 0 < Sum F ) reconsider F1 = F as FinSequence of REAL by Lm2; set i = len F; set R1 = (len F) |-> 0; reconsider R2 = F1 as Element of (len F) -tuples_on REAL by FINSEQ_2:92; A1: Seg (len F) = dom F by FINSEQ_1:def_3; assume A2: for i being Nat st i in dom F holds 0 <= F . i ; ::_thesis: ( for i being Nat holds ( not i in dom F or not 0 < F . i ) or 0 < Sum F ) A3: for j being Nat st j in Seg (len F) holds ((len F) |-> 0) . j <= R2 . j by A2, A1; given j being Nat such that A5: j in dom F and A6: 0 < F . j ; ::_thesis: 0 < Sum F ((len F) |-> 0) . j = 0 ; then Sum ((len F) |-> 0) < Sum R2 by A1, A3, A5, A6, Th83; hence 0 < Sum F by Th81; ::_thesis: verum end; theorem Th86: :: RVSUM_1:86 for F being real-valued FinSequence holds 0 <= Sum (sqr F) proof let F be real-valued FinSequence; ::_thesis: 0 <= Sum (sqr F) now__::_thesis:_for_i_being_Nat_st_i_in_dom_(sqr_F)_holds_ 0_<=_(sqr_F)_._i let i be Nat; ::_thesis: ( i in dom (sqr F) implies 0 <= (sqr F) . i ) assume i in dom (sqr F) ; ::_thesis: 0 <= (sqr F) . i 0 <= (F . i) ^2 by XREAL_1:63; hence 0 <= (sqr F) . i by VALUED_1:11; ::_thesis: verum end; hence 0 <= Sum (sqr F) by Th84; ::_thesis: verum end; theorem Th87: :: RVSUM_1:87 for r being real number for F being real-valued FinSequence holds Sum (r * F) = r * (Sum F) proof let r be real number ; ::_thesis: for F being real-valued FinSequence holds Sum (r * F) = r * (Sum F) let F be real-valued FinSequence; ::_thesis: Sum (r * F) = r * (Sum F) reconsider F1 = F as FinSequence of REAL by Lm2; reconsider s = r as Element of REAL by XREAL_0:def_1; set rM = multreal [;] (s,(id REAL)); thus Sum (r * F) = (multreal [;] (s,(id REAL))) . (addreal $$ F1) by Th3, Th8, SETWOP_2:30 .= r * (Sum F1) by Lm1 .= r * (Sum F) ; ::_thesis: verum end; theorem Th88: :: RVSUM_1:88 for F being real-valued FinSequence holds Sum (- F) = - (Sum F) proof let F be real-valued FinSequence; ::_thesis: Sum (- F) = - (Sum F) reconsider F1 = F as FinSequence of REAL by Lm2; thus Sum (- F) = compreal . (addreal $$ F1) by Th8, Th9, SETWOP_2:31 .= - (Sum F1) by BINOP_2:def_7 .= - (Sum F) ; ::_thesis: verum end; theorem Th89: :: RVSUM_1:89 for i being Nat for R1, R2 being Element of i -tuples_on REAL holds Sum (R1 + R2) = (Sum R1) + (Sum R2) proof let i be Nat; ::_thesis: for R1, R2 being Element of i -tuples_on REAL holds Sum (R1 + R2) = (Sum R1) + (Sum R2) let R1, R2 be Element of i -tuples_on REAL; ::_thesis: Sum (R1 + R2) = (Sum R1) + (Sum R2) thus Sum (R1 + R2) = addreal . ((addreal $$ R1),(addreal $$ R2)) by SETWOP_2:35 .= (Sum R1) + (Sum R2) by BINOP_2:def_9 ; ::_thesis: verum end; theorem Th90: :: RVSUM_1:90 for i being Nat for R1, R2 being Element of i -tuples_on REAL holds Sum (R1 - R2) = (Sum R1) - (Sum R2) proof let i be Nat; ::_thesis: for R1, R2 being Element of i -tuples_on REAL holds Sum (R1 - R2) = (Sum R1) - (Sum R2) let R1, R2 be Element of i -tuples_on REAL; ::_thesis: Sum (R1 - R2) = (Sum R1) - (Sum R2) thus Sum (R1 - R2) = (Sum R1) + (Sum (- R2)) by Th89 .= (Sum R1) + (- (Sum R2)) by Th88 .= (Sum R1) - (Sum R2) ; ::_thesis: verum end; theorem :: RVSUM_1:91 for i being Nat for R being Element of i -tuples_on REAL st Sum (sqr R) = 0 holds R = i |-> 0 proof let i be Nat; ::_thesis: for R being Element of i -tuples_on REAL st Sum (sqr R) = 0 holds R = i |-> 0 let R be Element of i -tuples_on REAL; ::_thesis: ( Sum (sqr R) = 0 implies R = i |-> 0 ) assume A1: Sum (sqr R) = 0 ; ::_thesis: R = i |-> 0 A2: len R = i by CARD_1:def_7; A3: len (i |-> 0) = i by CARD_1:def_7; assume R <> i |-> 0 ; ::_thesis: contradiction then consider j being Nat such that A4: j in dom R and A5: R . j <> (i |-> 0) . j by A2, A3, FINSEQ_2:9; set x = R . j; set x9 = (sqr R) . j; A6: dom R = Seg (len R) by FINSEQ_1:def_3; R . j <> 0 by A5; then 0 < (R . j) ^2 by SQUARE_1:12; then A7: 0 < (sqr R) . j by VALUED_1:11; A8: now__::_thesis:_for_k_being_Nat_st_k_in_dom_(sqr_R)_holds_ 0_<=_(sqr_R)_._k let k be Nat; ::_thesis: ( k in dom (sqr R) implies 0 <= (sqr R) . k ) assume k in dom (sqr R) ; ::_thesis: 0 <= (sqr R) . k set r = (sqr R) . k; set x = R . k; 0 <= (R . k) ^2 by XREAL_1:63; hence 0 <= (sqr R) . k by VALUED_1:11; ::_thesis: verum end; dom (sqr R) = Seg (len (sqr R)) by FINSEQ_1:def_3; then j in dom (sqr R) by A4, A6, FINSEQ_2:33; hence contradiction by A1, A8, A7, Th85; ::_thesis: verum end; theorem :: RVSUM_1:92 for i being Nat for R1, R2 being Element of i -tuples_on REAL holds (Sum (mlt (R1,R2))) ^2 <= (Sum (sqr R1)) * (Sum (sqr R2)) proof let i be Nat; ::_thesis: for R1, R2 being Element of i -tuples_on REAL holds (Sum (mlt (R1,R2))) ^2 <= (Sum (sqr R1)) * (Sum (sqr R2)) let R1, R2 be Element of i -tuples_on REAL; ::_thesis: (Sum (mlt (R1,R2))) ^2 <= (Sum (sqr R1)) * (Sum (sqr R2)) defpred S1[ Nat] means for R1, R2 being Element of $1 -tuples_on REAL holds (Sum (mlt (R1,R2))) ^2 <= (Sum (sqr R1)) * (Sum (sqr R2)); A1: for i being Nat st S1[i] holds S1[i + 1] proof let i be Nat; ::_thesis: ( S1[i] implies S1[i + 1] ) assume A2: for R1, R2 being Element of i -tuples_on REAL holds (Sum (mlt (R1,R2))) ^2 <= (Sum (sqr R1)) * (Sum (sqr R2)) ; ::_thesis: S1[i + 1] let R1, R2 be Element of (i + 1) -tuples_on REAL; ::_thesis: (Sum (mlt (R1,R2))) ^2 <= (Sum (sqr R1)) * (Sum (sqr R2)) consider R19 being Element of i -tuples_on REAL, x1 being Element of REAL such that A3: R1 = R19 ^ <*x1*> by FINSEQ_2:117; consider R29 being Element of i -tuples_on REAL, x2 being Element of REAL such that A4: R2 = R29 ^ <*x2*> by FINSEQ_2:117; A5: for r being real number for R being Element of i -tuples_on REAL holds Sum (sqr (R ^ <*r*>)) = (Sum (sqr R)) + (r ^2) proof let r be real number ; ::_thesis: for R being Element of i -tuples_on REAL holds Sum (sqr (R ^ <*r*>)) = (Sum (sqr R)) + (r ^2) let R be Element of i -tuples_on REAL; ::_thesis: Sum (sqr (R ^ <*r*>)) = (Sum (sqr R)) + (r ^2) reconsider s = r as Element of REAL by XREAL_0:def_1; sqr (R ^ <*s*>) = (sqrreal * R) ^ <*(sqrreal . s)*> by FINSEQOP:8 .= (sqr R) ^ <*(r ^2)*> by Def2 ; hence Sum (sqr (R ^ <*r*>)) = (Sum (sqr R)) + (r ^2) by Th74; ::_thesis: verum end; then A6: (Sum (sqr R29)) + (x2 ^2) = Sum (sqr R2) by A4; ((Sum (mlt (R19,R29))) ^2) + 0 <= (Sum (sqr R19)) * (Sum (sqr R29)) by A2; then A7: 0 <= ((Sum (sqr R19)) * (Sum (sqr R29))) - ((Sum (mlt (R19,R29))) ^2) by XREAL_1:19; mlt ((R19 ^ <*x1*>),(R29 ^ <*x2*>)) = (multreal .: (R19,R29)) ^ <*(multreal . (x1,x2))*> by FINSEQOP:10 .= (mlt (R19,R29)) ^ <*(x1 * x2)*> by BINOP_2:def_11 ; then A8: Sum (mlt ((R19 ^ <*x1*>),(R29 ^ <*x2*>))) = (Sum (mlt (R19,R29))) + (x1 * x2) by Th74; A9: (2 * (x1 * x2)) * (Sum (mlt (R19,R29))) = 2 * ((x1 * x2) * (Sum (mlt (R19,R29)))) .= 2 * (Sum ((x1 * x2) * (mlt (R19,R29)))) by Th87 .= 2 * (Sum (x1 * (x2 * (mlt (R19,R29))))) by RFUNCT_1:17 .= 2 * (Sum (x1 * (mlt (R29,(x2 * R19))))) by RFUNCT_1:12 .= 2 * (Sum (mlt ((x1 * R29),(x2 * R19)))) by FINSEQOP:26 ; A10: - (((Sum (mlt (R19,R29))) + (x1 * x2)) ^2) = (- ((x1 * x2) ^2)) + (- (((2 * (x1 * x2)) * (Sum (mlt (R19,R29)))) + ((Sum (mlt (R19,R29))) ^2))) .= (- ((x1 ^2) * (x2 ^2))) + ((- ((Sum (mlt (R19,R29))) ^2)) + (- (2 * (Sum (mlt ((x1 * R29),(x2 * R19))))))) by A9 ; A11: 0 <= Sum (sqr ((x1 * R29) - (x2 * R19))) by Th86; A12: ((Sum (sqr R19)) + (x1 ^2)) * ((Sum (sqr R29)) + (x2 ^2)) = (((Sum (sqr R19)) * (Sum (sqr R29))) + (((x1 ^2) * (Sum (sqr R29))) + ((Sum (sqr R19)) * (x2 ^2)))) + ((x1 ^2) * (x2 ^2)) .= (((Sum (sqr R19)) * (Sum (sqr R29))) + ((Sum ((x1 ^2) * (sqr R29))) + ((Sum (sqr R19)) * (x2 ^2)))) + ((x1 ^2) * (x2 ^2)) by Th87 .= (((Sum (sqr R19)) * (Sum (sqr R29))) + ((Sum (sqr (x1 * R29))) + ((x2 ^2) * (Sum (sqr R19))))) + ((x1 ^2) * (x2 ^2)) by Th58 .= (((Sum (sqr R19)) * (Sum (sqr R29))) + ((Sum (sqr (x1 * R29))) + (Sum ((x2 ^2) * (sqr R19))))) + ((x1 ^2) * (x2 ^2)) by Th87 .= (((Sum (sqr R19)) * (Sum (sqr R29))) + ((Sum (sqr (x1 * R29))) + (Sum (sqr (x2 * R19))))) + ((x1 ^2) * (x2 ^2)) by Th58 ; A13: ((Sum (sqr (x1 * R29))) + (Sum (sqr (x2 * R19)))) + (- (2 * (Sum (mlt ((x1 * R29),(x2 * R19)))))) = ((Sum (sqr (x1 * R29))) - (2 * (Sum (mlt ((x1 * R29),(x2 * R19)))))) + (Sum (sqr (x2 * R19))) .= ((Sum (sqr (x1 * R29))) - (Sum (2 * (mlt ((x1 * R29),(x2 * R19)))))) + (Sum (sqr (x2 * R19))) by Th87 .= (Sum ((sqr (x1 * R29)) - (2 * (mlt ((x1 * R29),(x2 * R19)))))) + (Sum (sqr (x2 * R19))) by Th90 .= Sum (((sqr (x1 * R29)) - (2 * (mlt ((x1 * R29),(x2 * R19))))) + (sqr (x2 * R19))) by Th89 ; (Sum (sqr R19)) + (x1 ^2) = Sum (sqr R1) by A3, A5; then ((Sum (sqr R1)) * (Sum (sqr R2))) - ((Sum (mlt (R1,R2))) ^2) = (((Sum (sqr R19)) + (x1 ^2)) * ((Sum (sqr R29)) + (x2 ^2))) + (- (((Sum (mlt (R19,R29))) + (x1 * x2)) ^2)) by A3, A4, A8, A6 .= (((Sum (sqr R19)) * (Sum (sqr R29))) + (- ((Sum (mlt (R19,R29))) ^2))) + (((Sum (sqr (x1 * R29))) + (Sum (sqr (x2 * R19)))) + (- (2 * (Sum (mlt ((x1 * R29),(x2 * R19))))))) by A12, A10 .= (((Sum (sqr R19)) * (Sum (sqr R29))) - ((Sum (mlt (R19,R29))) ^2)) + (Sum (sqr ((x1 * R29) - (x2 * R19)))) by A13, Th69 ; then ((Sum (mlt (R1,R2))) ^2) + 0 <= (Sum (sqr R1)) * (Sum (sqr R2)) by A7, A11, XREAL_1:19; hence (Sum (mlt (R1,R2))) ^2 <= (Sum (sqr R1)) * (Sum (sqr R2)) ; ::_thesis: verum end; A14: S1[ 0 ] ; for i being Nat holds S1[i] from NAT_1:sch_2(A14, A1); hence (Sum (mlt (R1,R2))) ^2 <= (Sum (sqr R1)) * (Sum (sqr R2)) ; ::_thesis: verum end; definition let F be complex-valued FinSequence; func Product F -> complex number means :Def13: :: RVSUM_1:def 13 ex f being FinSequence of COMPLEX st ( f = F & it = multcomplex $$ f ); existence ex b1 being complex number ex f being FinSequence of COMPLEX st ( f = F & b1 = multcomplex $$ f ) proof rng F c= COMPLEX by VALUED_0:def_1; then reconsider f = F as FinSequence of COMPLEX by FINSEQ_1:def_4; take multcomplex $$ f ; ::_thesis: ex f being FinSequence of COMPLEX st ( f = F & multcomplex $$ f = multcomplex $$ f ) thus ex f being FinSequence of COMPLEX st ( f = F & multcomplex $$ f = multcomplex $$ f ) ; ::_thesis: verum end; uniqueness for b1, b2 being complex number st ex f being FinSequence of COMPLEX st ( f = F & b1 = multcomplex $$ f ) & ex f being FinSequence of COMPLEX st ( f = F & b2 = multcomplex $$ f ) holds b1 = b2 ; end; :: deftheorem Def13 defines Product RVSUM_1:def_13_:_ for F being complex-valued FinSequence for b2 being complex number holds ( b2 = Product F iff ex f being FinSequence of COMPLEX st ( f = F & b2 = multcomplex $$ f ) ); registration let F be real-valued FinSequence; cluster Product F -> complex real ; coherence Product F is real proof set mc = multcomplex ; consider f being FinSequence of COMPLEX such that A1: f = F and A2: Product F = multcomplex $$ f by Def13; set g = [#] (f,(the_unity_wrt multcomplex)); defpred S1[ Nat] means multcomplex $$ ((finSeg F),([#] (f,(the_unity_wrt multcomplex)))) is real ; A3: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A4: S1[k] ; ::_thesis: S1[k + 1] reconsider k = k as Element of NAT by ORDINAL1:def_12; ([#] (f,(the_unity_wrt multcomplex))) . (k + 1) is real proof percases ( k + 1 in dom f or not k + 1 in dom f ) ; suppose k + 1 in dom f ; ::_thesis: ([#] (f,(the_unity_wrt multcomplex))) . (k + 1) is real then ([#] (f,(the_unity_wrt multcomplex))) . (k + 1) = f . (k + 1) by SETWOP_2:20; hence ([#] (f,(the_unity_wrt multcomplex))) . (k + 1) is real by A1; ::_thesis: verum end; suppose not k + 1 in dom f ; ::_thesis: ([#] (f,(the_unity_wrt multcomplex))) . (k + 1) is real hence ([#] (f,(the_unity_wrt multcomplex))) . (k + 1) is real by BINOP_2:6, SETWOP_2:20; ::_thesis: verum end; end; end; then reconsider a = ([#] (f,(the_unity_wrt multcomplex))) . (k + 1), b = multcomplex $$ ((finSeg k),([#] (f,(the_unity_wrt multcomplex)))) as real number by A4; not k + 1 in Seg k by FINSEQ_3:8; then multcomplex $$ (((finSeg k) \/ {.(k + 1).}),([#] (f,(the_unity_wrt multcomplex)))) = multcomplex . ((multcomplex $$ ((finSeg k),([#] (f,(the_unity_wrt multcomplex))))),(([#] (f,(the_unity_wrt multcomplex))) . (k + 1))) by SETWOP_2:2 .= b * a by BINOP_2:def_5 ; hence S1[k + 1] by FINSEQ_1:9; ::_thesis: verum end; A5: ( multcomplex $$ f = multcomplex $$ ((findom f),([#] (f,(the_unity_wrt multcomplex)))) & ex n being Nat st dom f = Seg n ) by FINSEQ_1:def_2, SETWOP_2:def_2; Seg 0 = {}. NAT ; then A6: S1[ 0 ] by BINOP_2:6, SETWISEO:31; for n being Nat holds S1[n] from NAT_1:sch_2(A6, A3); hence Product F is real by A2, A5; ::_thesis: verum end; end; theorem Th93: :: RVSUM_1:93 for F being FinSequence of REAL holds Product F = multreal $$ F proof set g = multreal ; set h = multcomplex ; let F be FinSequence of REAL ; ::_thesis: Product F = multreal $$ F rng F c= COMPLEX by NUMBERS:11, XBOOLE_1:1; then reconsider f = F as FinSequence of COMPLEX by FINSEQ_1:def_4; defpred S1[ Nat] means multreal $$ ((finSeg $1),([#] (F,(the_unity_wrt multreal)))) = multcomplex $$ ((finSeg $1),([#] (f,(the_unity_wrt multcomplex)))); consider n being Nat such that A1: dom f = Seg n by FINSEQ_1:def_2; A2: ( multreal $$ F = multreal $$ ((finSeg n),([#] (F,(the_unity_wrt multreal)))) & multcomplex $$ f = multcomplex $$ ((finSeg n),([#] (f,(the_unity_wrt multcomplex)))) ) by A1, SETWOP_2:def_2; A3: for k being Nat st S1[k] holds S1[k + 1] proof set j = [#] (f,(the_unity_wrt multcomplex)); set i = [#] (F,(the_unity_wrt multreal)); let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A4: S1[k] ; ::_thesis: S1[k + 1] A5: ([#] (F,(the_unity_wrt multreal))) . (k + 1) = ([#] (f,(the_unity_wrt multcomplex))) . (k + 1) proof percases ( k + 1 in dom f or not k + 1 in dom f ) ; supposeA6: k + 1 in dom f ; ::_thesis: ([#] (F,(the_unity_wrt multreal))) . (k + 1) = ([#] (f,(the_unity_wrt multcomplex))) . (k + 1) then ([#] (f,(the_unity_wrt multcomplex))) . (k + 1) = F . (k + 1) by SETWOP_2:20 .= ([#] (F,(the_unity_wrt multreal))) . (k + 1) by A6, SETWOP_2:20 ; hence ([#] (F,(the_unity_wrt multreal))) . (k + 1) = ([#] (f,(the_unity_wrt multcomplex))) . (k + 1) ; ::_thesis: verum end; supposeA7: not k + 1 in dom f ; ::_thesis: ([#] (F,(the_unity_wrt multreal))) . (k + 1) = ([#] (f,(the_unity_wrt multcomplex))) . (k + 1) then ([#] (f,(the_unity_wrt multcomplex))) . (k + 1) = the_unity_wrt multcomplex by SETWOP_2:20 .= ([#] (F,(the_unity_wrt multreal))) . (k + 1) by A7, BINOP_2:6, BINOP_2:7, SETWOP_2:20 ; hence ([#] (F,(the_unity_wrt multreal))) . (k + 1) = ([#] (f,(the_unity_wrt multcomplex))) . (k + 1) ; ::_thesis: verum end; end; end; A8: not k + 1 in Seg k by FINSEQ_3:8; reconsider k = k as Element of NAT by ORDINAL1:def_12; multreal $$ ((finSeg (k + 1)),([#] (F,(the_unity_wrt multreal)))) = multreal $$ (((finSeg k) \/ {.(k + 1).}),([#] (F,(the_unity_wrt multreal)))) by FINSEQ_1:9 .= multreal . ((multreal $$ ((finSeg k),([#] (F,(the_unity_wrt multreal))))),(([#] (F,(the_unity_wrt multreal))) . (k + 1))) by A8, SETWOP_2:2 .= (multreal $$ ((finSeg k),([#] (F,(the_unity_wrt multreal))))) * (([#] (F,(the_unity_wrt multreal))) . (k + 1)) by BINOP_2:def_11 .= multcomplex . ((multcomplex $$ ((finSeg k),([#] (f,(the_unity_wrt multcomplex))))),(([#] (f,(the_unity_wrt multcomplex))) . (k + 1))) by A4, A5, BINOP_2:def_5 .= multcomplex $$ (((finSeg k) \/ {.(k + 1).}),([#] (f,(the_unity_wrt multcomplex)))) by A8, SETWOP_2:2 .= multcomplex $$ ((finSeg (k + 1)),([#] (f,(the_unity_wrt multcomplex)))) by FINSEQ_1:9 ; hence S1[k + 1] ; ::_thesis: verum end; A9: Seg 0 = {}. NAT ; then multreal $$ ((finSeg 0),([#] (F,(the_unity_wrt multreal)))) = the_unity_wrt multcomplex by BINOP_2:6, BINOP_2:7, SETWISEO:31 .= multcomplex $$ ((finSeg 0),([#] (f,(the_unity_wrt multcomplex)))) by A9, SETWISEO:31 ; then A10: S1[ 0 ] ; for k being Nat holds S1[k] from NAT_1:sch_2(A10, A3); then multreal $$ F = multcomplex $$ f by A2; hence Product F = multreal $$ F by Def13; ::_thesis: verum end; definition let F be FinSequence of COMPLEX ; :: original: Product redefine func Product F -> Element of COMPLEX equals :: RVSUM_1:def 14 multcomplex $$ F; coherence Product F is Element of COMPLEX by XCMPLX_0:def_2; compatibility for b1 being Element of COMPLEX holds ( b1 = Product F iff b1 = multcomplex $$ F ) by Def13; end; :: deftheorem defines Product RVSUM_1:def_14_:_ for F being FinSequence of COMPLEX holds Product F = multcomplex $$ F; definition let F be FinSequence of REAL ; :: original: Product redefine func Product F -> Element of REAL equals :: RVSUM_1:def 15 multreal $$ F; coherence Product F is Element of REAL by XREAL_0:def_1; compatibility for b1 being Element of REAL holds ( b1 = Product F iff b1 = multreal $$ F ) by Th93; end; :: deftheorem defines Product RVSUM_1:def_15_:_ for F being FinSequence of REAL holds Product F = multreal $$ F; Lm3: for F being empty FinSequence holds Product F = 1 proof Product (<*> REAL) = 1 by BINOP_2:7, FINSOP_1:10; hence for F being empty FinSequence holds Product F = 1 ; ::_thesis: verum end; theorem Th94: :: RVSUM_1:94 Product (<*> REAL) = 1 by Lm3; registration let r be complex number ; cluster<*r*> -> complex-valued ; coherence <*r*> is complex-yielding proof reconsider p = r as Element of COMPLEX by XCMPLX_0:def_2; reconsider f = <*p*> as FinSequence of COMPLEX ; f is FinSequence-like ; hence <*r*> is complex-yielding ; ::_thesis: verum end; end; registration let r1, r2 be complex number ; cluster<*r1,r2*> -> complex-valued ; coherence <*r1,r2*> is complex-yielding proof reconsider p1 = r1, p2 = r2 as Element of COMPLEX by XCMPLX_0:def_2; reconsider f = <*p1,p2*> as FinSequence of COMPLEX ; f is FinSequence-like ; hence <*r1,r2*> is complex-yielding ; ::_thesis: verum end; end; registration let r1, r2, r3 be complex number ; cluster<*r1,r2,r3*> -> complex-valued ; coherence <*r1,r2,r3*> is complex-yielding proof reconsider p1 = r1, p2 = r2, p3 = r3 as Element of COMPLEX by XCMPLX_0:def_2; reconsider f = <*p1,p2,p3*> as FinSequence of COMPLEX ; f is FinSequence-like ; hence <*r1,r2,r3*> is complex-yielding ; ::_thesis: verum end; end; theorem Th95: :: RVSUM_1:95 for r being complex number holds Product <*r*> = r proof let r be complex number ; ::_thesis: Product <*r*> = r reconsider r9 = r as Element of COMPLEX by XCMPLX_0:def_2; reconsider F = <*r9*> as FinSequence of COMPLEX ; multcomplex $$ F = r by FINSOP_1:11; hence Product <*r*> = r by Def13; ::_thesis: verum end; registration let f, g be complex-valued FinSequence; clusterf ^ g -> complex-valued ; coherence f ^ g is complex-yielding proof A1: rng (f ^ g) = (rng f) \/ (rng g) by FINSEQ_1:31; ( rng f c= COMPLEX & rng g c= COMPLEX ) by VALUED_0:def_1; then rng (f ^ g) c= COMPLEX by A1, XBOOLE_1:8; hence f ^ g is complex-yielding by VALUED_0:def_1; ::_thesis: verum end; end; theorem Th96: :: RVSUM_1:96 for F being complex-valued FinSequence for r being complex number holds Product (F ^ <*r*>) = (Product F) * r proof let F be complex-valued FinSequence; ::_thesis: for r being complex number holds Product (F ^ <*r*>) = (Product F) * r let r be complex number ; ::_thesis: Product (F ^ <*r*>) = (Product F) * r reconsider p = r as Element of COMPLEX by XCMPLX_0:def_2; ( rng F c= COMPLEX & rng (F ^ <*p*>) c= COMPLEX ) by VALUED_0:def_1; then reconsider Fr = F ^ <*r*>, Ff = F as FinSequence of COMPLEX by FINSEQ_1:def_4; thus Product (F ^ <*r*>) = multcomplex $$ Fr by Def13 .= multcomplex . ((Product Ff),p) by FINSOP_1:4 .= (Product F) * r by BINOP_2:def_5 ; ::_thesis: verum end; theorem Th97: :: RVSUM_1:97 for F1, F2 being complex-valued FinSequence holds Product (F1 ^ F2) = (Product F1) * (Product F2) proof let F1, F2 be complex-valued FinSequence; ::_thesis: Product (F1 ^ F2) = (Product F1) * (Product F2) A1: rng (F1 ^ F2) c= COMPLEX by VALUED_0:def_1; ( rng F1 c= COMPLEX & rng F2 c= COMPLEX ) by VALUED_0:def_1; then reconsider FF = F1 ^ F2, f1 = F1, f2 = F2 as FinSequence of COMPLEX by A1, FINSEQ_1:def_4; thus Product (F1 ^ F2) = multcomplex $$ FF by Def13 .= multcomplex . ((Product f1),(Product f2)) by FINSOP_1:5 .= (Product F1) * (Product F2) by BINOP_2:def_5 ; ::_thesis: verum end; theorem :: RVSUM_1:98 for r being real number for F being real-valued FinSequence holds Product (<*r*> ^ F) = r * (Product F) proof let r be real number ; ::_thesis: for F being real-valued FinSequence holds Product (<*r*> ^ F) = r * (Product F) let F be real-valued FinSequence; ::_thesis: Product (<*r*> ^ F) = r * (Product F) thus Product (<*r*> ^ F) = (Product <*r*>) * (Product F) by Th97 .= r * (Product F) by Th95 ; ::_thesis: verum end; theorem Th99: :: RVSUM_1:99 for r1, r2 being complex number holds Product <*r1,r2*> = r1 * r2 proof let r1, r2 be complex number ; ::_thesis: Product <*r1,r2*> = r1 * r2 thus Product <*r1,r2*> = (Product <*r1*>) * r2 by Th96 .= r1 * r2 by Th95 ; ::_thesis: verum end; theorem :: RVSUM_1:100 for r1, r2, r3 being complex number holds Product <*r1,r2,r3*> = (r1 * r2) * r3 proof let r1, r2, r3 be complex number ; ::_thesis: Product <*r1,r2,r3*> = (r1 * r2) * r3 thus Product <*r1,r2,r3*> = (Product <*r1,r2*>) * r3 by Th96 .= (r1 * r2) * r3 by Th99 ; ::_thesis: verum end; theorem :: RVSUM_1:101 for R being Element of 0 -tuples_on REAL holds Product R = 1 by Lm3; theorem :: RVSUM_1:102 for i being Nat holds Product (i |-> 1) = 1 proof let i be Nat; ::_thesis: Product (i |-> 1) = 1 Product (i |-> (the_unity_wrt multreal)) = the_unity_wrt multreal by SETWOP_2:25; hence Product (i |-> 1) = 1 by BINOP_2:7; ::_thesis: verum end; Lm4: for p being complex-valued FinSequence st len p <> 0 holds ex q being complex-valued FinSequence ex d being complex number st p = q ^ <*d*> proof let p be complex-valued FinSequence; ::_thesis: ( len p <> 0 implies ex q being complex-valued FinSequence ex d being complex number st p = q ^ <*d*> ) assume len p <> 0 ; ::_thesis: ex q being complex-valued FinSequence ex d being complex number st p = q ^ <*d*> then consider q being FinSequence, d being set such that A1: p = q ^ <*d*> by CARD_1:27, FINSEQ_1:46; rng p c= COMPLEX by VALUED_0:def_1; then A2: p is FinSequence of COMPLEX by FINSEQ_1:def_4; for i being Nat st i in dom q holds q . i in COMPLEX proof let i be Nat; ::_thesis: ( i in dom q implies q . i in COMPLEX ) assume i in dom q ; ::_thesis: q . i in COMPLEX then ( p . i = q . i & i in dom p ) by A1, FINSEQ_1:def_7, FINSEQ_2:15; hence q . i in COMPLEX by A2, FINSEQ_2:11; ::_thesis: verum end; then A3: q is FinSequence of COMPLEX by FINSEQ_2:12; len p = (len q) + 1 by A1, FINSEQ_2:16; then p . (len p) = d by A1, FINSEQ_1:42; hence ex q being complex-valued FinSequence ex d being complex number st p = q ^ <*d*> by A1, A3; ::_thesis: verum end; theorem :: RVSUM_1:103 for F being complex-valued FinSequence holds ( ex k being Nat st ( k in dom F & F . k = 0 ) iff Product F = 0 ) proof defpred S1[ Nat] means for F being complex-valued FinSequence st len F = $1 holds ( ex k being Nat st ( k in Seg $1 & F . k = 0 ) iff Product F = 0 ); let F be complex-valued FinSequence; ::_thesis: ( ex k being Nat st ( k in dom F & F . k = 0 ) iff Product F = 0 ) A1: Seg (len F) = dom F by FINSEQ_1:def_3; A2: for i being Nat st S1[i] holds S1[i + 1] proof let i be Nat; ::_thesis: ( S1[i] implies S1[i + 1] ) assume A3: for F being complex-valued FinSequence st len F = i holds ( ex k being Nat st ( k in Seg i & F . k = 0 ) iff Product F = 0 ) ; ::_thesis: S1[i + 1] let F be complex-valued FinSequence; ::_thesis: ( len F = i + 1 implies ( ex k being Nat st ( k in Seg (i + 1) & F . k = 0 ) iff Product F = 0 ) ) assume A4: len F = i + 1 ; ::_thesis: ( ex k being Nat st ( k in Seg (i + 1) & F . k = 0 ) iff Product F = 0 ) then consider F9 being complex-valued FinSequence, x being complex number such that A5: F = F9 ^ <*x*> by Lm4; A6: len F = (len F9) + 1 by A5, FINSEQ_2:16; A7: Product F = (Product F9) * x by A5, Th96; thus ( ex k being Nat st ( k in Seg (i + 1) & F . k = 0 ) implies Product F = 0 ) ::_thesis: ( Product F = 0 implies ex k being Nat st ( k in Seg (i + 1) & F . k = 0 ) ) proof given k being Nat such that A8: k in Seg (i + 1) and A9: F . k = 0 ; ::_thesis: Product F = 0 now__::_thesis:_Product_F_=_0 percases ( k in Seg i or k = i + 1 ) by A8, FINSEQ_2:7; supposeA10: k in Seg i ; ::_thesis: Product F = 0 Seg (len F9) = dom F9 by FINSEQ_1:def_3; then F9 . k = F . k by A4, A5, A6, A10, FINSEQ_1:def_7; then Product F9 = 0 by A3, A4, A6, A9, A10; hence Product F = 0 by A7; ::_thesis: verum end; suppose k = i + 1 ; ::_thesis: Product F = 0 then x = 0 by A4, A5, A6, A9, FINSEQ_1:42; hence Product F = 0 by A7; ::_thesis: verum end; end; end; hence Product F = 0 ; ::_thesis: verum end; assume A11: Product F = 0 ; ::_thesis: ex k being Nat st ( k in Seg (i + 1) & F . k = 0 ) percases ( Product F9 = 0 or x = 0 ) by A7, A11; suppose Product F9 = 0 ; ::_thesis: ex k being Nat st ( k in Seg (i + 1) & F . k = 0 ) then consider k being Nat such that A12: k in Seg i and A13: F9 . k = 0 by A3, A4, A6; Seg (len F9) = dom F9 by FINSEQ_1:def_3; then F . k = 0 by A4, A5, A6, A12, A13, FINSEQ_1:def_7; hence ex k being Nat st ( k in Seg (i + 1) & F . k = 0 ) by A12, FINSEQ_2:8; ::_thesis: verum end; suppose x = 0 ; ::_thesis: ex k being Nat st ( k in Seg (i + 1) & F . k = 0 ) then F . (i + 1) = 0 by A4, A5, A6, FINSEQ_1:42; hence ex k being Nat st ( k in Seg (i + 1) & F . k = 0 ) by FINSEQ_1:4; ::_thesis: verum end; end; end; A14: S1[ 0 ] proof let F be complex-valued FinSequence; ::_thesis: ( len F = 0 implies ( ex k being Nat st ( k in Seg 0 & F . k = 0 ) iff Product F = 0 ) ) assume len F = 0 ; ::_thesis: ( ex k being Nat st ( k in Seg 0 & F . k = 0 ) iff Product F = 0 ) then F = <*> COMPLEX ; hence ( ex k being Nat st ( k in Seg 0 & F . k = 0 ) iff Product F = 0 ) by Th94; ::_thesis: verum end; for i being Nat holds S1[i] from NAT_1:sch_2(A14, A2); hence ( ex k being Nat st ( k in dom F & F . k = 0 ) iff Product F = 0 ) by A1; ::_thesis: verum end; theorem :: RVSUM_1:104 for i, j being Nat for r being real number holds Product ((i + j) |-> r) = (Product (i |-> r)) * (Product (j |-> r)) proof let i, j be Nat; ::_thesis: for r being real number holds Product ((i + j) |-> r) = (Product (i |-> r)) * (Product (j |-> r)) let r be real number ; ::_thesis: Product ((i + j) |-> r) = (Product (i |-> r)) * (Product (j |-> r)) reconsider s = r as Element of REAL by XREAL_0:def_1; Product ((i + j) |-> s) = multreal . ((multreal $$ (i |-> s)),(multreal $$ (j |-> s))) by SETWOP_2:26 .= (Product (i |-> s)) * (Product (j |-> s)) by BINOP_2:def_11 ; hence Product ((i + j) |-> r) = (Product (i |-> r)) * (Product (j |-> r)) ; ::_thesis: verum end; theorem :: RVSUM_1:105 for i, j being Nat for r being real number holds Product ((i * j) |-> r) = Product (j |-> (Product (i |-> r))) proof let i, j be Nat; ::_thesis: for r being real number holds Product ((i * j) |-> r) = Product (j |-> (Product (i |-> r))) let r be real number ; ::_thesis: Product ((i * j) |-> r) = Product (j |-> (Product (i |-> r))) reconsider r = r as Element of REAL by XREAL_0:def_1; Product ((i * j) |-> r) = Product (j |-> (Product (i |-> r))) by SETWOP_2:27; hence Product ((i * j) |-> r) = Product (j |-> (Product (i |-> r))) ; ::_thesis: verum end; theorem :: RVSUM_1:106 for i being Nat for r1, r2 being real number holds Product (i |-> (r1 * r2)) = (Product (i |-> r1)) * (Product (i |-> r2)) proof let i be Nat; ::_thesis: for r1, r2 being real number holds Product (i |-> (r1 * r2)) = (Product (i |-> r1)) * (Product (i |-> r2)) let r1, r2 be real number ; ::_thesis: Product (i |-> (r1 * r2)) = (Product (i |-> r1)) * (Product (i |-> r2)) reconsider s1 = r1, s2 = r2 as Element of REAL by XREAL_0:def_1; Product (i |-> (s1 * s2)) = multreal $$ (i |-> (multreal . (s1,s2))) by BINOP_2:def_11 .= multreal . ((multreal $$ (i |-> s1)),(multreal $$ (i |-> s2))) by SETWOP_2:36 .= (Product (i |-> s1)) * (Product (i |-> s2)) by BINOP_2:def_11 ; hence Product (i |-> (r1 * r2)) = (Product (i |-> r1)) * (Product (i |-> r2)) ; ::_thesis: verum end; theorem Th107: :: RVSUM_1:107 for i being Nat for R1, R2 being Element of i -tuples_on REAL holds Product (mlt (R1,R2)) = (Product R1) * (Product R2) proof let i be Nat; ::_thesis: for R1, R2 being Element of i -tuples_on REAL holds Product (mlt (R1,R2)) = (Product R1) * (Product R2) let R1, R2 be Element of i -tuples_on REAL; ::_thesis: Product (mlt (R1,R2)) = (Product R1) * (Product R2) thus Product (mlt (R1,R2)) = multreal . ((multreal $$ R1),(multreal $$ R2)) by SETWOP_2:35 .= (Product R1) * (Product R2) by BINOP_2:def_11 ; ::_thesis: verum end; theorem :: RVSUM_1:108 for i being Nat for r being real number for R being Element of i -tuples_on REAL holds Product (r * R) = (Product (i |-> r)) * (Product R) proof let i be Nat; ::_thesis: for r being real number for R being Element of i -tuples_on REAL holds Product (r * R) = (Product (i |-> r)) * (Product R) let r be real number ; ::_thesis: for R being Element of i -tuples_on REAL holds Product (r * R) = (Product (i |-> r)) * (Product R) let R be Element of i -tuples_on REAL; ::_thesis: Product (r * R) = (Product (i |-> r)) * (Product R) reconsider s = r as Element of REAL by XREAL_0:def_1; thus Product (r * R) = Product (mlt ((i |-> s),R)) by Th63 .= (Product (i |-> r)) * (Product R) by Th107 ; ::_thesis: verum end; theorem :: RVSUM_1:109 for i being Nat for R being Element of i -tuples_on REAL holds Product (sqr R) = (Product R) ^2 by Th107; begin theorem :: RVSUM_1:110 for F being FinSequence of COMPLEX holds Product F = multcomplex $$ F ; theorem :: RVSUM_1:111 for i, j being Nat for z being Element of COMPLEX holds Product ((i + j) |-> z) = (Product (i |-> z)) * (Product (j |-> z)) proof let i, j be Nat; ::_thesis: for z being Element of COMPLEX holds Product ((i + j) |-> z) = (Product (i |-> z)) * (Product (j |-> z)) let z be Element of COMPLEX ; ::_thesis: Product ((i + j) |-> z) = (Product (i |-> z)) * (Product (j |-> z)) thus Product ((i + j) |-> z) = multcomplex . ((multcomplex $$ (i |-> z)),(multcomplex $$ (j |-> z))) by SETWOP_2:26 .= (Product (i |-> z)) * (Product (j |-> z)) by BINOP_2:def_5 ; ::_thesis: verum end; theorem :: RVSUM_1:112 for i, j being Nat for z being Element of COMPLEX holds Product ((i * j) |-> z) = Product (j |-> (Product (i |-> z))) by SETWOP_2:27; theorem :: RVSUM_1:113 for i being Nat for z1, z2 being Element of COMPLEX holds Product (i |-> (z1 * z2)) = (Product (i |-> z1)) * (Product (i |-> z2)) proof let i be Nat; ::_thesis: for z1, z2 being Element of COMPLEX holds Product (i |-> (z1 * z2)) = (Product (i |-> z1)) * (Product (i |-> z2)) let z1, z2 be Element of COMPLEX ; ::_thesis: Product (i |-> (z1 * z2)) = (Product (i |-> z1)) * (Product (i |-> z2)) thus Product (i |-> (z1 * z2)) = multcomplex $$ (i |-> (multcomplex . (z1,z2))) by BINOP_2:def_5 .= multcomplex . ((multcomplex $$ (i |-> z1)),(multcomplex $$ (i |-> z2))) by SETWOP_2:36 .= (Product (i |-> z1)) * (Product (i |-> z2)) by BINOP_2:def_5 ; ::_thesis: verum end; begin theorem Th114: :: RVSUM_1:114 for x being real-valued FinSequence holds len (- x) = len x proof let x be real-valued FinSequence; ::_thesis: len (- x) = len x dom (- x) = dom x by VALUED_1:8; hence len (- x) = len x by FINSEQ_3:29; ::_thesis: verum end; theorem Th115: :: RVSUM_1:115 for x1, x2 being real-valued FinSequence st len x1 = len x2 holds len (x1 + x2) = len x1 proof let x1, x2 be real-valued FinSequence; ::_thesis: ( len x1 = len x2 implies len (x1 + x2) = len x1 ) set n = len x1; A1: x2 is FinSequence of REAL by Lm2; x1 is FinSequence of REAL by Lm2; then reconsider z1 = x1 as Element of (len x1) -tuples_on REAL by FINSEQ_2:92; assume len x1 = len x2 ; ::_thesis: len (x1 + x2) = len x1 then reconsider z2 = x2 as Element of (len x1) -tuples_on REAL by A1, FINSEQ_2:92; dom (z1 + z2) = Seg (len x1) by FINSEQ_2:124; hence len (x1 + x2) = len x1 by FINSEQ_1:def_3; ::_thesis: verum end; theorem Th116: :: RVSUM_1:116 for x1, x2 being real-valued FinSequence st len x1 = len x2 holds len (x1 - x2) = len x1 proof let x1, x2 be real-valued FinSequence; ::_thesis: ( len x1 = len x2 implies len (x1 - x2) = len x1 ) set n = len x1; A1: x2 is FinSequence of REAL by Lm2; x1 is FinSequence of REAL by Lm2; then reconsider z1 = x1 as Element of (len x1) -tuples_on REAL by FINSEQ_2:92; assume len x1 = len x2 ; ::_thesis: len (x1 - x2) = len x1 then reconsider z2 = x2 as Element of (len x1) -tuples_on REAL by A1, FINSEQ_2:92; dom (z1 - z2) = Seg (len x1) by FINSEQ_2:124; hence len (x1 - x2) = len x1 by FINSEQ_1:def_3; ::_thesis: verum end; theorem Th117: :: RVSUM_1:117 for a being real number for x being real-valued FinSequence holds len (a * x) = len x proof let a be real number ; ::_thesis: for x being real-valued FinSequence holds len (a * x) = len x let x be real-valued FinSequence; ::_thesis: len (a * x) = len x set n = len x; x is FinSequence of REAL by Lm2; then reconsider z = x as Element of (len x) -tuples_on REAL by FINSEQ_2:92; len (a * z) = len x by CARD_1:def_7; hence len (a * x) = len x ; ::_thesis: verum end; theorem Th118: :: RVSUM_1:118 for x, y, z being real-valued FinSequence st len x = len y & len y = len z holds mlt ((x + y),z) = (mlt (x,z)) + (mlt (y,z)) proof let x, y, z be real-valued FinSequence; ::_thesis: ( len x = len y & len y = len z implies mlt ((x + y),z) = (mlt (x,z)) + (mlt (y,z)) ) A1: ( x is FinSequence of REAL & y is FinSequence of REAL & z is FinSequence of REAL ) by Lm2; assume ( len x = len y & len y = len z ) ; ::_thesis: mlt ((x + y),z) = (mlt (x,z)) + (mlt (y,z)) then reconsider x2 = x, y2 = y, z2 = z as Element of (len x) -tuples_on REAL by A1, FINSEQ_2:92; A2: dom (mlt ((x + y),z)) = Seg (len (mlt ((x2 + y2),z2))) by FINSEQ_1:def_3 .= Seg (len x) by CARD_1:def_7 .= Seg (len ((mlt (x2,z2)) + (mlt (y2,z2)))) by CARD_1:def_7 .= dom ((mlt (x2,z2)) + (mlt (y2,z2))) by FINSEQ_1:def_3 ; A3: dom (mlt (x,z)) = Seg (len (mlt (x2,z2))) by FINSEQ_1:def_3 .= Seg (len x) by CARD_1:def_7 .= Seg (len ((mlt (x2,z2)) + (mlt (y2,z2)))) by CARD_1:def_7 .= dom ((mlt (x2,z2)) + (mlt (y2,z2))) by FINSEQ_1:def_3 ; for i being Nat st i in dom (mlt ((x + y),z)) holds (mlt ((x + y),z)) . i = ((mlt (x,z)) + (mlt (y,z))) . i proof let i be Nat; ::_thesis: ( i in dom (mlt ((x + y),z)) implies (mlt ((x + y),z)) . i = ((mlt (x,z)) + (mlt (y,z))) . i ) assume A4: i in dom (mlt ((x + y),z)) ; ::_thesis: (mlt ((x + y),z)) . i = ((mlt (x,z)) + (mlt (y,z))) . i set a = x . i; set b = y . i; set d = (x + y) . i; set e = z . i; len (x2 + y2) = len x by CARD_1:def_7; then dom (x2 + y2) = Seg (len x) by FINSEQ_1:def_3 .= Seg (len (mlt (x2,z2))) by CARD_1:def_7 .= dom (mlt (x,z)) by FINSEQ_1:def_3 ; then A5: (x + y) . i = (x . i) + (y . i) by A2, A3, A4, VALUED_1:def_1; thus (mlt ((x + y),z)) . i = ((x + y) . i) * (z . i) by VALUED_1:5 .= ((x . i) * (z . i)) + ((y . i) * (z . i)) by A5 .= ((mlt (x,z)) . i) + ((y . i) * (z . i)) by VALUED_1:5 .= ((mlt (x,z)) . i) + ((mlt (y,z)) . i) by VALUED_1:5 .= ((mlt (x,z)) + (mlt (y,z))) . i by A2, A4, VALUED_1:def_1 ; ::_thesis: verum end; hence mlt ((x + y),z) = (mlt (x,z)) + (mlt (y,z)) by A2, FINSEQ_1:13; ::_thesis: verum end; begin definition let x1, x2 be real-valued FinSequence; func|(x1,x2)| -> real number equals :: RVSUM_1:def 16 Sum (mlt (x1,x2)); correctness coherence Sum (mlt (x1,x2)) is real number ; ; commutativity for b1 being real number for x1, x2 being real-valued FinSequence st b1 = Sum (mlt (x1,x2)) holds b1 = Sum (mlt (x2,x1)) ; end; :: deftheorem defines |( RVSUM_1:def_16_:_ for x1, x2 being real-valued FinSequence holds |(x1,x2)| = Sum (mlt (x1,x2)); definition let x1, x2 be real-valued FinSequence; :: original: |( redefine func|(x1,x2)| -> Element of REAL ; correctness coherence |(x1,x2)| is Element of REAL ; ; commutativity for x1, x2 being real-valued FinSequence holds |(x1,x2)| = |(x2,x1)| ; end; theorem Th119: :: RVSUM_1:119 for x being real-valued FinSequence holds |(x,x)| >= 0 proof let x be real-valued FinSequence; ::_thesis: |(x,x)| >= 0 set n = len x; x is FinSequence of REAL by Lm2; then reconsider w = x as Element of (len x) -tuples_on REAL by FINSEQ_2:92; |(x,x)| = Sum (sqr w) ; hence |(x,x)| >= 0 by Th86; ::_thesis: verum end; theorem Th120: :: RVSUM_1:120 for x, y, z being real-valued FinSequence st len x = len y & len y = len z holds |((x + y),z)| = |(x,z)| + |(y,z)| proof let x, y, z be real-valued FinSequence; ::_thesis: ( len x = len y & len y = len z implies |((x + y),z)| = |(x,z)| + |(y,z)| ) A1: ( x is FinSequence of REAL & y is FinSequence of REAL & z is FinSequence of REAL ) by Lm2; assume A2: ( len x = len y & len y = len z ) ; ::_thesis: |((x + y),z)| = |(x,z)| + |(y,z)| then reconsider x2 = x, y2 = y, z2 = z as Element of (len x) -tuples_on REAL by A1, FINSEQ_2:92; |((x + y),z)| = Sum ((mlt (x,z)) + (mlt (y,z))) by A2, Th118 .= (Sum (mlt (x2,z2))) + (Sum (mlt (y2,z2))) by Th89 .= |(x,z)| + |(y,z)| ; hence |((x + y),z)| = |(x,z)| + |(y,z)| ; ::_thesis: verum end; theorem Th121: :: RVSUM_1:121 for x, y being real-valued FinSequence for a being real number st len x = len y holds |((a * x),y)| = a * |(x,y)| proof let x, y be real-valued FinSequence; ::_thesis: for a being real number st len x = len y holds |((a * x),y)| = a * |(x,y)| let a be real number ; ::_thesis: ( len x = len y implies |((a * x),y)| = a * |(x,y)| ) reconsider a2 = a as Element of REAL by XREAL_0:def_1; A1: ( x is FinSequence of REAL & y is FinSequence of REAL ) by Lm2; assume len x = len y ; ::_thesis: |((a * x),y)| = a * |(x,y)| then reconsider x2 = x, y2 = y as Element of (len x) -tuples_on REAL by A1, FINSEQ_2:92; |((a * x),y)| = Sum (a2 * (mlt (x2,y2))) by FINSEQOP:26 .= a * |(x,y)| by Th87 ; hence |((a * x),y)| = a * |(x,y)| ; ::_thesis: verum end; theorem Th122: :: RVSUM_1:122 for x1, x2 being real-valued FinSequence st len x1 = len x2 holds |((- x1),x2)| = - |(x1,x2)| proof let x1, x2 be real-valued FinSequence; ::_thesis: ( len x1 = len x2 implies |((- x1),x2)| = - |(x1,x2)| ) assume len x1 = len x2 ; ::_thesis: |((- x1),x2)| = - |(x1,x2)| then |((- x1),x2)| = (- 1) * |(x1,x2)| by Th121; hence |((- x1),x2)| = - |(x1,x2)| ; ::_thesis: verum end; theorem :: RVSUM_1:123 for x1, x2 being real-valued FinSequence st len x1 = len x2 holds |((- x1),(- x2))| = |(x1,x2)| proof let x1, x2 be real-valued FinSequence; ::_thesis: ( len x1 = len x2 implies |((- x1),(- x2))| = |(x1,x2)| ) assume A1: len x1 = len x2 ; ::_thesis: |((- x1),(- x2))| = |(x1,x2)| then len (- x2) = len x1 by Th114; then |((- x1),(- x2))| = - |(x1,(- x2))| by Th122 .= - (- |(x1,x2)|) by A1, Th122 ; hence |((- x1),(- x2))| = |(x1,x2)| ; ::_thesis: verum end; theorem Th124: :: RVSUM_1:124 for x1, x2, x3 being real-valued FinSequence st len x1 = len x2 & len x2 = len x3 holds |((x1 - x2),x3)| = |(x1,x3)| - |(x2,x3)| proof let x1, x2, x3 be real-valued FinSequence; ::_thesis: ( len x1 = len x2 & len x2 = len x3 implies |((x1 - x2),x3)| = |(x1,x3)| - |(x2,x3)| ) assume that A1: len x1 = len x2 and A2: len x2 = len x3 ; ::_thesis: |((x1 - x2),x3)| = |(x1,x3)| - |(x2,x3)| len (- x2) = len x2 by Th114; then |((x1 - x2),x3)| = |(x1,x3)| + |((- x2),x3)| by A1, A2, Th120 .= |(x1,x3)| + (- |(x2,x3)|) by A2, Th122 ; hence |((x1 - x2),x3)| = |(x1,x3)| - |(x2,x3)| ; ::_thesis: verum end; theorem :: RVSUM_1:125 for x, y being real number for x1, x2, x3 being real-valued FinSequence st len x1 = len x2 & len x2 = len x3 holds |(((x * x1) + (y * x2)),x3)| = (x * |(x1,x3)|) + (y * |(x2,x3)|) proof let x, y be real number ; ::_thesis: for x1, x2, x3 being real-valued FinSequence st len x1 = len x2 & len x2 = len x3 holds |(((x * x1) + (y * x2)),x3)| = (x * |(x1,x3)|) + (y * |(x2,x3)|) let x1, x2, x3 be real-valued FinSequence; ::_thesis: ( len x1 = len x2 & len x2 = len x3 implies |(((x * x1) + (y * x2)),x3)| = (x * |(x1,x3)|) + (y * |(x2,x3)|) ) assume that A1: len x1 = len x2 and A2: len x2 = len x3 ; ::_thesis: |(((x * x1) + (y * x2)),x3)| = (x * |(x1,x3)|) + (y * |(x2,x3)|) ( len (x * x1) = len x1 & len (y * x2) = len x2 ) by Th117; then |(((x * x1) + (y * x2)),x3)| = |((x * x1),x3)| + |((y * x2),x3)| by A1, A2, Th120 .= (x * |(x1,x3)|) + |((y * x2),x3)| by A1, A2, Th121 .= (x * |(x1,x3)|) + (y * |(x2,x3)|) by A2, Th121 ; hence |(((x * x1) + (y * x2)),x3)| = (x * |(x1,x3)|) + (y * |(x2,x3)|) ; ::_thesis: verum end; theorem Th126: :: RVSUM_1:126 for x1, x2, y1, y2 being real-valued FinSequence st len x1 = len x2 & len x2 = len y1 & len y1 = len y2 holds |((x1 + x2),(y1 + y2))| = ((|(x1,y1)| + |(x1,y2)|) + |(x2,y1)|) + |(x2,y2)| proof let x1, x2, y1, y2 be real-valued FinSequence; ::_thesis: ( len x1 = len x2 & len x2 = len y1 & len y1 = len y2 implies |((x1 + x2),(y1 + y2))| = ((|(x1,y1)| + |(x1,y2)|) + |(x2,y1)|) + |(x2,y2)| ) assume that A1: len x1 = len x2 and A2: len x2 = len y1 and A3: len y1 = len y2 ; ::_thesis: |((x1 + x2),(y1 + y2))| = ((|(x1,y1)| + |(x1,y2)|) + |(x2,y1)|) + |(x2,y2)| |((x1 + x2),y2)| = |(x1,y2)| + |(x2,y2)| by A1, A2, A3, Th120; then A4: |((x1 + x2),y1)| + |((x1 + x2),y2)| = (|(x1,y1)| + |(x2,y1)|) + (|(x1,y2)| + |(x2,y2)|) by A1, A2, Th120; len (x1 + x2) = len x1 by A1, Th115; hence |((x1 + x2),(y1 + y2))| = ((|(x1,y1)| + |(x1,y2)|) + |(x2,y1)|) + |(x2,y2)| by A1, A2, A3, A4, Th120; ::_thesis: verum end; theorem Th127: :: RVSUM_1:127 for x1, x2, y1, y2 being real-valued FinSequence st len x1 = len x2 & len x2 = len y1 & len y1 = len y2 holds |((x1 - x2),(y1 - y2))| = ((|(x1,y1)| - |(x1,y2)|) - |(x2,y1)|) + |(x2,y2)| proof let x1, x2, y1, y2 be real-valued FinSequence; ::_thesis: ( len x1 = len x2 & len x2 = len y1 & len y1 = len y2 implies |((x1 - x2),(y1 - y2))| = ((|(x1,y1)| - |(x1,y2)|) - |(x2,y1)|) + |(x2,y2)| ) assume that A1: len x1 = len x2 and A2: len x2 = len y1 and A3: len y1 = len y2 ; ::_thesis: |((x1 - x2),(y1 - y2))| = ((|(x1,y1)| - |(x1,y2)|) - |(x2,y1)|) + |(x2,y2)| |(x1,(y1 - y2))| = |(x1,y1)| - |(x1,y2)| by A1, A2, A3, Th124; then A4: |(x1,(y1 - y2))| - |(x2,(y1 - y2))| = (|(x1,y1)| - |(x1,y2)|) - (|(x2,y1)| - |(x2,y2)|) by A2, A3, Th124; len (y1 - y2) = len y1 by A3, Th116; hence |((x1 - x2),(y1 - y2))| = ((|(x1,y1)| - |(x1,y2)|) - |(x2,y1)|) + |(x2,y2)| by A1, A2, A4, Th124; ::_thesis: verum end; theorem :: RVSUM_1:128 for x, y being real-valued FinSequence st len x = len y holds |((x + y),(x + y))| = (|(x,x)| + (2 * |(x,y)|)) + |(y,y)| proof let x, y be real-valued FinSequence; ::_thesis: ( len x = len y implies |((x + y),(x + y))| = (|(x,x)| + (2 * |(x,y)|)) + |(y,y)| ) A1: (|(x,x)| + |(x,y)|) + |(x,y)| = |(x,x)| + (2 * |(x,y)|) ; assume len x = len y ; ::_thesis: |((x + y),(x + y))| = (|(x,x)| + (2 * |(x,y)|)) + |(y,y)| hence |((x + y),(x + y))| = (|(x,x)| + (2 * |(x,y)|)) + |(y,y)| by A1, Th126; ::_thesis: verum end; theorem :: RVSUM_1:129 for x, y being real-valued FinSequence st len x = len y holds |((x - y),(x - y))| = (|(x,x)| - (2 * |(x,y)|)) + |(y,y)| proof let x, y be real-valued FinSequence; ::_thesis: ( len x = len y implies |((x - y),(x - y))| = (|(x,x)| - (2 * |(x,y)|)) + |(y,y)| ) assume len x = len y ; ::_thesis: |((x - y),(x - y))| = (|(x,x)| - (2 * |(x,y)|)) + |(y,y)| then |((x - y),(x - y))| = ((|(x,x)| - |(x,y)|) - |(y,x)|) + |(y,y)| by Th127 .= (|(x,x)| - (2 * |(x,y)|)) + |(y,y)| ; hence |((x - y),(x - y))| = (|(x,x)| - (2 * |(x,y)|)) + |(y,y)| ; ::_thesis: verum end; theorem Th130: :: RVSUM_1:130 for n being Nat for p1, p2, p3 being Element of n -tuples_on REAL holds |((p1 + p2),p3)| = |(p1,p3)| + |(p2,p3)| proof let n be Nat; ::_thesis: for p1, p2, p3 being Element of n -tuples_on REAL holds |((p1 + p2),p3)| = |(p1,p3)| + |(p2,p3)| let p1, p2, p3 be Element of n -tuples_on REAL; ::_thesis: |((p1 + p2),p3)| = |(p1,p3)| + |(p2,p3)| reconsider f1 = p1, f2 = p2, f3 = p3 as real-valued FinSequence ; len f2 = n by CARD_1:def_7; then ( len f1 = len f2 & len f2 = len f3 ) by CARD_1:def_7; hence |((p1 + p2),p3)| = |(p1,p3)| + |(p2,p3)| by Th120; ::_thesis: verum end; theorem Th131: :: RVSUM_1:131 for n being Nat for p1, p2 being Element of n -tuples_on REAL for x being real number holds |((x * p1),p2)| = x * |(p1,p2)| proof let n be Nat; ::_thesis: for p1, p2 being Element of n -tuples_on REAL for x being real number holds |((x * p1),p2)| = x * |(p1,p2)| let p1, p2 be Element of n -tuples_on REAL; ::_thesis: for x being real number holds |((x * p1),p2)| = x * |(p1,p2)| let x be real number ; ::_thesis: |((x * p1),p2)| = x * |(p1,p2)| reconsider f1 = p1, f2 = p2 as real-valued FinSequence ; ( len f1 = n & len f2 = n ) by CARD_1:def_7; hence |((x * p1),p2)| = x * |(p1,p2)| by Th121; ::_thesis: verum end; theorem Th132: :: RVSUM_1:132 for n being Nat for p1, p2 being Element of n -tuples_on REAL holds |((- p1),p2)| = - |(p1,p2)| proof let n be Nat; ::_thesis: for p1, p2 being Element of n -tuples_on REAL holds |((- p1),p2)| = - |(p1,p2)| let p1, p2 be Element of n -tuples_on REAL; ::_thesis: |((- p1),p2)| = - |(p1,p2)| |((- p1),p2)| = |(((- 1) * p1),p2)| .= (- 1) * |(p1,p2)| by Th131 ; hence |((- p1),p2)| = - |(p1,p2)| ; ::_thesis: verum end; theorem :: RVSUM_1:133 for n being Nat for p1, p2 being Element of n -tuples_on REAL holds |((- p1),(- p2))| = |(p1,p2)| proof let n be Nat; ::_thesis: for p1, p2 being Element of n -tuples_on REAL holds |((- p1),(- p2))| = |(p1,p2)| let p1, p2 be Element of n -tuples_on REAL; ::_thesis: |((- p1),(- p2))| = |(p1,p2)| |((- p1),(- p2))| = - |(p1,(- p2))| by Th132 .= - (- |(p1,p2)|) by Th132 ; hence |((- p1),(- p2))| = |(p1,p2)| ; ::_thesis: verum end; theorem Th134: :: RVSUM_1:134 for n being Nat for p1, p2, p3 being Element of n -tuples_on REAL holds |((p1 - p2),p3)| = |(p1,p3)| - |(p2,p3)| proof let n be Nat; ::_thesis: for p1, p2, p3 being Element of n -tuples_on REAL holds |((p1 - p2),p3)| = |(p1,p3)| - |(p2,p3)| let p1, p2, p3 be Element of n -tuples_on REAL; ::_thesis: |((p1 - p2),p3)| = |(p1,p3)| - |(p2,p3)| |((p1 - p2),p3)| = |(p1,p3)| + |((- p2),p3)| by Th130 .= |(p1,p3)| + (- |(p2,p3)|) by Th132 ; hence |((p1 - p2),p3)| = |(p1,p3)| - |(p2,p3)| ; ::_thesis: verum end; theorem :: RVSUM_1:135 for n being Nat for x, y being real number for p1, p2, p3 being Element of n -tuples_on REAL holds |(((x * p1) + (y * p2)),p3)| = (x * |(p1,p3)|) + (y * |(p2,p3)|) proof let n be Nat; ::_thesis: for x, y being real number for p1, p2, p3 being Element of n -tuples_on REAL holds |(((x * p1) + (y * p2)),p3)| = (x * |(p1,p3)|) + (y * |(p2,p3)|) let x, y be real number ; ::_thesis: for p1, p2, p3 being Element of n -tuples_on REAL holds |(((x * p1) + (y * p2)),p3)| = (x * |(p1,p3)|) + (y * |(p2,p3)|) let p1, p2, p3 be Element of n -tuples_on REAL; ::_thesis: |(((x * p1) + (y * p2)),p3)| = (x * |(p1,p3)|) + (y * |(p2,p3)|) |(((x * p1) + (y * p2)),p3)| = |((x * p1),p3)| + |((y * p2),p3)| by Th130 .= (x * |(p1,p3)|) + |((y * p2),p3)| by Th131 .= (x * |(p1,p3)|) + (y * |(p2,p3)|) by Th131 ; hence |(((x * p1) + (y * p2)),p3)| = (x * |(p1,p3)|) + (y * |(p2,p3)|) ; ::_thesis: verum end; theorem Th136: :: RVSUM_1:136 for n being Nat for p1, p2, q1, q2 being Element of n -tuples_on REAL holds |((p1 + p2),(q1 + q2))| = ((|(p1,q1)| + |(p1,q2)|) + |(p2,q1)|) + |(p2,q2)| proof let n be Nat; ::_thesis: for p1, p2, q1, q2 being Element of n -tuples_on REAL holds |((p1 + p2),(q1 + q2))| = ((|(p1,q1)| + |(p1,q2)|) + |(p2,q1)|) + |(p2,q2)| let p1, p2, q1, q2 be Element of n -tuples_on REAL; ::_thesis: |((p1 + p2),(q1 + q2))| = ((|(p1,q1)| + |(p1,q2)|) + |(p2,q1)|) + |(p2,q2)| A1: ( |((p1 + p2),q1)| = |(p1,q1)| + |(p2,q1)| & |((p1 + p2),q2)| = |(p1,q2)| + |(p2,q2)| ) by Th130; |((p1 + p2),(q1 + q2))| = |((p1 + p2),q1)| + |((p1 + p2),q2)| by Th130 .= ((|(p1,q1)| + |(p1,q2)|) + |(p2,q1)|) + |(p2,q2)| by A1 ; hence |((p1 + p2),(q1 + q2))| = ((|(p1,q1)| + |(p1,q2)|) + |(p2,q1)|) + |(p2,q2)| ; ::_thesis: verum end; theorem Th137: :: RVSUM_1:137 for n being Nat for p1, p2, q1, q2 being Element of n -tuples_on REAL holds |((p1 - p2),(q1 - q2))| = ((|(p1,q1)| - |(p1,q2)|) - |(p2,q1)|) + |(p2,q2)| proof let n be Nat; ::_thesis: for p1, p2, q1, q2 being Element of n -tuples_on REAL holds |((p1 - p2),(q1 - q2))| = ((|(p1,q1)| - |(p1,q2)|) - |(p2,q1)|) + |(p2,q2)| let p1, p2, q1, q2 be Element of n -tuples_on REAL; ::_thesis: |((p1 - p2),(q1 - q2))| = ((|(p1,q1)| - |(p1,q2)|) - |(p2,q1)|) + |(p2,q2)| A1: ( |(p1,(q1 - q2))| = |(p1,q1)| - |(p1,q2)| & |(p2,(q1 - q2))| = |(p2,q1)| - |(p2,q2)| ) by Th134; |((p1 - p2),(q1 - q2))| = |(p1,(q1 - q2))| - |(p2,(q1 - q2))| by Th134 .= ((|(p1,q1)| - |(p1,q2)|) - |(p2,q1)|) + |(p2,q2)| by A1 ; hence |((p1 - p2),(q1 - q2))| = ((|(p1,q1)| - |(p1,q2)|) - |(p2,q1)|) + |(p2,q2)| ; ::_thesis: verum end; theorem :: RVSUM_1:138 for n being Nat for p, q being Element of n -tuples_on REAL holds |((p + q),(p + q))| = (|(p,p)| + (2 * |(p,q)|)) + |(q,q)| proof let n be Nat; ::_thesis: for p, q being Element of n -tuples_on REAL holds |((p + q),(p + q))| = (|(p,p)| + (2 * |(p,q)|)) + |(q,q)| let p, q be Element of n -tuples_on REAL; ::_thesis: |((p + q),(p + q))| = (|(p,p)| + (2 * |(p,q)|)) + |(q,q)| (|(p,p)| + |(p,q)|) + |(p,q)| = |(p,p)| + (2 * |(p,q)|) ; hence |((p + q),(p + q))| = (|(p,p)| + (2 * |(p,q)|)) + |(q,q)| by Th136; ::_thesis: verum end; theorem Th139: :: RVSUM_1:139 for n being Nat for p, q being Element of n -tuples_on REAL holds |((p - q),(p - q))| = (|(p,p)| - (2 * |(p,q)|)) + |(q,q)| proof let n be Nat; ::_thesis: for p, q being Element of n -tuples_on REAL holds |((p - q),(p - q))| = (|(p,p)| - (2 * |(p,q)|)) + |(q,q)| let p, q be Element of n -tuples_on REAL; ::_thesis: |((p - q),(p - q))| = (|(p,p)| - (2 * |(p,q)|)) + |(q,q)| |((p - q),(p - q))| = ((|(p,p)| - |(p,q)|) - |(p,q)|) + |(q,q)| by Th137 .= (|(p,p)| - (2 * |(p,q)|)) + |(q,q)| ; hence |((p - q),(p - q))| = (|(p,p)| - (2 * |(p,q)|)) + |(q,q)| ; ::_thesis: verum end; theorem :: RVSUM_1:140 for n being Nat for p, q being Element of n -tuples_on REAL holds |(p,q)| <= |(p,p)| + |(q,q)| proof let n be Nat; ::_thesis: for p, q being Element of n -tuples_on REAL holds |(p,q)| <= |(p,p)| + |(q,q)| let p, q be Element of n -tuples_on REAL; ::_thesis: |(p,q)| <= |(p,p)| + |(q,q)| ( 0 <= |(p,p)| & 0 <= |(q,q)| ) by Th119; then A1: 0 / 2 <= (|(p,p)| + |(q,q)|) / 2 ; |((p - q),(p - q))| = (|(p,p)| - (2 * |(p,q)|)) + |(q,q)| by Th139 .= (|(p,p)| + |(q,q)|) - (2 * |(p,q)|) ; then 2 * |(p,q)| <= (|(p,p)| + |(q,q)|) - 0 by Th119, XREAL_1:11; then (2 * |(p,q)|) / 2 <= (|(p,p)| + |(q,q)|) / 2 by XREAL_1:72; then 0 + |(p,q)| <= ((|(p,p)| + |(q,q)|) / 2) + ((|(p,p)| + |(q,q)|) / 2) by A1, XREAL_1:7; hence |(p,q)| <= |(p,p)| + |(q,q)| ; ::_thesis: verum end; definition let p, q be real-valued FinSequence; predp,q are_orthogonal means :Def17: :: RVSUM_1:def 17 |(p,q)| = 0 ; symmetry for p, q being real-valued FinSequence st |(p,q)| = 0 holds |(q,p)| = 0 ; end; :: deftheorem Def17 defines are_orthogonal RVSUM_1:def_17_:_ for p, q being real-valued FinSequence holds ( p,q are_orthogonal iff |(p,q)| = 0 ); theorem :: RVSUM_1:141 for n being Nat for a being real number for p, q being Element of n -tuples_on REAL st p,q are_orthogonal holds a * p,q are_orthogonal proof let n be Nat; ::_thesis: for a being real number for p, q being Element of n -tuples_on REAL st p,q are_orthogonal holds a * p,q are_orthogonal let a be real number ; ::_thesis: for p, q being Element of n -tuples_on REAL st p,q are_orthogonal holds a * p,q are_orthogonal let p, q be Element of n -tuples_on REAL; ::_thesis: ( p,q are_orthogonal implies a * p,q are_orthogonal ) assume p,q are_orthogonal ; ::_thesis: a * p,q are_orthogonal then |(p,q)| = 0 by Def17; then a * |(p,q)| = 0 ; then |((a * p),q)| = 0 by Th131; hence a * p,q are_orthogonal by Def17; ::_thesis: verum end; theorem :: RVSUM_1:142 for r1, r2, r3, r4 being real number holds Sum <*r1,r2,r3,r4*> = ((r1 + r2) + r3) + r4 proof let r1, r2, r3, r4 be real number ; ::_thesis: Sum <*r1,r2,r3,r4*> = ((r1 + r2) + r3) + r4 thus Sum <*r1,r2,r3,r4*> = (Sum <*r1,r2,r3*>) + r4 by Th74 .= ((r1 + r2) + r3) + r4 by Th78 ; ::_thesis: verum end; theorem Th143: :: RVSUM_1:143 for f being FinSequence of REAL holds ( len f = len (sqr f) & dom f = dom (sqr f) ) proof let f be FinSequence of REAL ; ::_thesis: ( len f = len (sqr f) & dom f = dom (sqr f) ) ( rng f c= REAL & dom sqrreal = REAL ) by FUNCT_2:def_1; hence len f = len (sqrreal * f) by FINSEQ_2:29 .= len (sqr f) ; ::_thesis: dom f = dom (sqr f) hence dom f = dom (sqr f) by FINSEQ_3:29; ::_thesis: verum end; theorem :: RVSUM_1:144 for f, g being FinSequence of REAL holds sqr (f ^ g) = (sqr f) ^ (sqr g) proof let f, g be FinSequence of REAL ; ::_thesis: sqr (f ^ g) = (sqr f) ^ (sqr g) A1: len f = len (sqr f) by Th143; A2: len (sqr (f ^ g)) = len (f ^ g) by Th143; A3: ( len g = len (sqr g) & len (f ^ g) = (len f) + (len g) ) by Th143, FINSEQ_1:22; A4: for i being Nat st 1 <= i & i <= len (sqr (f ^ g)) holds (sqr (f ^ g)) . i = ((sqr f) ^ (sqr g)) . i proof let i be Nat; ::_thesis: ( 1 <= i & i <= len (sqr (f ^ g)) implies (sqr (f ^ g)) . i = ((sqr f) ^ (sqr g)) . i ) assume that A5: 1 <= i and A6: i <= len (sqr (f ^ g)) ; ::_thesis: (sqr (f ^ g)) . i = ((sqr f) ^ (sqr g)) . i A7: i in dom (f ^ g) by A2, A5, A6, FINSEQ_3:25; percases ( i in dom f or not i in dom f ) ; supposeA8: i in dom f ; ::_thesis: (sqr (f ^ g)) . i = ((sqr f) ^ (sqr g)) . i then A9: i in dom (sqr f) by Th143; thus (sqr (f ^ g)) . i = (sqrreal * (f ^ g)) . i .= sqrreal . ((f ^ g) . i) by A7, FUNCT_1:13 .= sqrreal . (f . i) by A8, FINSEQ_1:def_7 .= (f . i) ^2 by Def2 .= (sqr f) . i by VALUED_1:11 .= ((sqr f) ^ (sqr g)) . i by A9, FINSEQ_1:def_7 ; ::_thesis: verum end; suppose not i in dom f ; ::_thesis: (sqr (f ^ g)) . i = ((sqr f) ^ (sqr g)) . i then A10: len f < i by A5, FINSEQ_3:25; then reconsider j = i - (len f) as Element of NAT by INT_1:5; A11: i <= len (f ^ g) by A6, Th143; A12: i <= len ((sqr f) ^ (sqr g)) by A1, A3, A2, A6, FINSEQ_1:22; thus (sqr (f ^ g)) . i = (sqrreal * (f ^ g)) . i .= sqrreal . ((f ^ g) . i) by A7, FUNCT_1:13 .= sqrreal . (g . j) by A10, A11, FINSEQ_1:24 .= (g . j) ^2 by Def2 .= (sqr g) . j by VALUED_1:11 .= ((sqr f) ^ (sqr g)) . i by A1, A10, A12, FINSEQ_1:24 ; ::_thesis: verum end; end; end; len (sqr (f ^ g)) = len ((sqr f) ^ (sqr g)) by A1, A3, A2, FINSEQ_1:22; hence sqr (f ^ g) = (sqr f) ^ (sqr g) by A4, FINSEQ_1:14; ::_thesis: verum end; theorem :: RVSUM_1:145 for F being real-valued FinSequence holds F is FinSequence of REAL proof let F be real-valued FinSequence; ::_thesis: F is FinSequence of REAL thus rng F c= REAL ; :: according to FINSEQ_1:def_4 ::_thesis: verum end;