:: PRGCOR_2 semantic presentation begin definition let D be non empty set ; let p be XFinSequence of ; let q be FinSequence of D; predp is_an_xrep_of q means :Def1: :: PRGCOR_2:def 1 ( NAT c= D & p . 0 = len q & len q < len p & ( for i being Nat st 1 <= i & i <= len q holds p . i = q . i ) ); end; :: deftheorem Def1 defines is_an_xrep_of PRGCOR_2:def_1_:_ for D being non empty set for p being XFinSequence of for q being FinSequence of D holds ( p is_an_xrep_of q iff ( NAT c= D & p . 0 = len q & len q < len p & ( for i being Nat st 1 <= i & i <= len q holds p . i = q . i ) ) ); theorem :: PRGCOR_2:1 for D being non empty set for p being XFinSequence of st NAT c= D & p . 0 is Nat & p . 0 in len p holds p is_an_xrep_of XFS2FS* p proof let D be non empty set ; ::_thesis: for p being XFinSequence of st NAT c= D & p . 0 is Nat & p . 0 in len p holds p is_an_xrep_of XFS2FS* p let p be XFinSequence of ; ::_thesis: ( NAT c= D & p . 0 is Nat & p . 0 in len p implies p is_an_xrep_of XFS2FS* p ) assume that A1: NAT c= D and A2: p . 0 is Nat and A3: p . 0 in len p ; ::_thesis: p is_an_xrep_of XFS2FS* p reconsider m0 = p . 0 as Nat by A2; A4: m0 < len p by A3, NAT_1:44; ( len (XFS2FS* p) = m0 & ( for i being Nat st 1 <= i & i <= m0 holds (XFS2FS* p) . i = p . i ) ) by A3, AFINSQ_1:def_11; hence p is_an_xrep_of XFS2FS* p by A1, A4, Def1; ::_thesis: verum end; definition let x, y, a, b, c be set ; func IFLGT (x,y,a,b,c) -> set equals :Def2: :: PRGCOR_2:def 2 a if x in y b if x = y otherwise c; correctness coherence ( ( x in y implies a is set ) & ( x = y implies b is set ) & ( not x in y & not x = y implies c is set ) ); consistency for b1 being set st x in y & x = y holds ( b1 = a iff b1 = b ); ; end; :: deftheorem Def2 defines IFLGT PRGCOR_2:def_2_:_ for x, y, a, b, c being set holds ( ( x in y implies IFLGT (x,y,a,b,c) = a ) & ( x = y implies IFLGT (x,y,a,b,c) = b ) & ( not x in y & not x = y implies IFLGT (x,y,a,b,c) = c ) ); theorem Th2: :: PRGCOR_2:2 for D being non empty set for q being FinSequence of D for n being Nat st NAT c= D & n > len q holds ex p being XFinSequence of st ( len p = n & p is_an_xrep_of q ) proof let D be non empty set ; ::_thesis: for q being FinSequence of D for n being Nat st NAT c= D & n > len q holds ex p being XFinSequence of st ( len p = n & p is_an_xrep_of q ) let q be FinSequence of D; ::_thesis: for n being Nat st NAT c= D & n > len q holds ex p being XFinSequence of st ( len p = n & p is_an_xrep_of q ) let n be Nat; ::_thesis: ( NAT c= D & n > len q implies ex p being XFinSequence of st ( len p = n & p is_an_xrep_of q ) ) assume that A1: NAT c= D and A2: n > len q ; ::_thesis: ex p being XFinSequence of st ( len p = n & p is_an_xrep_of q ) reconsider n = n as Element of NAT by ORDINAL1:def_12; len q in NAT ; then consider d2 being set such that A3: d2 in D and A4: d2 = len q by A1; reconsider d = d2 as Element of D by A3; deffunc H1( set ) -> set = IFEQ (\$1,0,d,(IFLGT (\$1,(len q),(q . \$1),(q . \$1),d))); ex p being XFinSequence st ( len p = n & ( for k being Nat st k in n holds p . k = H1(k) ) ) from AFINSQ_1:sch_2(); then consider p being XFinSequence such that A5: len p = n and A6: for k being Nat st k in n holds p . k = H1(k) ; rng p c= D proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng p or y in D ) assume y in rng p ; ::_thesis: y in D then consider x being set such that A7: x in dom p and A8: y = p . x by FUNCT_1:def_3; reconsider nx = x as Ordinal by A7; reconsider kx = nx as Element of NAT by A7; A9: p . kx = H1(kx) by A5, A6, A7; now__::_thesis:_(_(_x_=_0_&_p_._x_in_D_)_or_(_x_<>_0_&_p_._x_in_D_)_) percases ( x = 0 or x <> 0 ) ; case x = 0 ; ::_thesis: p . x in D then H1(x) = d by FUNCOP_1:def_8; hence p . x in D by A9; ::_thesis: verum end; caseA10: x <> 0 ; ::_thesis: p . x in D then A11: H1(x) = IFLGT (x,(len q),(q . x),(q . x),d) by FUNCOP_1:def_8; now__::_thesis:_(_(_x_in_len_q_&_p_._x_in_D_)_or_(_x_=_len_q_&_p_._x_in_D_)_or_(_not_x_in_len_q_&_not_x_=_len_q_&_p_._x_in_D_)_) percases ( x in len q or x = len q or ( not x in len q & not x = len q ) ) ; caseA12: x in len q ; ::_thesis: p . x in D then A13: kx < len q by NAT_1:44; 0 + 1 <= kx by A10, NAT_1:13; then kx in Seg (len q) by A13, FINSEQ_1:1; then x in dom q by FINSEQ_1:def_3; then A14: q . x in rng q by FUNCT_1:def_3; A15: rng q c= D by FINSEQ_1:def_4; H1(x) = q . x by A11, A12, Def2; hence p . x in D by A9, A14, A15; ::_thesis: verum end; caseA16: x = len q ; ::_thesis: p . x in D 0 + 1 <= kx by A10, NAT_1:13; then kx in Seg (len q) by A16, FINSEQ_1:1; then x in dom q by FINSEQ_1:def_3; then A17: q . x in rng q by FUNCT_1:def_3; A18: rng q c= D by FINSEQ_1:def_4; H1(x) = q . x by A11, A16, Def2; hence p . x in D by A9, A17, A18; ::_thesis: verum end; case ( not x in len q & not x = len q ) ; ::_thesis: p . x in D then H1(x) = d by A11, Def2; hence p . x in D by A9; ::_thesis: verum end; end; end; hence p . x in D ; ::_thesis: verum end; end; end; hence y in D by A8; ::_thesis: verum end; then reconsider p = p as XFinSequence of by RELAT_1:def_19; reconsider p2 = Replace (p,0,d) as XFinSequence of ; A19: for i being Nat st 1 <= i & i <= len q holds p2 . i = q . i proof let i be Nat; ::_thesis: ( 1 <= i & i <= len q implies p2 . i = q . i ) assume that A20: 1 <= i and A21: i <= len q ; ::_thesis: p2 . i = q . i ( i < len q or i = len q ) by A21, XXREAL_0:1; then A22: ( i in len q or i = len q ) by NAT_1:44; i < n by A2, A21, XXREAL_0:2; then A23: i in n by NAT_1:44; i in NAT by ORDINAL1:def_12; hence p2 . i = p . i by A20, AFINSQ_1:44 .= H1(i) by A6, A23 .= IFLGT (i,(len q),(q . i),(q . i),d) by A20, FUNCOP_1:def_8 .= q . i by A22, Def2 ; ::_thesis: verum end; A24: len p2 = len p by AFINSQ_1:44; p2 . 0 = len q by A2, A4, A5, AFINSQ_1:44; then p2 is_an_xrep_of q by A1, A2, A5, A24, A19, Def1; hence ex p being XFinSequence of st ( len p = n & p is_an_xrep_of q ) by A5, A24; ::_thesis: verum end; definition let a, b be XFinSequence of ; assume that A1: b . 0 is Nat and A2: b . 0 < len a ; func inner_prd_prg (a,b) -> Real means :Def3: :: PRGCOR_2:def 3 ex s being XFinSequence of ex n being Integer st ( len s = len a & s . 0 = 0 & n = b . 0 & ( n <> 0 implies for i being Nat st i < n holds s . (i + 1) = (s . i) + ((a . (i + 1)) * (b . (i + 1))) ) & it = s . n ); existence ex b1 being Real ex s being XFinSequence of ex n being Integer st ( len s = len a & s . 0 = 0 & n = b . 0 & ( n <> 0 implies for i being Nat st i < n holds s . (i + 1) = (s . i) + ((a . (i + 1)) * (b . (i + 1))) ) & b1 = s . n ) proof reconsider q0 = <%0%> as XFinSequence of ; set n2 = len a; reconsider nn2 = b . 0 as Nat by A1; reconsider nn = nn2 as Integer ; defpred S1[ Nat] means ex q being XFinSequence of st ( len q = \$1 + 1 & q . 0 = 0 & ( for k being Nat st k < \$1 & k < nn2 holds q . (k + 1) = (q . k) + ((a . (k + 1)) * (b . (k + 1))) ) ); A3: for k being Nat st k < 0 & k < nn2 holds q0 . (k + 1) = (q0 . k) + ((a . (k + 1)) * (b . (k + 1))) ; A4: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) reconsider k0 = k as Nat ; assume S1[k] ; ::_thesis: S1[k + 1] then consider q2 being XFinSequence of such that A5: len q2 = k + 1 and A6: q2 . 0 = 0 and A7: for k2 being Nat st k2 < k & k2 < nn2 holds q2 . (k2 + 1) = (q2 . k2) + ((a . (k2 + 1)) * (b . (k2 + 1))) ; reconsider qab = (q2 . k0) + ((a . (k0 + 1)) * (b . (k0 + 1))) as Real ; set q3 = q2 ^ <%qab%>; 0 in len q2 by A5, NAT_1:44; then A8: (q2 ^ <%qab%>) . 0 = 0 by A6, AFINSQ_1:def_3; A9: for k2 being Nat st k2 < k + 1 & k2 < nn2 holds (q2 ^ <%qab%>) . (k2 + 1) = ((q2 ^ <%qab%>) . k2) + ((a . (k2 + 1)) * (b . (k2 + 1))) proof let k2 be Nat; ::_thesis: ( k2 < k + 1 & k2 < nn2 implies (q2 ^ <%qab%>) . (k2 + 1) = ((q2 ^ <%qab%>) . k2) + ((a . (k2 + 1)) * (b . (k2 + 1))) ) assume that A10: k2 < k + 1 and A11: k2 < nn2 ; ::_thesis: (q2 ^ <%qab%>) . (k2 + 1) = ((q2 ^ <%qab%>) . k2) + ((a . (k2 + 1)) * (b . (k2 + 1))) A12: k2 <= k by A10, NAT_1:13; now__::_thesis:_(_(_k2_<_k_&_(q2_^_<%qab%>)_._(k2_+_1)_=_((q2_^_<%qab%>)_._k2)_+_((a_._(k2_+_1))_*_(b_._(k2_+_1)))_)_or_(_k2_=_k_&_(q2_^_<%qab%>)_._(k2_+_1)_=_((q2_^_<%qab%>)_._k2)_+_((a_._(k2_+_1))_*_(b_._(k2_+_1)))_)_) percases ( k2 < k or k2 = k ) by A12, XXREAL_0:1; caseA13: k2 < k ; ::_thesis: (q2 ^ <%qab%>) . (k2 + 1) = ((q2 ^ <%qab%>) . k2) + ((a . (k2 + 1)) * (b . (k2 + 1))) then k2 < len q2 by A5, NAT_1:13; then k2 in dom q2 by NAT_1:44; then A14: (q2 ^ <%qab%>) . k2 = q2 . k2 by AFINSQ_1:def_3; k2 + 1 < k + 1 by A13, XREAL_1:6; then k2 + 1 in len q2 by A5, NAT_1:44; then (q2 ^ <%qab%>) . (k2 + 1) = q2 . (k2 + 1) by AFINSQ_1:def_3; hence (q2 ^ <%qab%>) . (k2 + 1) = ((q2 ^ <%qab%>) . k2) + ((a . (k2 + 1)) * (b . (k2 + 1))) by A7, A11, A13, A14; ::_thesis: verum end; caseA15: k2 = k ; ::_thesis: (q2 ^ <%qab%>) . (k2 + 1) = ((q2 ^ <%qab%>) . k2) + ((a . (k2 + 1)) * (b . (k2 + 1))) 0 in 1 by NAT_1:44; then ( <%((q2 . k0) + ((a . (k0 + 1)) * (b . (k0 + 1))))%> . 0 = (q2 . k0) + ((a . (k0 + 1)) * (b . (k0 + 1))) & 0 in dom <%((q2 . k0) + ((a . (k0 + 1)) * (b . (k0 + 1))))%> ) by AFINSQ_1:def_4; then A16: (q2 ^ <%qab%>) . ((k2 + 1) + 0) = (q2 . k0) + ((a . (k0 + 1)) * (b . (k0 + 1))) by A5, A15, AFINSQ_1:def_3; k2 < k2 + 1 by NAT_1:13; then k2 in dom q2 by A5, A15, NAT_1:44; hence (q2 ^ <%qab%>) . (k2 + 1) = ((q2 ^ <%qab%>) . k2) + ((a . (k2 + 1)) * (b . (k2 + 1))) by A15, A16, AFINSQ_1:def_3; ::_thesis: verum end; end; end; hence (q2 ^ <%qab%>) . (k2 + 1) = ((q2 ^ <%qab%>) . k2) + ((a . (k2 + 1)) * (b . (k2 + 1))) ; ::_thesis: verum end; len (q2 ^ <%qab%>) = (len q2) + (len <%((q2 . k0) + ((a . (k0 + 1)) * (b . (k0 + 1))))%>) by AFINSQ_1:17 .= (k + 1) + 1 by A5, AFINSQ_1:33 ; hence S1[k + 1] by A8, A9; ::_thesis: verum end; ( len q0 = 1 & q0 . 0 = 0 ) by AFINSQ_1:def_4; then A17: S1[ 0 ] by A3; for k being Nat holds S1[k] from NAT_1:sch_2(A17, A4); then consider q being XFinSequence of such that A18: ( len q = ((len a) -' 1) + 1 & q . 0 = 0 ) and A19: for k3 being Nat st k3 < (len a) -' 1 & k3 < nn2 holds q . (k3 + 1) = (q . k3) + ((a . (k3 + 1)) * (b . (k3 + 1))) ; reconsider ss2 = q . nn2 as Real ; len a >= 0 + 1 by A1, A2, NAT_1:13; then (len a) - 1 >= 0 by XREAL_1:48; then A20: (len a) -' 1 = (len a) - 1 by XREAL_0:def_2; ( nn <> 0 implies for i being Nat st i < nn holds q . (i + 1) = (q . i) + ((a . (i + 1)) * (b . (i + 1))) ) proof assume nn <> 0 ; ::_thesis: for i being Nat st i < nn holds q . (i + 1) = (q . i) + ((a . (i + 1)) * (b . (i + 1))) thus for i being Nat st i < nn holds q . (i + 1) = (q . i) + ((a . (i + 1)) * (b . (i + 1))) ::_thesis: verum proof let i be Nat; ::_thesis: ( i < nn implies q . (i + 1) = (q . i) + ((a . (i + 1)) * (b . (i + 1))) ) assume A21: i < nn ; ::_thesis: q . (i + 1) = (q . i) + ((a . (i + 1)) * (b . (i + 1))) nn + 1 <= len a by A2, NAT_1:13; then (nn + 1) - 1 <= (len a) - 1 by XREAL_1:9; then i < (len a) -' 1 by A20, A21, XXREAL_0:2; hence q . (i + 1) = (q . i) + ((a . (i + 1)) * (b . (i + 1))) by A19, A21; ::_thesis: verum end; end; then ex s being XFinSequence of ex n being Integer st ( len s = len a & s . 0 = 0 & n = b . 0 & ( n <> 0 implies for i being Nat st i < n holds s . (i + 1) = (s . i) + ((a . (i + 1)) * (b . (i + 1))) ) & ss2 = s . n ) by A18, A20; hence ex b1 being Real ex s being XFinSequence of ex n being Integer st ( len s = len a & s . 0 = 0 & n = b . 0 & ( n <> 0 implies for i being Nat st i < n holds s . (i + 1) = (s . i) + ((a . (i + 1)) * (b . (i + 1))) ) & b1 = s . n ) ; ::_thesis: verum end; uniqueness for b1, b2 being Real st ex s being XFinSequence of ex n being Integer st ( len s = len a & s . 0 = 0 & n = b . 0 & ( n <> 0 implies for i being Nat st i < n holds s . (i + 1) = (s . i) + ((a . (i + 1)) * (b . (i + 1))) ) & b1 = s . n ) & ex s being XFinSequence of ex n being Integer st ( len s = len a & s . 0 = 0 & n = b . 0 & ( n <> 0 implies for i being Nat st i < n holds s . (i + 1) = (s . i) + ((a . (i + 1)) * (b . (i + 1))) ) & b2 = s . n ) holds b1 = b2 proof thus for w1, w2 being Real st ex s being XFinSequence of ex n1 being Integer st ( len s = len a & s . 0 = 0 & n1 = b . 0 & ( n1 <> 0 implies for i being Nat st i < n1 holds s . (i + 1) = (s . i) + ((a . (i + 1)) * (b . (i + 1))) ) & w1 = s . n1 ) & ex s being XFinSequence of ex n2 being Integer st ( len s = len a & s . 0 = 0 & n2 = b . 0 & ( n2 <> 0 implies for i being Nat st i < n2 holds s . (i + 1) = (s . i) + ((a . (i + 1)) * (b . (i + 1))) ) & w2 = s . n2 ) holds w1 = w2 ::_thesis: verum proof let w1, w2 be Real; ::_thesis: ( ex s being XFinSequence of ex n1 being Integer st ( len s = len a & s . 0 = 0 & n1 = b . 0 & ( n1 <> 0 implies for i being Nat st i < n1 holds s . (i + 1) = (s . i) + ((a . (i + 1)) * (b . (i + 1))) ) & w1 = s . n1 ) & ex s being XFinSequence of ex n2 being Integer st ( len s = len a & s . 0 = 0 & n2 = b . 0 & ( n2 <> 0 implies for i being Nat st i < n2 holds s . (i + 1) = (s . i) + ((a . (i + 1)) * (b . (i + 1))) ) & w2 = s . n2 ) implies w1 = w2 ) assume that A22: ex s being XFinSequence of ex n1 being Integer st ( len s = len a & s . 0 = 0 & n1 = b . 0 & ( n1 <> 0 implies for i being Nat st i < n1 holds s . (i + 1) = (s . i) + ((a . (i + 1)) * (b . (i + 1))) ) & w1 = s . n1 ) and A23: ex s being XFinSequence of ex n2 being Integer st ( len s = len a & s . 0 = 0 & n2 = b . 0 & ( n2 <> 0 implies for i being Nat st i < n2 holds s . (i + 1) = (s . i) + ((a . (i + 1)) * (b . (i + 1))) ) & w2 = s . n2 ) ; ::_thesis: w1 = w2 consider s1 being XFinSequence of , n1 being Integer such that len s1 = len a and A24: s1 . 0 = 0 and A25: n1 = b . 0 and A26: ( n1 <> 0 implies for i being Nat st i < n1 holds s1 . (i + 1) = (s1 . i) + ((a . (i + 1)) * (b . (i + 1))) ) and A27: w1 = s1 . n1 by A22; consider s2 being XFinSequence of , n2 being Integer such that len s2 = len a and A28: s2 . 0 = 0 and A29: n2 = b . 0 and A30: ( n2 <> 0 implies for i being Nat st i < n2 holds s2 . (i + 1) = (s2 . i) + ((a . (i + 1)) * (b . (i + 1))) ) and A31: w2 = s2 . n2 by A23; reconsider n = n1 as Nat by A1, A25; defpred S1[ Nat] means ( \$1 <= n implies s1 . \$1 = s2 . \$1 ); A32: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A33: S1[k] ; ::_thesis: S1[k + 1] now__::_thesis:_(_k_+_1_<=_n_implies_s1_._(k_+_1)_=_s2_._(k_+_1)_) assume k + 1 <= n ; ::_thesis: s1 . (k + 1) = s2 . (k + 1) then A34: k < n by NAT_1:13; then s1 . (k + 1) = (s1 . k) + ((a . (k + 1)) * (b . (k + 1))) by A26; hence s1 . (k + 1) = s2 . (k + 1) by A25, A29, A30, A33, A34; ::_thesis: verum end; hence S1[k + 1] ; ::_thesis: verum end; A35: S1[ 0 ] by A24, A28; for k being Nat holds S1[k] from NAT_1:sch_2(A35, A32); hence w1 = w2 by A25, A27, A29, A31; ::_thesis: verum end; end; end; :: deftheorem Def3 defines inner_prd_prg PRGCOR_2:def_3_:_ for a, b being XFinSequence of st b . 0 is Nat & b . 0 < len a holds for b3 being Real holds ( b3 = inner_prd_prg (a,b) iff ex s being XFinSequence of ex n being Integer st ( len s = len a & s . 0 = 0 & n = b . 0 & ( n <> 0 implies for i being Nat st i < n holds s . (i + 1) = (s . i) + ((a . (i + 1)) * (b . (i + 1))) ) & b3 = s . n ) ); theorem Th3: :: PRGCOR_2:3 for a being FinSequence of REAL for s being XFinSequence of st s . 0 = 0 & ( for i being Nat st i < len a holds s . (i + 1) = (s . i) + (a . (i + 1)) ) holds Sum a = s . (len a) proof let a be FinSequence of REAL ; ::_thesis: for s being XFinSequence of st s . 0 = 0 & ( for i being Nat st i < len a holds s . (i + 1) = (s . i) + (a . (i + 1)) ) holds Sum a = s . (len a) let s be XFinSequence of ; ::_thesis: ( s . 0 = 0 & ( for i being Nat st i < len a holds s . (i + 1) = (s . i) + (a . (i + 1)) ) implies Sum a = s . (len a) ) assume that A1: s . 0 = 0 and A2: for i being Nat st i < len a holds s . (i + 1) = (s . i) + (a . (i + 1)) ; ::_thesis: Sum a = s . (len a) defpred S1[ Nat] means ( \$1 <= len a implies Sum (a | \$1) = s . \$1 ); A3: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) reconsider k1 = k as Element of NAT by ORDINAL1:def_12; reconsider m = k1 + 1 as Nat ; assume A4: S1[k] ; ::_thesis: S1[k + 1] ( k + 1 <= len a implies Sum (a | m) = s . (k + 1) ) proof reconsider x0 = <*(a /. m)*> as FinSequence of REAL ; reconsider rx = a /. m as Element of REAL ; reconsider q0 = a | k as FinSequence of REAL ; assume A5: k + 1 <= len a ; ::_thesis: Sum (a | m) = s . (k + 1) then A6: a | m = (a | k) ^ <*(a /. m)*> by FINSEQ_5:82; A7: 1 <= k + 1 by NAT_1:11; then m in Seg (len a) by A5, FINSEQ_1:1; then A8: m in dom a by FINSEQ_1:def_3; m in Seg m by A7, FINSEQ_1:1; then m in Seg (len (a | m)) by A5, FINSEQ_1:59; then A9: m in dom (a | m) by FINSEQ_1:def_3; Sum x0 = rx by RVSUM_1:73; then A10: Sum (a | m) = (s . k) + rx by A4, A5, A6, NAT_1:13, RVSUM_1:75; A11: len (a | m) = m by A5, FINSEQ_1:59; A12: k < len a by A5, NAT_1:13; len (a | m) = (len q0) + (len <*rx*>) by A6, FINSEQ_1:22 .= (len q0) + 1 by FINSEQ_1:40 ; then rx = (a | m) . m by A6, A11, FINSEQ_1:42 .= (a | m) /. m by A9, PARTFUN1:def_6 .= a /. m by A9, FINSEQ_4:70 .= a . m by A8, PARTFUN1:def_6 ; hence Sum (a | m) = s . (k + 1) by A2, A12, A10; ::_thesis: verum end; hence S1[k + 1] ; ::_thesis: verum end; A13: S1[ 0 ] by A1, RVSUM_1:72; for k being Nat holds S1[k] from NAT_1:sch_2(A13, A3); then S1[ len a] ; hence Sum a = s . (len a) by FINSEQ_1:58; ::_thesis: verum end; theorem :: PRGCOR_2:4 for a being FinSequence of REAL ex s being XFinSequence of st ( len s = (len a) + 1 & s . 0 = 0 & ( for i being Nat st i < len a holds s . (i + 1) = (s . i) + (a . (i + 1)) ) & Sum a = s . (len a) ) proof let a be FinSequence of REAL ; ::_thesis: ex s being XFinSequence of st ( len s = (len a) + 1 & s . 0 = 0 & ( for i being Nat st i < len a holds s . (i + 1) = (s . i) + (a . (i + 1)) ) & Sum a = s . (len a) ) deffunc H1( Nat) -> Element of REAL = Sum (a | \$1); ex p being XFinSequence st ( len p = (len a) + 1 & ( for k being Nat st k in (len a) + 1 holds p . k = H1(k) ) ) from AFINSQ_1:sch_2(); then consider p being XFinSequence such that A1: len p = (len a) + 1 and A2: for k being Nat st k in (len a) + 1 holds p . k = H1(k) ; rng p c= REAL proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng p or y in REAL ) assume y in rng p ; ::_thesis: y in REAL then consider x being set such that A3: x in dom p and A4: y = p . x by FUNCT_1:def_3; reconsider nx = x as Element of NAT by A3; p . nx = Sum (a | nx) by A1, A2, A3; hence y in REAL by A4; ::_thesis: verum end; then reconsider p = p as XFinSequence of by RELAT_1:def_19; A5: for i being Nat st i < len a holds p . (i + 1) = (p . i) + (a . (i + 1)) proof let i be Nat; ::_thesis: ( i < len a implies p . (i + 1) = (p . i) + (a . (i + 1)) ) assume A6: i < len a ; ::_thesis: p . (i + 1) = (p . i) + (a . (i + 1)) reconsider i = i as Element of NAT by ORDINAL1:def_12; reconsider ii = i + 1 as Nat ; A7: i + 1 <= len a by A6, NAT_1:13; 1 <= 1 + i by NAT_1:11; then i + 1 in Seg (len a) by A7, FINSEQ_1:1; then A8: i + 1 in dom a by FINSEQ_1:def_3; i < (len a) + 1 by A6, NAT_1:13; then i in (len a) + 1 by NAT_1:44; then A9: p . i = Sum (a | i) by A2; i + 1 < (len a) + 1 by A6, XREAL_1:6; then A10: i + 1 in (len a) + 1 by NAT_1:44; a | ii = (a | i) ^ <*(a /. ii)*> by A7, FINSEQ_5:82; then Sum (a | ii) = (Sum (a | i)) + (Sum <*(a /. ii)*>) by RVSUM_1:75 .= (p . i) + (a /. ii) by A9, RVSUM_1:73 .= (p . i) + (a . ii) by A8, PARTFUN1:def_6 ; hence p . (i + 1) = (p . i) + (a . (i + 1)) by A2, A10; ::_thesis: verum end; 0 in (len a) + 1 by NAT_1:44; then A11: p . 0 = H1( 0 ) by A2 .= 0 by RVSUM_1:72 ; then Sum a = p . (len a) by A5, Th3; hence ex s being XFinSequence of st ( len s = (len a) + 1 & s . 0 = 0 & ( for i being Nat st i < len a holds s . (i + 1) = (s . i) + (a . (i + 1)) ) & Sum a = s . (len a) ) by A1, A11, A5; ::_thesis: verum end; theorem :: PRGCOR_2:5 for a, b being FinSequence of REAL for n being Nat st len a = len b & n > len a holds |(a,b)| = inner_prd_prg ((FS2XFS* (a,n)),(FS2XFS* (b,n))) proof let a, b be FinSequence of REAL ; ::_thesis: for n being Nat st len a = len b & n > len a holds |(a,b)| = inner_prd_prg ((FS2XFS* (a,n)),(FS2XFS* (b,n))) let n2 be Nat; ::_thesis: ( len a = len b & n2 > len a implies |(a,b)| = inner_prd_prg ((FS2XFS* (a,n2)),(FS2XFS* (b,n2))) ) assume that A1: len a = len b and A2: n2 > len a ; ::_thesis: |(a,b)| = inner_prd_prg ((FS2XFS* (a,n2)),(FS2XFS* (b,n2))) reconsider rb = b as Element of (len a) -tuples_on REAL by A1, FINSEQ_2:92; reconsider ra = a as Element of (len a) -tuples_on REAL by FINSEQ_2:92; set ri = inner_prd_prg ((FS2XFS* (a,n2)),(FS2XFS* (b,n2))); set pa = FS2XFS* (a,n2); set pb = FS2XFS* (b,n2); A3: len b = (FS2XFS* (b,n2)) . 0 by A1, A2, AFINSQ_1:def_10; len (FS2XFS* (a,n2)) = n2 by A2, AFINSQ_1:def_10; then consider s being XFinSequence of , n being Integer such that len s = len (FS2XFS* (a,n2)) and A4: s . 0 = 0 and A5: n = (FS2XFS* (b,n2)) . 0 and A6: ( n <> 0 implies for i being Nat st i < n holds s . (i + 1) = (s . i) + (((FS2XFS* (a,n2)) . (i + 1)) * ((FS2XFS* (b,n2)) . (i + 1))) ) and A7: inner_prd_prg ((FS2XFS* (a,n2)),(FS2XFS* (b,n2))) = s . n by A1, A2, A3, Def3; A8: len (mlt (ra,rb)) = len a by CARD_1:def_7; for i being Nat st i < len (mlt (a,b)) holds s . (i + 1) = (s . i) + ((mlt (a,b)) . (i + 1)) proof let i be Nat; ::_thesis: ( i < len (mlt (a,b)) implies s . (i + 1) = (s . i) + ((mlt (a,b)) . (i + 1)) ) assume A9: i < len (mlt (a,b)) ; ::_thesis: s . (i + 1) = (s . i) + ((mlt (a,b)) . (i + 1)) then ( 1 <= i + 1 & i + 1 <= len a ) by A8, NAT_1:11, NAT_1:13; then A10: ( (FS2XFS* (a,n2)) . (i + 1) = a . (i + 1) & (FS2XFS* (b,n2)) . (i + 1) = b . (i + 1) ) by A1, A2, AFINSQ_1:def_10; A11: i < n by A1, A2, A5, A8, A9, AFINSQ_1:def_10; now__::_thesis:_(_(_n_<>_0_&_s_._(i_+_1)_=_(s_._i)_+_((mlt_(a,b))_._(i_+_1))_)_or_(_n_=_0_&_contradiction_)_) percases ( n <> 0 or n = 0 ) ; case n <> 0 ; ::_thesis: s . (i + 1) = (s . i) + ((mlt (a,b)) . (i + 1)) s . (i + 1) = (s . i) + (((FS2XFS* (a,n2)) . (i + 1)) * ((FS2XFS* (b,n2)) . (i + 1))) by A6, A11 .= (s . i) + ((mlt (a,b)) . (i + 1)) by A10, RVSUM_1:59 ; hence s . (i + 1) = (s . i) + ((mlt (a,b)) . (i + 1)) ; ::_thesis: verum end; case n = 0 ; ::_thesis: contradiction hence contradiction by A1, A2, A5, A8, A9, AFINSQ_1:def_10; ::_thesis: verum end; end; end; hence s . (i + 1) = (s . i) + ((mlt (a,b)) . (i + 1)) ; ::_thesis: verum end; then Sum (mlt (a,b)) = s . n by A1, A3, A4, A5, A8, Th3; hence |(a,b)| = inner_prd_prg ((FS2XFS* (a,n2)),(FS2XFS* (b,n2))) by A7, RVSUM_1:def_16; ::_thesis: verum end; definition let b, c be XFinSequence of ; let a be Real; let m be Integer; predm scalar_prd_prg c,a,b means :Def4: :: PRGCOR_2:def 4 ( len c = m & len b = m & ex n being Integer st ( c . 0 = b . 0 & n = b . 0 & ( n <> 0 implies for i being Nat st 1 <= i & i <= n holds c . i = a * (b . i) ) ) ); end; :: deftheorem Def4 defines scalar_prd_prg PRGCOR_2:def_4_:_ for b, c being XFinSequence of for a being Real for m being Integer holds ( m scalar_prd_prg c,a,b iff ( len c = m & len b = m & ex n being Integer st ( c . 0 = b . 0 & n = b . 0 & ( n <> 0 implies for i being Nat st 1 <= i & i <= n holds c . i = a * (b . i) ) ) ) ); theorem :: PRGCOR_2:6 for b being non empty XFinSequence of for a being Real for m being Nat st b . 0 is Nat & len b = m & b . 0 < m holds ( ex c being XFinSequence of st m scalar_prd_prg c,a,b & ( for c being non empty XFinSequence of st m scalar_prd_prg c,a,b holds XFS2FS* c = a * (XFS2FS* b) ) ) proof let b be non empty XFinSequence of ; ::_thesis: for a being Real for m being Nat st b . 0 is Nat & len b = m & b . 0 < m holds ( ex c being XFinSequence of st m scalar_prd_prg c,a,b & ( for c being non empty XFinSequence of st m scalar_prd_prg c,a,b holds XFS2FS* c = a * (XFS2FS* b) ) ) let a be Real; ::_thesis: for m being Nat st b . 0 is Nat & len b = m & b . 0 < m holds ( ex c being XFinSequence of st m scalar_prd_prg c,a,b & ( for c being non empty XFinSequence of st m scalar_prd_prg c,a,b holds XFS2FS* c = a * (XFS2FS* b) ) ) let m be Nat; ::_thesis: ( b . 0 is Nat & len b = m & b . 0 < m implies ( ex c being XFinSequence of st m scalar_prd_prg c,a,b & ( for c being non empty XFinSequence of st m scalar_prd_prg c,a,b holds XFS2FS* c = a * (XFS2FS* b) ) ) ) assume that A1: b . 0 is Nat and A2: len b = m and A3: b . 0 < m ; ::_thesis: ( ex c being XFinSequence of st m scalar_prd_prg c,a,b & ( for c being non empty XFinSequence of st m scalar_prd_prg c,a,b holds XFS2FS* c = a * (XFS2FS* b) ) ) reconsider k = b . 0 as Nat by A1; reconsider c2 = a * (XFS2FS* b) as FinSequence of REAL ; dom (a * (XFS2FS* b)) = dom (XFS2FS* b) by VALUED_1:def_5; then A4: Seg (len (a * (XFS2FS* b))) = dom (XFS2FS* b) by FINSEQ_1:def_3; A5: b . 0 in m by A1, A3, NAT_1:44; then len (XFS2FS* b) = b . 0 by A2, AFINSQ_1:def_11; then A6: len c2 = k by A4, FINSEQ_1:def_3; then consider p being XFinSequence of such that A7: len p = m and A8: p is_an_xrep_of c2 by A3, Th2; reconsider p2 = Replace (p,0,(b . 0)) as XFinSequence of ; A9: now__::_thesis:_(_k_<>_0_implies_for_i_being_Nat_st_1_<=_i_&_i_<=_k_holds_ p2_._i_=_a_*_(b_._i)_) assume k <> 0 ; ::_thesis: for i being Nat st 1 <= i & i <= k holds p2 . i = a * (b . i) thus for i being Nat st 1 <= i & i <= k holds p2 . i = a * (b . i) ::_thesis: verum proof let i be Nat; ::_thesis: ( 1 <= i & i <= k implies p2 . i = a * (b . i) ) assume that A10: 1 <= i and A11: i <= k ; ::_thesis: p2 . i = a * (b . i) (XFS2FS* b) . i = b . i by A2, A5, A10, A11, AFINSQ_1:def_11; then A12: (a * (XFS2FS* b)) . i = a * (b . i) by RVSUM_1:44; ( i in NAT & p . i = c2 . i ) by A6, A8, A10, A11, Def1, ORDINAL1:def_12; hence p2 . i = a * (b . i) by A10, A12, AFINSQ_1:44; ::_thesis: verum end; end; ( len p = len p2 & p2 . 0 = b . 0 ) by A1, A3, A7, AFINSQ_1:44; then m scalar_prd_prg p2,a,b by A2, A7, A9, Def4; hence ex c being XFinSequence of st m scalar_prd_prg c,a,b ; ::_thesis: for c being non empty XFinSequence of st m scalar_prd_prg c,a,b holds XFS2FS* c = a * (XFS2FS* b) A13: 0 < len b ; thus for c being non empty XFinSequence of st m scalar_prd_prg c,a,b holds XFS2FS* c = a * (XFS2FS* b) ::_thesis: verum proof let c be non empty XFinSequence of ; ::_thesis: ( m scalar_prd_prg c,a,b implies XFS2FS* c = a * (XFS2FS* b) ) assume A14: m scalar_prd_prg c,a,b ; ::_thesis: XFS2FS* c = a * (XFS2FS* b) then consider n being Integer such that A15: c . 0 = b . 0 and A16: n = b . 0 and A17: ( n <> 0 implies for i being Nat st 1 <= i & i <= n holds c . i = a * (b . i) ) by Def4; A18: ( len c = m & ex n being Integer st ( c . 0 = b . 0 & n = b . 0 & ( n <> 0 implies for i being Nat st 1 <= i & i <= n holds c . i = a * (b . i) ) ) ) by A14, Def4; then A19: len (XFS2FS* c) = c . 0 by A5, AFINSQ_1:def_11; now__::_thesis:_(_(_n_=_0_&_XFS2FS*_c_=_a_*_(XFS2FS*_b)_)_or_(_n_<>_0_&_XFS2FS*_c_=_a_*_(XFS2FS*_b)_)_) percases ( n = 0 or n <> 0 ) ; case n = 0 ; ::_thesis: XFS2FS* c = a * (XFS2FS* b) then ( XFS2FS* b = <*> REAL & XFS2FS* c = <*> REAL ) by A13, A18, A16, AFINSQ_1:64; hence XFS2FS* c = a * (XFS2FS* b) by RVSUM_1:46; ::_thesis: verum end; case n <> 0 ; ::_thesis: XFS2FS* c = a * (XFS2FS* b) set p3 = XFS2FS* c; for k3 being Nat st 1 <= k3 & k3 <= len (XFS2FS* c) holds (XFS2FS* c) . k3 = c2 . k3 proof let k3 be Nat; ::_thesis: ( 1 <= k3 & k3 <= len (XFS2FS* c) implies (XFS2FS* c) . k3 = c2 . k3 ) assume that A20: 1 <= k3 and A21: k3 <= len (XFS2FS* c) ; ::_thesis: (XFS2FS* c) . k3 = c2 . k3 A22: c . 0 in len c by A1, A3, A18, NAT_1:44; then A23: k3 <= n by A15, A16, A21, AFINSQ_1:def_11; then A24: b . k3 = (XFS2FS* b) . k3 by A2, A5, A16, A20, AFINSQ_1:def_11; len (XFS2FS* c) = n by A15, A16, A22, AFINSQ_1:def_11; then (XFS2FS* c) . k3 = c . k3 by A15, A16, A20, A21, A22, AFINSQ_1:def_11 .= a * (b . k3) by A17, A20, A23 ; hence (XFS2FS* c) . k3 = c2 . k3 by A24, RVSUM_1:44; ::_thesis: verum end; hence XFS2FS* c = a * (XFS2FS* b) by A6, A15, A19, FINSEQ_1:14; ::_thesis: verum end; end; end; hence XFS2FS* c = a * (XFS2FS* b) ; ::_thesis: verum end; end; definition let b, c be XFinSequence of ; let m be Integer; predm vector_minus_prg c,b means :Def5: :: PRGCOR_2:def 5 ( len c = m & len b = m & ex n being Integer st ( c . 0 = b . 0 & n = b . 0 & ( n <> 0 implies for i being Nat st 1 <= i & i <= n holds c . i = - (b . i) ) ) ); end; :: deftheorem Def5 defines vector_minus_prg PRGCOR_2:def_5_:_ for b, c being XFinSequence of for m being Integer holds ( m vector_minus_prg c,b iff ( len c = m & len b = m & ex n being Integer st ( c . 0 = b . 0 & n = b . 0 & ( n <> 0 implies for i being Nat st 1 <= i & i <= n holds c . i = - (b . i) ) ) ) ); theorem :: PRGCOR_2:7 for b being non empty XFinSequence of for m being Nat st b . 0 is Nat & len b = m & b . 0 < m holds ( ex c being XFinSequence of st m vector_minus_prg c,b & ( for c being non empty XFinSequence of st m vector_minus_prg c,b holds XFS2FS* c = - (XFS2FS* b) ) ) proof let b be non empty XFinSequence of ; ::_thesis: for m being Nat st b . 0 is Nat & len b = m & b . 0 < m holds ( ex c being XFinSequence of st m vector_minus_prg c,b & ( for c being non empty XFinSequence of st m vector_minus_prg c,b holds XFS2FS* c = - (XFS2FS* b) ) ) let m be Nat; ::_thesis: ( b . 0 is Nat & len b = m & b . 0 < m implies ( ex c being XFinSequence of st m vector_minus_prg c,b & ( for c being non empty XFinSequence of st m vector_minus_prg c,b holds XFS2FS* c = - (XFS2FS* b) ) ) ) assume that A1: b . 0 is Nat and A2: len b = m and A3: b . 0 < m ; ::_thesis: ( ex c being XFinSequence of st m vector_minus_prg c,b & ( for c being non empty XFinSequence of st m vector_minus_prg c,b holds XFS2FS* c = - (XFS2FS* b) ) ) reconsider k = b . 0 as Nat by A1; reconsider c2 = - (XFS2FS* b) as FinSequence of REAL ; dom (- (XFS2FS* b)) = dom (XFS2FS* b) by VALUED_1:8; then A4: Seg (len (- (XFS2FS* b))) = dom (XFS2FS* b) by FINSEQ_1:def_3; A5: b . 0 in m by A1, A3, NAT_1:44; then len (XFS2FS* b) = b . 0 by A2, AFINSQ_1:def_11; then A6: len c2 = k by A4, FINSEQ_1:def_3; then consider p being XFinSequence of such that A7: len p = m and A8: p is_an_xrep_of c2 by A3, Th2; reconsider p2 = Replace (p,0,(b . 0)) as XFinSequence of ; A9: ( k <> 0 implies for i being Nat st 1 <= i & i <= k holds p2 . i = - (b . i) ) proof assume k <> 0 ; ::_thesis: for i being Nat st 1 <= i & i <= k holds p2 . i = - (b . i) let i be Nat; ::_thesis: ( 1 <= i & i <= k implies p2 . i = - (b . i) ) assume that A10: 1 <= i and A11: i <= k ; ::_thesis: p2 . i = - (b . i) (XFS2FS* b) . i = b . i by A2, A5, A10, A11, AFINSQ_1:def_11; then A12: (- (XFS2FS* b)) . i = - (b . i) by RVSUM_1:17; ( i in NAT & p . i = c2 . i ) by A6, A8, A10, A11, Def1, ORDINAL1:def_12; hence p2 . i = - (b . i) by A10, A12, AFINSQ_1:44; ::_thesis: verum end; ( len p = len p2 & p2 . 0 = b . 0 ) by A1, A3, A7, AFINSQ_1:44; then m vector_minus_prg p2,b by A2, A7, A9, Def5; hence ex c being XFinSequence of st m vector_minus_prg c,b ; ::_thesis: for c being non empty XFinSequence of st m vector_minus_prg c,b holds XFS2FS* c = - (XFS2FS* b) A13: 0 < len b ; thus for c being non empty XFinSequence of st m vector_minus_prg c,b holds XFS2FS* c = - (XFS2FS* b) ::_thesis: verum proof let c be non empty XFinSequence of ; ::_thesis: ( m vector_minus_prg c,b implies XFS2FS* c = - (XFS2FS* b) ) assume A14: m vector_minus_prg c,b ; ::_thesis: XFS2FS* c = - (XFS2FS* b) then consider n being Integer such that A15: c . 0 = b . 0 and A16: n = b . 0 and A17: ( n <> 0 implies for i being Nat st 1 <= i & i <= n holds c . i = - (b . i) ) by Def5; A18: ( len c = m & ex n being Integer st ( c . 0 = b . 0 & n = b . 0 & ( n <> 0 implies for i being Nat st 1 <= i & i <= n holds c . i = - (b . i) ) ) ) by A14, Def5; then A19: len (XFS2FS* c) = c . 0 by A5, AFINSQ_1:def_11; now__::_thesis:_(_(_n_=_0_&_XFS2FS*_c_=_-_(XFS2FS*_b)_)_or_(_n_<>_0_&_XFS2FS*_c_=_-_(XFS2FS*_b)_)_) percases ( n = 0 or n <> 0 ) ; caseA20: n = 0 ; ::_thesis: XFS2FS* c = - (XFS2FS* b) then XFS2FS* b = <*> REAL by A13, A16, AFINSQ_1:64; hence XFS2FS* c = - (XFS2FS* b) by A18, A16, A20, AFINSQ_1:64, RVSUM_1:19; ::_thesis: verum end; case n <> 0 ; ::_thesis: XFS2FS* c = - (XFS2FS* b) set p3 = XFS2FS* c; for k3 being Nat st 1 <= k3 & k3 <= len (XFS2FS* c) holds (XFS2FS* c) . k3 = c2 . k3 proof let k3 be Nat; ::_thesis: ( 1 <= k3 & k3 <= len (XFS2FS* c) implies (XFS2FS* c) . k3 = c2 . k3 ) A21: c . 0 in len c by A1, A3, A18, NAT_1:44; then A22: len (XFS2FS* c) = n by A15, A16, AFINSQ_1:def_11; assume A23: ( 1 <= k3 & k3 <= len (XFS2FS* c) ) ; ::_thesis: (XFS2FS* c) . k3 = c2 . k3 then A24: b . k3 = (XFS2FS* b) . k3 by A2, A5, A16, A22, AFINSQ_1:def_11; (XFS2FS* c) . k3 = c . k3 by A15, A16, A23, A21, A22, AFINSQ_1:def_11 .= - (b . k3) by A17, A23, A22 ; hence (XFS2FS* c) . k3 = c2 . k3 by A24, RVSUM_1:17; ::_thesis: verum end; hence XFS2FS* c = - (XFS2FS* b) by A6, A15, A19, FINSEQ_1:14; ::_thesis: verum end; end; end; hence XFS2FS* c = - (XFS2FS* b) ; ::_thesis: verum end; end; definition let a, b, c be XFinSequence of ; let m be Integer; predm vector_add_prg c,a,b means :Def6: :: PRGCOR_2:def 6 ( len c = m & len a = m & len b = m & ex n being Integer st ( c . 0 = b . 0 & n = b . 0 & ( n <> 0 implies for i being Nat st 1 <= i & i <= n holds c . i = (a . i) + (b . i) ) ) ); end; :: deftheorem Def6 defines vector_add_prg PRGCOR_2:def_6_:_ for a, b, c being XFinSequence of for m being Integer holds ( m vector_add_prg c,a,b iff ( len c = m & len a = m & len b = m & ex n being Integer st ( c . 0 = b . 0 & n = b . 0 & ( n <> 0 implies for i being Nat st 1 <= i & i <= n holds c . i = (a . i) + (b . i) ) ) ) ); theorem :: PRGCOR_2:8 for a, b being non empty XFinSequence of for m being Nat st b . 0 is Nat & len a = m & len b = m & a . 0 = b . 0 & b . 0 < m holds ( ex c being XFinSequence of st m vector_add_prg c,a,b & ( for c being non empty XFinSequence of st m vector_add_prg c,a,b holds XFS2FS* c = (XFS2FS* a) + (XFS2FS* b) ) ) proof let a, b be non empty XFinSequence of ; ::_thesis: for m being Nat st b . 0 is Nat & len a = m & len b = m & a . 0 = b . 0 & b . 0 < m holds ( ex c being XFinSequence of st m vector_add_prg c,a,b & ( for c being non empty XFinSequence of st m vector_add_prg c,a,b holds XFS2FS* c = (XFS2FS* a) + (XFS2FS* b) ) ) let m be Nat; ::_thesis: ( b . 0 is Nat & len a = m & len b = m & a . 0 = b . 0 & b . 0 < m implies ( ex c being XFinSequence of st m vector_add_prg c,a,b & ( for c being non empty XFinSequence of st m vector_add_prg c,a,b holds XFS2FS* c = (XFS2FS* a) + (XFS2FS* b) ) ) ) assume that A1: b . 0 is Nat and A2: len a = m and A3: len b = m and A4: a . 0 = b . 0 and A5: b . 0 < m ; ::_thesis: ( ex c being XFinSequence of st m vector_add_prg c,a,b & ( for c being non empty XFinSequence of st m vector_add_prg c,a,b holds XFS2FS* c = (XFS2FS* a) + (XFS2FS* b) ) ) reconsider k = b . 0 as Nat by A1; reconsider Fb = XFS2FS* b as FinSequence of REAL ; reconsider Fa = XFS2FS* a as FinSequence of REAL ; reconsider c2 = Fa + Fb as FinSequence of REAL ; A6: b . 0 in m by A1, A5, NAT_1:44; then A7: len (XFS2FS* a) = b . 0 by A2, A4, AFINSQ_1:def_11; A8: len (XFS2FS* b) = b . 0 by A3, A6, AFINSQ_1:def_11; then A9: len c2 = len (XFS2FS* a) by A7, RVSUM_1:115; then dom c2 = Seg (len (XFS2FS* b)) by A8, A7, FINSEQ_1:def_3; then dom ((XFS2FS* a) + (XFS2FS* b)) = dom (XFS2FS* b) by FINSEQ_1:def_3; then Seg (len c2) = dom (XFS2FS* b) by FINSEQ_1:def_3; then A10: len c2 = k by A8, FINSEQ_1:def_3; then consider p being XFinSequence of such that A11: len p = m and A12: p is_an_xrep_of c2 by A5, Th2; reconsider p2 = Replace (p,0,(b . 0)) as XFinSequence of ; A13: now__::_thesis:_(_k_<>_0_implies_for_i_being_Nat_st_1_<=_i_&_i_<=_k_holds_ p2_._i_=_(a_._i)_+_(b_._i)_) assume k <> 0 ; ::_thesis: for i being Nat st 1 <= i & i <= k holds p2 . i = (a . i) + (b . i) thus for i being Nat st 1 <= i & i <= k holds p2 . i = (a . i) + (b . i) ::_thesis: verum proof let i be Nat; ::_thesis: ( 1 <= i & i <= k implies p2 . i = (a . i) + (b . i) ) assume that A14: 1 <= i and A15: i <= k ; ::_thesis: p2 . i = (a . i) + (b . i) i in Seg (len c2) by A7, A9, A14, A15, FINSEQ_1:1; then A16: i in dom c2 by FINSEQ_1:def_3; ( (XFS2FS* a) . i = a . i & (XFS2FS* b) . i = b . i ) by A2, A3, A4, A6, A14, A15, AFINSQ_1:def_11; then A17: ((XFS2FS* a) + (XFS2FS* b)) . i = (a . i) + (b . i) by A16, VALUED_1:def_1; ( i in NAT & p . i = c2 . i ) by A10, A12, A14, A15, Def1, ORDINAL1:def_12; hence p2 . i = (a . i) + (b . i) by A14, A17, AFINSQ_1:44; ::_thesis: verum end; end; ( len p = len p2 & p2 . 0 = b . 0 ) by A1, A5, A11, AFINSQ_1:44; then m vector_add_prg p2,a,b by A2, A3, A11, A13, Def6; hence ex c being XFinSequence of st m vector_add_prg c,a,b ; ::_thesis: for c being non empty XFinSequence of st m vector_add_prg c,a,b holds XFS2FS* c = (XFS2FS* a) + (XFS2FS* b) A18: 0 < len b ; thus for c being non empty XFinSequence of st m vector_add_prg c,a,b holds XFS2FS* c = (XFS2FS* a) + (XFS2FS* b) ::_thesis: verum proof let c be non empty XFinSequence of ; ::_thesis: ( m vector_add_prg c,a,b implies XFS2FS* c = (XFS2FS* a) + (XFS2FS* b) ) assume A19: m vector_add_prg c,a,b ; ::_thesis: XFS2FS* c = (XFS2FS* a) + (XFS2FS* b) then consider n being Integer such that A20: c . 0 = b . 0 and A21: n = b . 0 and A22: ( n <> 0 implies for i being Nat st 1 <= i & i <= n holds c . i = (a . i) + (b . i) ) by Def6; A23: ( len c = m & ex n being Integer st ( c . 0 = b . 0 & n = b . 0 & ( n <> 0 implies for i being Nat st 1 <= i & i <= n holds c . i = (a . i) + (b . i) ) ) ) by A19, Def6; then A24: len (XFS2FS* c) = c . 0 by A6, AFINSQ_1:def_11; now__::_thesis:_(_(_n_=_0_&_XFS2FS*_c_=_(XFS2FS*_a)_+_(XFS2FS*_b)_)_or_(_n_<>_0_&_XFS2FS*_c_=_(XFS2FS*_a)_+_(XFS2FS*_b)_)_) percases ( n = 0 or n <> 0 ) ; case n = 0 ; ::_thesis: XFS2FS* c = (XFS2FS* a) + (XFS2FS* b) then ( XFS2FS* b = <*> REAL & XFS2FS* c = <*> REAL ) by A18, A23, A21, AFINSQ_1:64; hence XFS2FS* c = (XFS2FS* a) + (XFS2FS* b) by RVSUM_1:12; ::_thesis: verum end; case n <> 0 ; ::_thesis: XFS2FS* c = (XFS2FS* a) + (XFS2FS* b) set p3 = XFS2FS* c; for k3 being Nat st 1 <= k3 & k3 <= len (XFS2FS* c) holds (XFS2FS* c) . k3 = c2 . k3 proof let k3 be Nat; ::_thesis: ( 1 <= k3 & k3 <= len (XFS2FS* c) implies (XFS2FS* c) . k3 = c2 . k3 ) assume that A25: 1 <= k3 and A26: k3 <= len (XFS2FS* c) ; ::_thesis: (XFS2FS* c) . k3 = c2 . k3 A27: c . 0 in len c by A1, A5, A23, NAT_1:44; then A28: k3 <= n by A20, A21, A26, AFINSQ_1:def_11; then A29: ( a . k3 = (XFS2FS* a) . k3 & b . k3 = (XFS2FS* b) . k3 ) by A2, A3, A4, A6, A21, A25, AFINSQ_1:def_11; k3 in Seg (len c2) by A10, A21, A25, A28, FINSEQ_1:1; then A30: k3 in dom c2 by FINSEQ_1:def_3; len (XFS2FS* c) = n by A20, A21, A27, AFINSQ_1:def_11; then (XFS2FS* c) . k3 = c . k3 by A20, A21, A25, A26, A27, AFINSQ_1:def_11 .= (a . k3) + (b . k3) by A22, A25, A28 ; hence (XFS2FS* c) . k3 = c2 . k3 by A30, A29, VALUED_1:def_1; ::_thesis: verum end; hence XFS2FS* c = (XFS2FS* a) + (XFS2FS* b) by A10, A20, A24, FINSEQ_1:14; ::_thesis: verum end; end; end; hence XFS2FS* c = (XFS2FS* a) + (XFS2FS* b) ; ::_thesis: verum end; end; definition let a, b, c be XFinSequence of ; let m be Integer; predm vector_sub_prg c,a,b means :Def7: :: PRGCOR_2:def 7 ( len c = m & len a = m & len b = m & ex n being Integer st ( c . 0 = b . 0 & n = b . 0 & ( n <> 0 implies for i being Nat st 1 <= i & i <= n holds c . i = (a . i) - (b . i) ) ) ); end; :: deftheorem Def7 defines vector_sub_prg PRGCOR_2:def_7_:_ for a, b, c being XFinSequence of for m being Integer holds ( m vector_sub_prg c,a,b iff ( len c = m & len a = m & len b = m & ex n being Integer st ( c . 0 = b . 0 & n = b . 0 & ( n <> 0 implies for i being Nat st 1 <= i & i <= n holds c . i = (a . i) - (b . i) ) ) ) ); theorem :: PRGCOR_2:9 for a, b being non empty XFinSequence of for m being Nat st b . 0 is Nat & len a = m & len b = m & a . 0 = b . 0 & b . 0 < m holds ( ex c being XFinSequence of st m vector_sub_prg c,a,b & ( for c being non empty XFinSequence of st m vector_sub_prg c,a,b holds XFS2FS* c = (XFS2FS* a) - (XFS2FS* b) ) ) proof let a, b be non empty XFinSequence of ; ::_thesis: for m being Nat st b . 0 is Nat & len a = m & len b = m & a . 0 = b . 0 & b . 0 < m holds ( ex c being XFinSequence of st m vector_sub_prg c,a,b & ( for c being non empty XFinSequence of st m vector_sub_prg c,a,b holds XFS2FS* c = (XFS2FS* a) - (XFS2FS* b) ) ) let m be Nat; ::_thesis: ( b . 0 is Nat & len a = m & len b = m & a . 0 = b . 0 & b . 0 < m implies ( ex c being XFinSequence of st m vector_sub_prg c,a,b & ( for c being non empty XFinSequence of st m vector_sub_prg c,a,b holds XFS2FS* c = (XFS2FS* a) - (XFS2FS* b) ) ) ) assume that A1: b . 0 is Nat and A2: len a = m and A3: len b = m and A4: a . 0 = b . 0 and A5: b . 0 < m ; ::_thesis: ( ex c being XFinSequence of st m vector_sub_prg c,a,b & ( for c being non empty XFinSequence of st m vector_sub_prg c,a,b holds XFS2FS* c = (XFS2FS* a) - (XFS2FS* b) ) ) reconsider k = b . 0 as Nat by A1; reconsider Fb = XFS2FS* b as FinSequence of REAL ; reconsider Fa = XFS2FS* a as FinSequence of REAL ; reconsider c2 = Fa - Fb as FinSequence of REAL ; A6: b . 0 in m by A1, A5, NAT_1:44; then A7: len (XFS2FS* a) = b . 0 by A2, A4, AFINSQ_1:def_11; A8: len (XFS2FS* b) = b . 0 by A3, A6, AFINSQ_1:def_11; then A9: len c2 = len (XFS2FS* a) by A7, RVSUM_1:116; then dom c2 = Seg (len (XFS2FS* b)) by A8, A7, FINSEQ_1:def_3; then dom ((XFS2FS* a) - (XFS2FS* b)) = dom (XFS2FS* b) by FINSEQ_1:def_3; then Seg (len c2) = dom (XFS2FS* b) by FINSEQ_1:def_3; then A10: len c2 = k by A8, FINSEQ_1:def_3; then consider p being XFinSequence of such that A11: len p = m and A12: p is_an_xrep_of c2 by A5, Th2; reconsider p2 = Replace (p,0,(b . 0)) as XFinSequence of ; A13: now__::_thesis:_(_k_<>_0_implies_for_i_being_Nat_st_1_<=_i_&_i_<=_k_holds_ p2_._i_=_(a_._i)_-_(b_._i)_) assume k <> 0 ; ::_thesis: for i being Nat st 1 <= i & i <= k holds p2 . i = (a . i) - (b . i) thus for i being Nat st 1 <= i & i <= k holds p2 . i = (a . i) - (b . i) ::_thesis: verum proof let i be Nat; ::_thesis: ( 1 <= i & i <= k implies p2 . i = (a . i) - (b . i) ) assume that A14: 1 <= i and A15: i <= k ; ::_thesis: p2 . i = (a . i) - (b . i) i in Seg (len c2) by A7, A9, A14, A15, FINSEQ_1:1; then A16: i in dom c2 by FINSEQ_1:def_3; ( (XFS2FS* a) . i = a . i & (XFS2FS* b) . i = b . i ) by A2, A3, A4, A6, A14, A15, AFINSQ_1:def_11; then A17: ((XFS2FS* a) - (XFS2FS* b)) . i = (a . i) - (b . i) by A16, VALUED_1:13; ( i in NAT & p . i = c2 . i ) by A10, A12, A14, A15, Def1, ORDINAL1:def_12; hence p2 . i = (a . i) - (b . i) by A14, A17, AFINSQ_1:44; ::_thesis: verum end; end; ( len p = len p2 & p2 . 0 = b . 0 ) by A1, A5, A11, AFINSQ_1:44; then m vector_sub_prg p2,a,b by A2, A3, A11, A13, Def7; hence ex c being XFinSequence of st m vector_sub_prg c,a,b ; ::_thesis: for c being non empty XFinSequence of st m vector_sub_prg c,a,b holds XFS2FS* c = (XFS2FS* a) - (XFS2FS* b) A18: 0 < len b ; thus for c being non empty XFinSequence of st m vector_sub_prg c,a,b holds XFS2FS* c = (XFS2FS* a) - (XFS2FS* b) ::_thesis: verum proof let c be non empty XFinSequence of ; ::_thesis: ( m vector_sub_prg c,a,b implies XFS2FS* c = (XFS2FS* a) - (XFS2FS* b) ) assume A19: m vector_sub_prg c,a,b ; ::_thesis: XFS2FS* c = (XFS2FS* a) - (XFS2FS* b) then consider n being Integer such that A20: c . 0 = b . 0 and A21: n = b . 0 and A22: ( n <> 0 implies for i being Nat st 1 <= i & i <= n holds c . i = (a . i) - (b . i) ) by Def7; A23: ( len c = m & ex n being Integer st ( c . 0 = b . 0 & n = b . 0 & ( n <> 0 implies for i being Nat st 1 <= i & i <= n holds c . i = (a . i) - (b . i) ) ) ) by A19, Def7; then A24: len (XFS2FS* c) = c . 0 by A6, AFINSQ_1:def_11; now__::_thesis:_(_(_n_=_0_&_XFS2FS*_c_=_(XFS2FS*_a)_-_(XFS2FS*_b)_)_or_(_n_<>_0_&_XFS2FS*_c_=_(XFS2FS*_a)_-_(XFS2FS*_b)_)_) percases ( n = 0 or n <> 0 ) ; case n = 0 ; ::_thesis: XFS2FS* c = (XFS2FS* a) - (XFS2FS* b) then ( XFS2FS* b = <*> REAL & XFS2FS* c = <*> REAL ) by A18, A23, A21, AFINSQ_1:64; hence XFS2FS* c = (XFS2FS* a) - (XFS2FS* b) by RVSUM_1:28; ::_thesis: verum end; case n <> 0 ; ::_thesis: XFS2FS* c = (XFS2FS* a) - (XFS2FS* b) set p3 = XFS2FS* c; for k3 being Nat st 1 <= k3 & k3 <= len (XFS2FS* c) holds (XFS2FS* c) . k3 = c2 . k3 proof let k3 be Nat; ::_thesis: ( 1 <= k3 & k3 <= len (XFS2FS* c) implies (XFS2FS* c) . k3 = c2 . k3 ) assume that A25: 1 <= k3 and A26: k3 <= len (XFS2FS* c) ; ::_thesis: (XFS2FS* c) . k3 = c2 . k3 A27: c . 0 in len c by A1, A5, A23, NAT_1:44; then A28: k3 <= n by A20, A21, A26, AFINSQ_1:def_11; then A29: ( a . k3 = (XFS2FS* a) . k3 & b . k3 = (XFS2FS* b) . k3 ) by A2, A3, A4, A6, A21, A25, AFINSQ_1:def_11; k3 in Seg (len c2) by A10, A21, A25, A28, FINSEQ_1:1; then A30: k3 in dom c2 by FINSEQ_1:def_3; A31: len (XFS2FS* c) = n by A20, A21, A27, AFINSQ_1:def_11; then (XFS2FS* c) . k3 = c . k3 by A20, A21, A25, A26, A27, AFINSQ_1:def_11 .= (a . k3) - (b . k3) by A22, A25, A26, A31 ; hence (XFS2FS* c) . k3 = c2 . k3 by A30, A29, VALUED_1:13; ::_thesis: verum end; hence XFS2FS* c = (XFS2FS* a) - (XFS2FS* b) by A10, A20, A24, FINSEQ_1:14; ::_thesis: verum end; end; end; hence XFS2FS* c = (XFS2FS* a) - (XFS2FS* b) ; ::_thesis: verum end; end;