algseq_1.miz



    begin

    reserve i,k,l,m,n for Nat,

x for set;

    reserve R for non empty ZeroStr;

    definition

      let R;

      let F be sequence of R;

      :: original: finite-Support

      redefine

      :: ALGSEQ_1:def1

      attr F is finite-Support means

      : Def1: ex n st for i st i >= n holds (F . i) = ( 0. R);

      compatibility

      proof

        thus F is finite-Support implies ex n st for i st i >= n holds (F . i) = ( 0. R)

        proof

          assume

           A1: ( Support F) is finite;

          per cases ;

            suppose

             A2: ( Support F) = {} ;

            take 0 ;

            let i;

            assume i >= 0 ;

            assume

             A3: (F . i) <> ( 0. R);

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

            i in ( Support F) by A3, POLYNOM1:def 4;

            hence contradiction by A2;

          end;

            suppose ( Support F) <> {} ;

            then

            reconsider A = ( Support F) as non empty finite Subset of NAT by A1;

            take n = (( max A) + 1);

            let i;

            assume i >= n;

            then

             A4: i > ( max A) by NAT_1: 13;

            assume

             A5: (F . i) <> ( 0. R);

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

            i in ( Support F) by A5, POLYNOM1:def 4;

            hence contradiction by A4, XXREAL_2:def 8;

          end;

        end;

        given n such that

         A6: for i st i >= n holds (F . i) = ( 0. R);

        ( Support F) c= ( Segm n)

        proof

          let e be object;

          assume

           A7: e in ( Support F);

          then

          reconsider i = e as Nat;

          (F . i) <> ( 0. R) by A7, POLYNOM1:def 3;

          hence e in ( Segm n) by A6, NAT_1: 44;

        end;

        hence ( Support F) is finite;

      end;

    end

    registration

      let R;

      cluster finite-Support for sequence of R;

      existence

      proof

        reconsider f = ( NAT --> ( 0. R)) as sequence of the carrier of R;

        take f, 0 ;

        let i;

        thus thesis by FUNCOP_1: 7, ORDINAL1:def 12;

      end;

    end

    definition

      let R;

      mode AlgSequence of R is finite-Support sequence of R;

    end

    reserve p,q for AlgSequence of R;

    definition

      let R, p;

      let k be Nat;

      :: ALGSEQ_1:def2

      pred k is_at_least_length_of p means

      : Def2: for i st i >= k holds (p . i) = ( 0. R);

    end

    

     Lm1: ex m st m is_at_least_length_of p

    proof

      consider n such that

       A1: for i st i >= n holds (p . i) = ( 0. R) by Def1;

      take n;

      thus thesis by A1;

    end;

    definition

      let R, p;

      :: ALGSEQ_1:def3

      func len p -> Element of NAT means

      : Def3: it is_at_least_length_of p & for m st m is_at_least_length_of p holds it <= m;

      existence

      proof

        defpred P[ Nat] means $1 is_at_least_length_of p;

        

         A1: ex m be Nat st P[m] by Lm1;

        ex k st P[k] & for n st P[n] holds k <= n from NAT_1:sch 5( A1);

        then

        consider k such that

         A2: k is_at_least_length_of p & for n st n is_at_least_length_of p holds k <= n;

        take k;

        thus thesis by A2, ORDINAL1:def 12;

      end;

      uniqueness

      proof

        let k,l be Element of NAT ;

        assume k is_at_least_length_of p & (for m st m is_at_least_length_of p holds k <= m) & l is_at_least_length_of p & for m st m is_at_least_length_of p holds l <= m;

        then k <= l & l <= k;

        hence thesis by XXREAL_0: 1;

      end;

    end

    ::$Canceled

    theorem :: ALGSEQ_1:8

    

     Th1: i >= ( len p) implies (p . i) = ( 0. R)

    proof

      assume

       A1: i >= ( len p);

      ( len p) is_at_least_length_of p by Def3;

      hence thesis by A1;

    end;

    theorem :: ALGSEQ_1:9

    

     Th2: (for i st i < k holds (p . i) <> ( 0. R)) implies ( len p) >= k

    proof

      assume

       A1: for i st i < k holds (p . i) <> ( 0. R);

      for i st i < k holds ( len p) > i

      proof

        let i;

        assume i < k;

        then (p . i) <> ( 0. R) by A1;

        hence thesis by Th1;

      end;

      hence thesis;

    end;

    theorem :: ALGSEQ_1:10

    

     Th3: ( len p) = (k + 1) implies (p . k) <> ( 0. R)

    proof

      assume

       A1: ( len p) = (k + 1);

      then k < ( len p) by XREAL_1: 29;

      then not k is_at_least_length_of p by Def3;

      then

      consider i such that

       A2: i >= k and

       A3: (p . i) <> ( 0. R);

      i < (k + 1) by A1, A3, Th1;

      then i <= k by NAT_1: 13;

      hence thesis by A2, A3, XXREAL_0: 1;

    end;

    scheme :: ALGSEQ_1:sch1

    AlgSeqLambdaF { R() -> non empty ZeroStr , A() -> Nat , F( Nat) -> Element of R() } :

