prgcor_2.miz



    begin

    reserve k,i for Nat;

    reserve D for non empty set;

    definition

      let D;

      let p be XFinSequence of D, q be FinSequence of D;

      :: PRGCOR_2:def1

      pred p is_an_xrep_of q means NAT c= D & (p . 0 ) = ( len q) & ( len q) < ( len p) & for i st 1 <= i & i <= ( len q) holds (p . i) = (q . i);

    end

    theorem :: PRGCOR_2:1

    for p be XFinSequence of D st NAT c= D & (p . 0 ) is Nat & (p . 0 ) in ( dom p) holds p is_an_xrep_of ( XFS2FS* p)

    proof

      let p be XFinSequence of D;

      assume that

       A1: NAT c= D and

       A2: (p . 0 ) is Nat and

       A3: (p . 0 ) in ( dom p);

      reconsider m0 = (p . 0 ) as Nat by A2;

      

       A4: m0 < ( len p) by A3, AFINSQ_1: 86;

      (p . 0 ) in ( len p) by A3;

      then ( len ( XFS2FS* p)) = m0 & for i st 1 <= i & i <= m0 holds (( XFS2FS* p) . i) = (p . i) by AFINSQ_1:def 11;

      hence thesis by A1, A4;

    end;

    definition

      let x be object, y be set, a,b,c be object;

      :: PRGCOR_2:def2

      func IFLGT (x,y,a,b,c) -> object equals

      : Def2: a if x in y,