ex p be AlgSequence of R() st ( len p) <= A() & for k st k < A() holds (p . k) = F(k);

      defpred P[ Nat, Element of R()] means $1 < A() & $2 = F($1) or $1 >= A() & $2 = ( 0. R());

      

       A1: for x be Element of NAT holds ex y be Element of R() st P[x, y]

      proof

        let x be Element of NAT ;

        x < A() implies x < A() & F(x) = F(x);

        hence thesis;

      end;

      ex f be sequence of the carrier of R() st for x be Element of NAT holds P[x, (f . x)] from FUNCT_2:sch 3( A1);

      then

      consider f be sequence of the carrier of R() such that

       A2: for x be Element of NAT holds x < A() & (f . x) = F(x) or x >= A() & (f . x) = ( 0. R());

      ex n st for i st i >= n holds (f . i) = ( 0. R())

      proof

        reconsider n = A() as Element of NAT by ORDINAL1:def 12;

        take n;

        let i;

        i in NAT by ORDINAL1:def 12;

        hence thesis by A2;

      end;

      then

      reconsider f as AlgSequence of R() by Def1;

      take f;

      now

        let i;

        assume

         A3: i >= A();

        i in NAT by ORDINAL1:def 12;

        hence (f . i) = ( 0. R()) by A2, A3;

      end;

      then A() is_at_least_length_of f;

      hence ( len f) <= A() by Def3;

      let k;

      k in NAT by ORDINAL1:def 12;

      hence thesis by A2;

    end;

    ::$Canceled

    theorem :: ALGSEQ_1:12

    

     Th4: ( len p) = ( len q) & (for k st k < ( len p) holds (p . k) = (q . k)) implies p = q

    proof

      assume that

       A1: ( len p) = ( len q) and

       A2: for k st k < ( len p) holds (p . k) = (q . k);

      

       A3: for x be object st x in NAT holds (p . x) = (q . x)

      proof

        let x be object;

        assume x in NAT ;

        then

        reconsider k = x as Element of NAT ;

        k >= ( len p) implies (p . k) = (q . k)

        proof

          assume

           A4: k >= ( len p);

          then (p . k) = ( 0. R) by Th1;

          hence thesis by A1, A4, Th1;

        end;

        hence thesis by A2;

      end;

      ( dom p) = NAT & ( dom q) = NAT by FUNCT_2:def 1;

      hence thesis by A3, FUNCT_1: 2;

    end;

    theorem :: ALGSEQ_1:13

    the carrier of R <> {( 0. R)} implies for k holds ex p be AlgSequence of R st ( len p) = k

    proof

      set D = the carrier of R;

      assume D <> {( 0. R)};

      then

      consider t be object such that

       A1: t in D and

       A2: t <> ( 0. R) by ZFMISC_1: 35;

      reconsider y = t as Element of R by A1;

      let k;

      deffunc F( Nat) = y;

      consider p be AlgSequence of R such that

       A3: ( len p) <= k & for i st i < k holds (p . i) = F(i) from AlgSeqLambdaF;

      for i st i < k holds (p . i) <> ( 0. R) by A2, A3;

      then ( len p) >= k by Th2;

      hence thesis by A3, XXREAL_0: 1;

    end;

    reserve x for Element of R;

    definition

      ::$Canceled

      let R, x;

      :: ALGSEQ_1:def5

      func <%x%> -> AlgSequence of R means

      : Def4: ( len it ) <= 1 & (it . 0 ) = x;

      existence

      proof

        deffunc F( Nat) = x;

        consider p such that

         A1: ( len p) <= 1 & for k st k < 1 holds (p . k) = F(k) from AlgSeqLambdaF;

        take p;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let p, q such that

         A2: ( len p) <= 1 and

         A3: (p . 0 ) = x and

         A4: ( len q) <= 1 and

         A5: (q . 0 ) = x;

        

         A6: 1 = ( 0 + 1);

         A7:

        now

          assume

           A8: x = ( 0. R);

          then ( len p) < 1 by A2, A3, A6, Th3, XXREAL_0: 1;

          then

           A9: ( len p) = 0 by NAT_1: 14;

          ( len q) < 1 by A4, A5, A6, A8, Th3, XXREAL_0: 1;

          hence ( len p) = ( len q) by A9, NAT_1: 14;

        end;

        

         A10: for k st k < ( len p) holds (p . k) = (q . k)

        proof

          let k;

          assume k < ( len p);

          then k < 1 by A2, XXREAL_0: 2;

          then k = 0 by NAT_1: 14;

          hence thesis by A3, A5;

        end;

        now

          assume

           A11: x <> ( 0. R);

          then ( len p) = 1 by A2, A3, A6, Th1, NAT_1: 8;

          hence ( len p) = ( len q) by A4, A5, A6, A11, Th1, NAT_1: 8;

        end;

        hence thesis by A7, A10, Th4;

      end;

    end

    

     Lm2: p = <%( 0. R)%> implies ( len p) = 0

    proof

      assume p = <%( 0. R)%>;

      then

       A1: (p . 0 ) = ( 0. R) & ( len p) <= 1 by Def4;

      ( 0 + 1) = 1;

      then ( len p) < 1 by A1, Th3, XXREAL_0: 1;

      hence thesis by NAT_1: 14;

    end;

    theorem :: ALGSEQ_1:14

    

     Th6: p = <%( 0. R)%> iff ( len p) = 0

    proof

      thus p = <%( 0. R)%> implies ( len p) = 0 by Lm2;

      thus ( len p) = 0 implies p = <%( 0. R)%>

      proof

        assume ( len p) = 0 ;

        then ( len p) = ( len <%( 0. R)%>) & for k st k < ( len p) holds (p . k) = ( <%( 0. R)%> . k) by Lm2, NAT_1: 2;

        hence thesis by Th4;

      end;

    end;

    ::$Canceled

    theorem :: ALGSEQ_1:16

    

     Th7: ( <%( 0. R)%> . i) = ( 0. R)

    proof

      set p0 = <%( 0. R)%>;

      now

        assume i <> 0 ;

        then i > 0 by NAT_1: 3;

        then i >= ( len p0) by Th6;

        hence thesis by Th1;

      end;

      hence thesis by Def4;

    end;

    theorem :: ALGSEQ_1:17

    p = <%( 0. R)%> iff ( rng p) = {( 0. R)}

    proof

      thus p = <%( 0. R)%> implies ( rng p) = {( 0. R)}

      proof

        assume

         A1: p = <%( 0. R)%>;

        thus ( rng p) c= {( 0. R)}

        proof

          let x be object;

          assume x in ( rng p);

          then

          consider i be object such that

           A2: i in ( dom p) and

           A3: x = (p . i) by FUNCT_1:def 3;

          reconsider i as Element of NAT by A2, FUNCT_2:def 1;

          (p . i) = ( 0. R) by A1, Th7;

          hence thesis by A3, TARSKI:def 1;

        end;

        thus {( 0. R)} c= ( rng p)

        proof

          let x be object;

          assume x in {( 0. R)};

          then x = ( 0. R) by TARSKI:def 1;

          then

           A4: (p . 0 ) = x by A1, Def4;

          ( dom p) = NAT by FUNCT_2:def 1;

          hence thesis by A4, FUNCT_1:def 3;

        end;

      end;

      thus ( rng p) = {( 0. R)} implies p = <%( 0. R)%>

      proof

        assume

         A5: ( rng p) = {( 0. R)};

        

         A6: for k st k >= 0 holds (p . k) = ( 0. R)

        proof

          let k;

          k in NAT by ORDINAL1:def 12;

          then k in ( dom p) by FUNCT_2:def 1;

          then (p . k) in ( rng p) by FUNCT_1:def 3;

          hence thesis by A5, TARSKI:def 1;

        end;

        for m st m is_at_least_length_of p holds 0 <= m by NAT_1: 2;

        then ( len p) = 0 by A6, Def2, Def3;

        hence thesis by Th6;

      end;

    end;