b if x = y

      otherwise c;

      correctness

      proof

        reconsider xx = x as set by TARSKI: 1;

         not xx in xx;

        hence thesis;

      end;

    end

    theorem :: PRGCOR_2:2

    

     Th2: for q be FinSequence of D, n be Nat st NAT c= D & n > ( len q) holds ex p be XFinSequence of D st ( len p) = n & p is_an_xrep_of q

    proof

      let q be FinSequence of D, n be Nat;

      assume that

       A1: NAT c= D and

       A2: n > ( len q);

      reconsider n as Element of NAT by ORDINAL1:def 12;

      consider d2 be set such that

       A3: d2 in D and

       A4: d2 = ( len q) by A1;

      reconsider d = d2 as Element of D by A3;

      deffunc F( object) = ( IFEQ ($1, 0 ,d,( IFLGT ($1,( len q),(q . $1),(q . $1),d))));

      ex p be XFinSequence st ( len p) = n & for k be Nat st k in n holds (p . k) = F(k) from AFINSQ_1:sch 2;

      then

      consider p be XFinSequence such that

       A5: ( len p) = n and

       A6: for k be Nat st k in n holds (p . k) = F(k);

      ( rng p) c= D

      proof

        let y be object;

        assume y in ( rng p);

        then

        consider x be object 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) = F(kx) by A5, A6, A7;

        now

          per cases ;

            case x = 0 ;

            then F(x) = d by FUNCOP_1:def 8;

            hence (p . x) in D by A9;

          end;

            case

             A10: x <> 0 ;

            then

             A11: F(x) = ( IFLGT (x,( len q),(q . x),(q . x),d)) by FUNCOP_1:def 8;

            now

              per cases ;

                case

                 A12: x in ( Segm ( len q));

                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;

                 F(x) = (q . x) by A11, A12, Def2;

                hence (p . x) in D by A9, A14, A15;

              end;

                case

                 A16: x = ( len q);

                ( 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;

                 F(x) = (q . x) by A11, A16, Def2;

                hence (p . x) in D by A9, A17, A18;

              end;

                case not (x in ( len q) or x = ( len q));

                then F(x) = d by A11, Def2;

                hence (p . x) in D by A9;

              end;

            end;

            hence (p . x) in D;

          end;

        end;

        hence thesis by A8;

      end;

      then

      reconsider p as XFinSequence of D by RELAT_1:def 19;

      reconsider p2 = ( Replace (p, 0 ,d)) as XFinSequence of D;

      

       A19: for i st 1 <= i & i <= ( len q) holds (p2 . i) = (q . i)

      proof

        let i;

        assume that

         A20: 1 <= i and

         A21: i <= ( len q);

        i < ( len q) or i = ( len q) by A21, XXREAL_0: 1;

        then

         A22: i in ( Segm ( len q)) or i = ( len q) by NAT_1: 44;

        i < n by A2, A21, XXREAL_0: 2;

        then

         A23: i in ( Segm n) by NAT_1: 44;

        i in NAT by ORDINAL1:def 12;

        

        hence (p2 . i) = (p . i) by A20, AFINSQ_1: 44

        .= F(i) by A6, A23

        .= ( IFLGT (i,( len q),(q . i),(q . i),d)) by A20, FUNCOP_1:def 8

        .= (q . i) by A22, Def2;

      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;

      hence thesis by A5, A24;

    end;

    definition

      let a,b be XFinSequence of REAL ;

      assume that

       A1: (b . 0 ) is Nat and

       A2: (b . 0 ) < ( len a);

      :: PRGCOR_2:def3

      func inner_prd_prg (a,b) -> Real means

      : Def3: ex s be XFinSequence of REAL , n be Integer st ( len s) = ( len a) & (s . 0 ) = 0 & n = (b . 0 ) & (n <> 0 implies for i be Nat st i < n holds (s . (i + 1)) = ((s . i) + ((a . (i + 1)) * (b . (i + 1))))) & it = (s . n);

      existence

      proof

        reconsider q0 = <%( In ( 0 , REAL ))%> as XFinSequence of REAL ;

        set n2 = ( len a);

        reconsider nn2 = (b . 0 ) as Nat by A1;

        reconsider nn = nn2 as Integer;

        defpred P[ Nat] means ex q be XFinSequence of REAL st (( len q) = ($1 + 1) & (q . 0 ) = 0 & (for k st k < $1 & k < nn2 holds (q . (k + 1)) = ((q . k) + ((a . (k + 1)) * (b . (k + 1))))));

        

         A3: for k st k < 0 & k < nn2 holds (q0 . (k + 1)) = ((q0 . k) + ((a . (k + 1)) * (b . (k + 1))));

        

         A4: for k be Nat st P[k] holds P[(k + 1)]

        proof

          let k be Nat;

          reconsider k0 = k as Nat;

          assume P[k];

          then

          consider q2 be XFinSequence of REAL such that

           A5: ( len q2) = (k + 1) and

           A6: (q2 . 0 ) = 0 and

           A7: for k2 be 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 Element of REAL by XREAL_0:def 1;

          set q3 = (q2 ^ <%qab%>);

           0 in ( len q2) by A5, AFINSQ_1: 86;

          then

           A8: (q3 . 0 ) = 0 by A6, AFINSQ_1:def 3;

          

           A9: for k2 be Nat st k2 < (k + 1) & k2 < nn2 holds (q3 . (k2 + 1)) = ((q3 . k2) + ((a . (k2 + 1)) * (b . (k2 + 1))))

          proof

            let k2 be Nat;

            assume that

             A10: k2 < (k + 1) and

             A11: k2 < nn2;

            

             A12: k2 <= k by A10, NAT_1: 13;

            now

              per cases by A12, XXREAL_0: 1;

                case

                 A13: k2 < k;

                then k2 < ( len q2) by A5, NAT_1: 13;

                then k2 in ( dom q2) by AFINSQ_1: 86;

                then

                 A14: (q3 . 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, AFINSQ_1: 86;

                then (q3 . (k2 + 1)) = (q2 . (k2 + 1)) by AFINSQ_1:def 3;

                hence thesis by A7, A11, A13, A14;

              end;

                case

                 A15: k2 = k;

                 0 in ( Segm 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: (q3 . ((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, AFINSQ_1: 86;

                hence thesis by A15, A16, AFINSQ_1:def 3;

              end;

            end;

            hence thesis;

          end;

          ( len q3) = (( len q2) + ( len <%((q2 . k0) + ((a . (k0 + 1)) * (b . (k0 + 1))))%>)) by AFINSQ_1: 17

          .= ((k + 1) + 1) by A5, AFINSQ_1: 33;

          hence thesis by A8, A9;

        end;

        ( len q0) = 1 & (q0 . 0 ) = ( In ( 0 , REAL )) by AFINSQ_1:def 4;

        then

         A17: P[ 0 ] by A3;

        for k be Nat holds P[k] from NAT_1:sch 2( A17, A4);

        then

        consider q be XFinSequence of REAL such that

         A18: ( len q) = ((n2 -' 1) + 1) & (q . 0 ) = 0 and

         A19: for k3 be Nat st k3 < (n2 -' 1) & k3 < nn2 holds (q . (k3 + 1)) = ((q . k3) + ((a . (k3 + 1)) * (b . (k3 + 1))));

        reconsider ss2 = (q . nn2) as Real;

        n2 >= ( 0 + 1) by A1, A2, NAT_1: 13;

        then (n2 - 1) >= 0 by XREAL_1: 48;

        then

         A20: (n2 -' 1) = (n2 - 1) by XREAL_0:def 2;

        nn <> 0 implies for i be Nat st i < nn holds (q . (i + 1)) = ((q . i) + ((a . (i + 1)) * (b . (i + 1))))

        proof

          assume nn <> 0 ;

          thus for i be Nat st i < nn holds (q . (i + 1)) = ((q . i) + ((a . (i + 1)) * (b . (i + 1))))

          proof

            let i be Nat;

            assume

             A21: i < nn;

            (nn + 1) <= n2 by A2, NAT_1: 13;

            then ((nn + 1) - 1) <= (n2 - 1) by XREAL_1: 9;

            then i < (n2 -' 1) by A20, A21, XXREAL_0: 2;

            hence thesis by A19, A21;

          end;

        end;

        then ex s be XFinSequence of REAL , n be Integer st ( len s) = ( len a) & (s . 0 ) = 0 & n = (b . 0 ) & (n <> 0 implies for i be Nat st i < n holds (s . (i + 1)) = ((s . i) + ((a . (i + 1)) * (b . (i + 1))))) & ss2 = (s . n) by A18, A20;

        hence thesis;

      end;

      uniqueness

      proof

        thus for w1,w2 be Real st (ex s be XFinSequence of REAL , n1 be Integer st ( len s) = ( len a) & (s . 0 ) = 0 & n1 = (b . 0 ) & (n1 <> 0 implies for i be Nat st i < n1 holds (s . (i + 1)) = ((s . i) + ((a . (i + 1)) * (b . (i + 1))))) & w1 = (s . n1)) & (ex s be XFinSequence of REAL , n2 be Integer st ( len s) = ( len a) & (s . 0 ) = 0 & n2 = (b . 0 ) & (n2 <> 0 implies for i be Nat st i < n2 holds (s . (i + 1)) = ((s . i) + ((a . (i + 1)) * (b . (i + 1))))) & w2 = (s . n2)) holds w1 = w2

        proof

          let w1,w2 be Real;

          assume that

           A22: ex s be XFinSequence of REAL , n1 be Integer st ( len s) = ( len a) & (s . 0 ) = 0 & n1 = (b . 0 ) & (n1 <> 0 implies for i be Nat st i < n1 holds (s . (i + 1)) = ((s . i) + ((a . (i + 1)) * (b . (i + 1))))) & w1 = (s . n1) and

           A23: ex s be XFinSequence of REAL , n2 be Integer st ( len s) = ( len a) & (s . 0 ) = 0 & n2 = (b . 0 ) & (n2 <> 0 implies for i be Nat st i < n2 holds (s . (i + 1)) = ((s . i) + ((a . (i + 1)) * (b . (i + 1))))) & w2 = (s . n2);

          consider s1 be XFinSequence of REAL , n1 be Integer such that ( len s1) = ( len a) and

           A24: (s1 . 0 ) = 0 and

           A25: n1 = (b . 0 ) and

           A26: n1 <> 0 implies for i be 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 be XFinSequence of REAL , n2 be Integer such that ( len s2) = ( len a) and

           A28: (s2 . 0 ) = 0 and

           A29: n2 = (b . 0 ) and

           A30: n2 <> 0 implies for i be 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 P2[ Nat] means $1 <= n implies (s1 . $1) = (s2 . $1);

          

           A32: for k be Nat st P2[k] holds P2[(k + 1)]

          proof

            let k be Nat;

            assume

             A33: P2[k];

            now

              assume (k + 1) <= n;

              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;

            end;

            hence thesis;

          end;

          

           A35: P2[ 0 ] by A24, A28;

          for k be Nat holds P2[k] from NAT_1:sch 2( A35, A32);

          hence thesis by A25, A27, A29, A31;

        end;

      end;

    end

    theorem :: PRGCOR_2:3

    

     Th3: for a be FinSequence of REAL , s be XFinSequence of REAL st (s . 0 ) = 0 & (for i 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 , s be XFinSequence of REAL ;

      assume that

       A1: (s . 0 ) = 0 and

       A2: for i st i < ( len a) holds (s . (i + 1)) = ((s . i) + (a . (i + 1)));

      defpred P[ Nat] means $1 <= ( len a) implies ( Sum (a | $1)) = (s . $1);

      

       A3: for k st P[k] holds P[(k + 1)]

      proof

        let k;

        reconsider k1 = k as Element of NAT by ORDINAL1:def 12;

        reconsider m = (k1 + 1) as Nat;

        assume

         A4: P[k];

        (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);

          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 thesis by A2, A12, A10;

        end;

        hence thesis;

      end;

      

       A13: P[ 0 ] by A1, RVSUM_1: 72;

      for k holds P[k] from NAT_1:sch 2( A13, A3);

      then P[( len a)];

      hence thesis by FINSEQ_1: 58;

    end;

    theorem :: PRGCOR_2:4

    for a be FinSequence of REAL holds ex s be XFinSequence of REAL st ( len s) = (( len a) + 1) & (s . 0 ) = 0 & (for i 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 ;

      deffunc F( Nat) = ( Sum (a | $1));

      ex p be XFinSequence st ( len p) = (( len a) + 1) & for k be Nat st k in (( len a) + 1) holds (p . k) = F(k) from AFINSQ_1:sch 2;

      then

      consider p be XFinSequence such that

       A1: ( len p) = (( len a) + 1) and

       A2: for k be Nat st k in (( len a) + 1) holds (p . k) = F(k);

      ( rng p) c= REAL

      proof

        let y be object;

        assume y in ( rng p);

        then

        consider x be object 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 thesis by A4, XREAL_0:def 1;

      end;

      then

      reconsider p as XFinSequence of REAL by RELAT_1:def 19;

      

       A5: for i st i < ( len a) holds (p . (i + 1)) = ((p . i) + (a . (i + 1)))

      proof

        let i;

        assume

         A6: i < ( len a);

        reconsider 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 ( Segm (( 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 ( Segm (( 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 thesis by A2, A10;

      end;

       0 in ( Segm (( len a) + 1)) by NAT_1: 44;

      

      then

       A11: (p . 0 ) = F(0) by A2

      .= 0 by RVSUM_1: 72;

      then ( Sum a) = (p . ( len a)) by A5, Th3;

      hence thesis by A1, A11, A5;

    end;

    theorem :: PRGCOR_2:5

    for a,b be FinSequence of REAL , n be 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 , n2 be Nat;

      assume that

       A1: ( len a) = ( len b) and

       A2: n2 > ( len a);

      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) = (pb . 0 ) by A1, A2, AFINSQ_1:def 10, NUMBERS: 19;

      ( len pa) = n2 by A2, AFINSQ_1:def 10, NUMBERS: 19;

      then

      consider s be XFinSequence of REAL , n be Integer such that ( len s) = ( len pa) and

       A4: (s . 0 ) = 0 and

       A5: n = (pb . 0 ) and

       A6: n <> 0 implies for i be Nat st i < n holds (s . (i + 1)) = ((s . i) + ((pa . (i + 1)) * (pb . (i + 1)))) and

       A7: ri = (s . n) by A1, A2, A3, Def3;

      

       A8: ( len ( mlt (ra,rb))) = ( len a) by CARD_1:def 7;

      for i st i < ( len ( mlt (a,b))) holds (s . (i + 1)) = ((s . i) + (( mlt (a,b)) . (i + 1)))

      proof

        let i;

        assume

         A9: i < ( len ( mlt (a,b)));

        then 1 <= (i + 1) & (i + 1) <= ( len a) by A8, NAT_1: 11, NAT_1: 13;

        then

         A10: (pa . (i + 1)) = (a . (i + 1)) & (pb . (i + 1)) = (b . (i + 1)) by A1, A2, AFINSQ_1:def 10, NUMBERS: 19;

        

         A11: i < n by A1, A2, A5, A8, A9, AFINSQ_1:def 10, NUMBERS: 19;

        now

          per cases ;

            case n <> 0 ;

            (s . (i + 1)) = ((s . i) + ((pa . (i + 1)) * (pb . (i + 1)))) by A6, A11

            .= ((s . i) + (( mlt (a,b)) . (i + 1))) by A10, RVSUM_1: 59;

            hence thesis;

          end;

            case n = 0 ;

            hence contradiction by A1, A2, A5, A8, A9, AFINSQ_1:def 10, NUMBERS: 19;

          end;

        end;

        hence thesis;

      end;

      then ( Sum ( mlt (a,b))) = (s . n) by A1, A3, A4, A5, A8, Th3;

      hence thesis by A7, RVSUM_1:def 16;

    end;

    definition

      let b,c be XFinSequence of REAL , a be Real, m be Integer;

      :: PRGCOR_2:def4

      pred m scalar_prd_prg c,a,b means ( len c) = m & ( len b) = m & ex n be Integer st (c . 0 ) = (b . 0 ) & n = (b . 0 ) & (n <> 0 implies for i be Nat st 1 <= i & i <= n holds (c . i) = (a * (b . i)));

    end

    theorem :: PRGCOR_2:6

    for b be non empty XFinSequence of REAL , a be Real, m be Nat st (b . 0 ) is Nat & ( len b) = m & (b . 0 ) < m holds (ex c be XFinSequence of REAL st m scalar_prd_prg (c,a,b)) & for c be non empty XFinSequence of REAL st m scalar_prd_prg (c,a,b) holds ( XFS2FS* c) = (a * ( XFS2FS* b))

    proof

      let b be non empty XFinSequence of REAL , a be Real, m be Nat;

      assume that

       A1: (b . 0 ) is Nat and

       A2: ( len b) = m and

       A3: (b . 0 ) < m;

      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 ( Segm 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 be XFinSequence of REAL such that

       A7: ( len p) = m and

       A8: p is_an_xrep_of c2 by A3, Th2, NUMBERS: 19;

      reconsider b0 = (b . 0 ) as Element of REAL by XREAL_0:def 1;

      reconsider p2 = ( Replace (p, 0 ,b0)) as XFinSequence of REAL ;

       A9:

      now

        assume k <> 0 ;

        thus for i be Nat st 1 <= i & i <= k holds (p2 . i) = (a * (b . i))

        proof

          let i be Nat;

          assume that

           A10: 1 <= i and

           A11: i <= k;

          (( 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, ORDINAL1:def 12;

          hence thesis by A10, A12, AFINSQ_1: 44;

        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;

      hence ex c be XFinSequence of REAL st m scalar_prd_prg (c,a,b);

      

       A13: 0 < ( len b);

      thus for c be non empty XFinSequence of REAL st m scalar_prd_prg (c,a,b) holds ( XFS2FS* c) = (a * ( XFS2FS* b))

      proof

        let c be non empty XFinSequence of REAL ;

        assume

         A14: m scalar_prd_prg (c,a,b);

        then

        consider n be Integer such that

         A15: (c . 0 ) = (b . 0 ) and

         A16: n = (b . 0 ) and

         A17: n <> 0 implies for i be Nat st 1 <= i & i <= n holds (c . i) = (a * (b . i));

        

         A18: ( len c) = m & ex n be Integer st (c . 0 ) = (b . 0 ) & n = (b . 0 ) & (n <> 0 implies for i be Nat st 1 <= i & i <= n holds (c . i) = (a * (b . i))) by A14;

        then

         A19: ( len ( XFS2FS* c)) = (c . 0 ) by A5, AFINSQ_1:def 11;

        now

          per cases ;

            case n = 0 ;

            then ( XFS2FS* b) = ( <*> REAL ) & ( XFS2FS* c) = ( <*> REAL ) by A13, A18, A16, AFINSQ_1: 64;

            hence thesis by RVSUM_1: 46;

          end;

            case n <> 0 ;

            set p3 = ( XFS2FS* c);

            for k3 be Nat st 1 <= k3 & k3 <= ( len p3) holds (p3 . k3) = (c2 . k3)

            proof

              let k3 be Nat;

              assume that

               A20: 1 <= k3 and

               A21: k3 <= ( len p3);

              

               A22: (c . 0 ) in ( len c) by A1, A3, A18, AFINSQ_1: 86;

              then

               A23: k3 <= n by A15, A16, A21, AFINSQ_1:def 11, A1;

              then

               A24: (b . k3) = (( XFS2FS* b) . k3) by A2, A5, A16, A20, AFINSQ_1:def 11;

              ( len p3) = n by A15, A16, A22, AFINSQ_1:def 11, A1;

              

              then (p3 . k3) = (c . k3) by A15, A16, A20, A21, A22, AFINSQ_1:def 11

              .= (a * (b . k3)) by A17, A20, A23;

              hence thesis by A24, RVSUM_1: 44;

            end;

            hence thesis by A6, A15, A19, FINSEQ_1: 14;

          end;

        end;

        hence thesis;

      end;

    end;

    definition

      let b,c be XFinSequence of REAL , m be Integer;

      :: PRGCOR_2:def5

      pred m vector_minus_prg c,b means ( len c) = m & ( len b) = m & ex n be Integer st (c . 0 ) = (b . 0 ) & n = (b . 0 ) & (n <> 0 implies for i be Nat st 1 <= i & i <= n holds (c . i) = ( - (b . i)));

    end

    theorem :: PRGCOR_2:7

    for b be non empty XFinSequence of REAL , m be Nat st (b . 0 ) is Nat & ( len b) = m & (b . 0 ) < m holds (ex c be XFinSequence of REAL st m vector_minus_prg (c,b)) & for c be non empty XFinSequence of REAL st m vector_minus_prg (c,b) holds ( XFS2FS* c) = ( - ( XFS2FS* b))

    proof

      let b be non empty XFinSequence of REAL , m be Nat;

      assume that

       A1: (b . 0 ) is Nat and

       A2: ( len b) = m and

       A3: (b . 0 ) < m;

      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 ( Segm 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 be XFinSequence of REAL such that

       A7: ( len p) = m and

       A8: p is_an_xrep_of c2 by A3, Th2, NUMBERS: 19;

      reconsider b0 = (b . 0 ) as Element of REAL by XREAL_0:def 1;

      reconsider p2 = ( Replace (p, 0 ,b0)) as XFinSequence of REAL ;

      

       A9: k <> 0 implies for i be Nat st 1 <= i & i <= k holds (p2 . i) = ( - (b . i))

      proof

        assume k <> 0 ;

        let i be Nat;

        assume that

         A10: 1 <= i and

         A11: i <= k;

        (( 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, ORDINAL1:def 12;

        hence thesis by A10, A12, AFINSQ_1: 44;

      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;

      hence ex c be XFinSequence of REAL st m vector_minus_prg (c,b);

      

       A13: 0 < ( len b);

      thus for c be non empty XFinSequence of REAL st m vector_minus_prg (c,b) holds ( XFS2FS* c) = ( - ( XFS2FS* b))

      proof

        let c be non empty XFinSequence of REAL ;

        assume

         A14: m vector_minus_prg (c,b);

        then

        consider n be Integer such that

         A15: (c . 0 ) = (b . 0 ) and

         A16: n = (b . 0 ) and

         A17: n <> 0 implies for i be Nat st 1 <= i & i <= n holds (c . i) = ( - (b . i));

        

         A18: ( len c) = m & ex n be Integer st (c . 0 ) = (b . 0 ) & n = (b . 0 ) & (n <> 0 implies for i be Nat st 1 <= i & i <= n holds (c . i) = ( - (b . i))) by A14;

        then

         A19: ( len ( XFS2FS* c)) = (c . 0 ) by A5, AFINSQ_1:def 11;

        now

          per cases ;

            case

             A20: n = 0 ;

            then ( XFS2FS* b) = ( <*> REAL ) by A13, A16, AFINSQ_1: 64;

            hence thesis by A18, A16, A20, AFINSQ_1: 64, RVSUM_1: 19;

          end;

            case n <> 0 ;

            set p3 = ( XFS2FS* c);

            for k3 be Nat st 1 <= k3 & k3 <= ( len p3) holds (p3 . k3) = (c2 . k3)

            proof

              let k3 be Nat;

              

               A21: (c . 0 ) in ( len c) by A1, A3, A18, AFINSQ_1: 86;

              then

               A22: ( len p3) = n by A15, A16, AFINSQ_1:def 11, A1;

              assume

               A23: 1 <= k3 & k3 <= ( len p3);

              then

               A24: (b . k3) = (( XFS2FS* b) . k3) by A2, A5, A16, A22, AFINSQ_1:def 11;

              (p3 . k3) = (c . k3) by A15, A16, A23, A21, A22, AFINSQ_1:def 11

              .= ( - (b . k3)) by A17, A23, A22;

              hence thesis by A24, RVSUM_1: 17;

            end;

            hence thesis by A6, A15, A19, FINSEQ_1: 14;

          end;

        end;

        hence thesis;

      end;

    end;

    definition

      let a,b,c be XFinSequence of REAL , m be Integer;

      :: PRGCOR_2:def6

      pred m vector_add_prg c,a,b means ( len c) = m & ( len a) = m & ( len b) = m & ex n be Integer st (c . 0 ) = (b . 0 ) & n = (b . 0 ) & (n <> 0 implies for i be Nat st 1 <= i & i <= n holds (c . i) = ((a . i) + (b . i)));

    end

    theorem :: PRGCOR_2:8

    for a,b be non empty XFinSequence of REAL , m be Nat st (b . 0 ) is Nat & ( len a) = m & ( len b) = m & (a . 0 ) = (b . 0 ) & (b . 0 ) < m holds (ex c be XFinSequence of REAL st m vector_add_prg (c,a,b)) & for c be non empty XFinSequence of REAL st m vector_add_prg (c,a,b) holds ( XFS2FS* c) = (( XFS2FS* a) + ( XFS2FS* b))

    proof

      let a,b be non empty XFinSequence of REAL , m be Nat;

      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;

      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 ( Segm 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 be XFinSequence of REAL such that

       A11: ( len p) = m and

       A12: p is_an_xrep_of c2 by A5, Th2, NUMBERS: 19;

      reconsider b0 = (b . 0 ) as Element of REAL by XREAL_0:def 1;

      reconsider p2 = ( Replace (p, 0 ,b0)) as XFinSequence of REAL ;

       A13:

      now

        assume k <> 0 ;

        thus for i be Nat st 1 <= i & i <= k holds (p2 . i) = ((a . i) + (b . i))

        proof

          let i be Nat;

          assume that

           A14: 1 <= i and

           A15: i <= k;

          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, ORDINAL1:def 12;

          hence thesis by A14, A17, AFINSQ_1: 44;

        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;

      hence ex c be XFinSequence of REAL st m vector_add_prg (c,a,b);

      

       A18: 0 < ( len b);

      thus for c be non empty XFinSequence of REAL st m vector_add_prg (c,a,b) holds ( XFS2FS* c) = (( XFS2FS* a) + ( XFS2FS* b))

      proof

        let c be non empty XFinSequence of REAL ;

        assume

         A19: m vector_add_prg (c,a,b);

        then

        consider n be Integer such that

         A20: (c . 0 ) = (b . 0 ) and

         A21: n = (b . 0 ) and

         A22: n <> 0 implies for i be Nat st 1 <= i & i <= n holds (c . i) = ((a . i) + (b . i));

        

         A23: ( len c) = m & ex n be Integer st (c . 0 ) = (b . 0 ) & n = (b . 0 ) & (n <> 0 implies for i be Nat st 1 <= i & i <= n holds (c . i) = ((a . i) + (b . i))) by A19;

        then

         A24: ( len ( XFS2FS* c)) = (c . 0 ) by A6, AFINSQ_1:def 11;

        now

          per cases ;

            case n = 0 ;

            then ( XFS2FS* b) = ( <*> REAL ) & ( XFS2FS* c) = ( <*> REAL ) by A18, A23, A21, AFINSQ_1: 64;

            hence thesis by RVSUM_1: 12;

          end;

            case n <> 0 ;

            set p3 = ( XFS2FS* c);

            for k3 be Nat st 1 <= k3 & k3 <= ( len p3) holds (p3 . k3) = (c2 . k3)

            proof

              let k3 be Nat;

              assume that

               A25: 1 <= k3 and

               A26: k3 <= ( len p3);

              

               A27: (c . 0 ) in ( len c) by A1, A5, A23, AFINSQ_1: 86;

              then

               A28: k3 <= n by A20, A21, A26, AFINSQ_1:def 11, A1;

              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 p3) = n by A20, A21, A27, AFINSQ_1:def 11, A1;

              

              then (p3 . k3) = (c . k3) by A20, A21, A25, A26, A27, AFINSQ_1:def 11

              .= ((a . k3) + (b . k3)) by A22, A25, A28;

              hence thesis by A30, A29, VALUED_1:def 1;

            end;

            hence thesis by A10, A20, A24, FINSEQ_1: 14;

          end;

        end;

        hence thesis;

      end;

    end;

    definition

      let a,b,c be XFinSequence of REAL , m be Integer;

      :: PRGCOR_2:def7

      pred m vector_sub_prg c,a,b means ( len c) = m & ( len a) = m & ( len b) = m & ex n be Integer st (c . 0 ) = (b . 0 ) & n = (b . 0 ) & (n <> 0 implies for i be Nat st 1 <= i & i <= n holds (c . i) = ((a . i) - (b . i)));

    end

    theorem :: PRGCOR_2:9

    for a,b be non empty XFinSequence of REAL , m be Nat st (b . 0 ) is Nat & ( len a) = m & ( len b) = m & (a . 0 ) = (b . 0 ) & (b . 0 ) < m holds (ex c be XFinSequence of REAL st m vector_sub_prg (c,a,b)) & for c be non empty XFinSequence of REAL st m vector_sub_prg (c,a,b) holds ( XFS2FS* c) = (( XFS2FS* a) - ( XFS2FS* b))

    proof

      let a,b be non empty XFinSequence of REAL , m be Nat;

      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;

      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 ( Segm 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 be XFinSequence of REAL such that

       A11: ( len p) = m and

       A12: p is_an_xrep_of c2 by A5, Th2, NUMBERS: 19;

      reconsider b0 = (b . 0 ) as Element of REAL by XREAL_0:def 1;

      reconsider p2 = ( Replace (p, 0 ,b0)) as XFinSequence of REAL ;

       A13:

      now

        assume k <> 0 ;

        thus for i be Nat st 1 <= i & i <= k holds (p2 . i) = ((a . i) - (b . i))

        proof

          let i be Nat;

          assume that

           A14: 1 <= i and

           A15: i <= k;

          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, ORDINAL1:def 12;

          hence thesis by A14, A17, AFINSQ_1: 44;

        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;

      hence ex c be XFinSequence of REAL st m vector_sub_prg (c,a,b);

      

       A18: 0 < ( len b);

      thus for c be non empty XFinSequence of REAL st m vector_sub_prg (c,a,b) holds ( XFS2FS* c) = (( XFS2FS* a) - ( XFS2FS* b))

      proof

        let c be non empty XFinSequence of REAL ;

        assume

         A19: m vector_sub_prg (c,a,b);

        then

        consider n be Integer such that

         A20: (c . 0 ) = (b . 0 ) and

         A21: n = (b . 0 ) and

         A22: n <> 0 implies for i be Nat st 1 <= i & i <= n holds (c . i) = ((a . i) - (b . i));

        

         A23: ( len c) = m & ex n be Integer st (c . 0 ) = (b . 0 ) & n = (b . 0 ) & (n <> 0 implies for i be Nat st 1 <= i & i <= n holds (c . i) = ((a . i) - (b . i))) by A19;

        then

         A24: ( len ( XFS2FS* c)) = (c . 0 ) by A6, AFINSQ_1:def 11;

        now

          per cases ;

            case n = 0 ;

            then ( XFS2FS* b) = ( <*> REAL ) & ( XFS2FS* c) = ( <*> REAL ) by A18, A23, A21, AFINSQ_1: 64;

            hence thesis by RVSUM_1: 28;

          end;

            case n <> 0 ;

            set p3 = ( XFS2FS* c);

            for k3 be Nat st 1 <= k3 & k3 <= ( len p3) holds (p3 . k3) = (c2 . k3)

            proof

              let k3 be Nat;

              assume that

               A25: 1 <= k3 and

               A26: k3 <= ( len p3);

              

               A27: (c . 0 ) in ( len c) by A1, A5, A23, AFINSQ_1: 86;

              then

               A28: k3 <= n by A20, A21, A26, AFINSQ_1:def 11, A1;

              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 p3) = n by A20, A21, A27, AFINSQ_1:def 11, A1;

              

              then (p3 . k3) = (c . k3) by A20, A21, A25, A26, A27, AFINSQ_1:def 11

              .= ((a . k3) - (b . k3)) by A22, A25, A26, A31;

              hence thesis by A30, A29, VALUED_1: 13;

            end;

            hence thesis by A10, A20, A24, FINSEQ_1: 14;

          end;

        end;

        hence thesis;

      end;

    end;