afinsq_1.miz



    begin

    reserve k,n for Nat,

x,y,z,y1,y2 for object,

X,Y for set,

f,g for Function;

    theorem :: AFINSQ_1:1

    

     Th0: for n be non zero Nat holds (n - 1) is Nat & 1 <= n

    proof

      let n be non zero Nat;

      

       A1: ( 0 + 1) <= n by NAT_1: 13;

      then (( 0 + 1) - 1) <= (n - 1) by XREAL_1: 9;

      then (n - 1) in NAT by INT_1: 3;

      hence (n - 1) is Nat;

      thus thesis by A1;

    end;

    theorem :: AFINSQ_1:2

    

     Th1: (( Segm n) \/ {n}) = ( Segm (n + 1))

    proof

      n in ( Segm (n + 1)) by NAT_1: 45;

      then

       A1: {n} c= ( Segm (n + 1)) by ZFMISC_1: 31;

      ( Segm n) c= ( Segm (n + 1)) by NAT_1: 39, NAT_1: 11;

      hence (( Segm n) \/ {n}) c= ( Segm (n + 1)) by A1, XBOOLE_1: 8;

      let x be object;

      assume

       A2: x in ( Segm (n + 1));

      then

      reconsider x as Nat;

      now

        x < (n + 1) by A2, NAT_1: 44;

        per cases by NAT_1: 22;

          case x < n;

          hence x in ( Segm n) by NAT_1: 44;

        end;

          case x = n;

          hence x in {n} by TARSKI:def 1;

        end;

      end;

      hence thesis by XBOOLE_0:def 3;

    end;

    theorem :: AFINSQ_1:3

    

     Th2: ( Seg n) c= ( Segm (n + 1))

    proof

      let x be object;

      assume

       A1: x in ( Seg n);

      then

      reconsider x as Element of NAT ;

      x <= n by A1, FINSEQ_1: 1;

      then x < (n + 1) by NAT_1: 13;

      hence thesis by NAT_1: 44;

    end;

    theorem :: AFINSQ_1:4

    (n + 1) = ( { 0 } \/ ( Seg n))

    proof

      thus (n + 1) c= ( { 0 } \/ ( Seg n))

      proof

        let x be object;

        assume x in (n + 1);

        then x in { j where j be Nat : j < (n + 1) } by AXIOMS: 4;

        then

        consider j be Nat such that

         A1: j = x and

         A2: j < (n + 1);

        j = 0 or 1 < (j + 1) & j <= n by A2, NAT_1: 13, XREAL_1: 29;

        then j = 0 or 1 <= j & j <= n by NAT_1: 13;

        then x in { 0 } or x in ( Seg n) by A1, FINSEQ_1: 1, TARSKI:def 1;

        hence thesis by XBOOLE_0:def 3;

      end;

      

       A3: ( Segm 1) c= ( Segm (n + 1)) by NAT_1: 39, NAT_1: 11;

      ( Seg n) c= ( Segm (n + 1)) by Th2;

      hence thesis by A3, CARD_1: 49, XBOOLE_1: 8;

    end;

    theorem :: AFINSQ_1:5

    for r be Function holds r is finite Sequence-like iff ex n st ( dom r) = n by FINSET_1: 10;

    definition

      mode XFinSequence is finite Sequence;

    end

    reserve p,q,r,s,t for XFinSequence;

    registration

      let p;

      cluster ( dom p) -> natural;

      coherence ;

    end

    notation

      let p;

      synonym len p for card p;

    end

    registration

      let p;

      identify dom p with len p;

      compatibility

      proof

        

        thus ( len p) = ( card ( dom p)) by CARD_1: 62

        .= ( dom p);

      end;

      identify len p with dom p;

      compatibility ;

    end

    definition

      let p;

      :: original: len

      redefine

      func len p -> Element of NAT ;

      coherence

      proof

        ( card p) = ( card p);

        hence thesis;

      end;

    end

    definition

      let p;

      :: original: dom

      redefine

      func dom p -> Subset of NAT ;

      coherence

      proof

        { i where i be Nat : i < ( len p) } c= NAT

        proof

          let x be object;

          assume x in { i where i be Nat : i < ( len p) };

          then ex i be Nat st i = x & i < ( len p);

          hence thesis by ORDINAL1:def 12;

        end;

        hence thesis by AXIOMS: 4;

      end;

    end

    theorem :: AFINSQ_1:6

    (ex k st ( dom f) c= k) implies ex p st f c= p

    proof

      given k such that

       A1: ( dom f) c= k;

      deffunc F( object) = (f . $1);

      consider g such that

       A2: ( dom g) = k & for x be object st x in k holds (g . x) = F(x) from FUNCT_1:sch 3;

      reconsider g as XFinSequence by A2, FINSET_1: 10, ORDINAL1:def 7;

      take g;

      let y,z be object;

      assume

       A3: [y, z] in f;

      then

       A4: y in ( dom f) by XTUPLE_0:def 12;

      then

       A5: [y, (g . y)] in g by A1, A2, FUNCT_1: 1;

      z is set by TARSKI: 1;

      then (f . y) = z by A3, A4, FUNCT_1:def 2;

      hence thesis by A1, A2, A4, A5;

    end;

    scheme :: AFINSQ_1:sch1

    XSeqEx { A() -> Nat , P[ object, object] } :

ex p st ( dom p) = A() & for k st k in A() holds P[k, (p . k)]

      provided

       A1: for k st k in A() holds ex x be object st P[k, x];

      

       A2: for x be object st x in A() holds ex y be object st P[x, y]

      proof

        let x be object;

        assume

         A3: x in A();

        A() = { i where i be Nat : i < A() } by AXIOMS: 4;

        then ex i be Nat st i = x & i < A() by A3;

        hence thesis by A1, A3;

      end;

      consider f be Function such that

       A4: ( dom f) = A() & for x be object st x in A() holds P[x, (f . x)] from CLASSES1:sch 1( A2);

      reconsider p = f as XFinSequence by A4, FINSET_1: 10, ORDINAL1:def 7;

      take p;

      thus thesis by A4;

    end;

    scheme :: AFINSQ_1:sch2

    XSeqLambda { A() -> Nat , F( object) -> object } :

ex p be XFinSequence st ( len p) = A() & for k st k in A() holds (p . k) = F(k);

      consider f be Function such that

       A1: ( dom f) = A() & for x be object st x in A() holds (f . x) = F(x) from FUNCT_1:sch 3;

      reconsider p = f as XFinSequence by A1, FINSET_1: 10, ORDINAL1:def 7;

      take p;

      thus thesis by A1;

    end;

    theorem :: AFINSQ_1:7

    z in p implies ex k st k in ( dom p) & z = [k, (p . k)]

    proof

      assume

       A1: z in p;

      then

      consider x,y be object such that

       A2: z = [x, y] by RELAT_1:def 1;

      x in ( dom p) by A1, A2, FUNCT_1: 1;

      then

      reconsider k = x as Element of NAT ;

      take k;

      thus thesis by A1, A2, FUNCT_1: 1;

    end;

    theorem :: AFINSQ_1:8

    ( dom p) = ( dom q) & (for k st k in ( dom p) holds (p . k) = (q . k)) implies p = q;

    

     Lm1: k < ( len p) iff k in ( dom p)

    proof

      thus k < ( len p) implies k in ( dom p)

      proof

        assume k < ( len p);

        then k in ( Segm ( len p)) by NAT_1: 44;

        hence k in ( dom p);

      end;

      assume k in ( dom p);

      then k in ( Segm ( len p));

      hence k < ( len p) by NAT_1: 44;

    end;

    theorem :: AFINSQ_1:9

    

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

      for x be object st x in ( dom p) holds (p . x) = (q . x) by A2, Lm1;

      hence thesis by A1;

    end;

    registration

      let p, n;

      cluster (p | n) -> finite;

      coherence ;

    end

    theorem :: AFINSQ_1:10

    ( rng p) c= ( dom f) implies (f * p) is XFinSequence

    proof

      assume ( rng p) c= ( dom f);

      then ( dom (f * p)) = ( len p) by RELAT_1: 27;

      hence thesis by ORDINAL1:def 7;

    end;

    theorem :: AFINSQ_1:11

    

     Th10: k <= ( len p) implies ( dom (p | k)) = k

    proof

      assume k <= ( len p);

      then ( Segm k) c= ( Segm ( len p)) by NAT_1: 39;

      hence ( dom (p | k)) = k by RELAT_1: 62;

    end;

    registration

      let D be set;

      cluster finite for Sequence of D;

      existence

      proof

         {} is Sequence of D by ORDINAL1: 30;

        hence thesis;

      end;

    end

    definition

      let D be set;

      mode XFinSequence of D is finite Sequence of D;

    end

    theorem :: AFINSQ_1:12

    

     Th11: for D be set, f be XFinSequence of D holds f is PartFunc of NAT , D

    proof

      let D be set, f be XFinSequence of D;

      ( dom f) c= NAT & ( rng f) c= D by RELAT_1:def 19;

      hence thesis by RELSET_1: 4;

    end;

    registration

      cluster empty -> Sequence-like for Function;

      coherence ;

    end

    reserve D for set;

    registration

      let k be Nat, a be object;

      cluster (( Segm k) --> a) -> finite Sequence-like;

      coherence ;

    end

    ::$Canceled

    theorem :: AFINSQ_1:14

    

     Th12: for D be non empty set holds ex p be XFinSequence of D st ( len p) = k

    proof

      let D be non empty set;

      set y = the Element of D;

      set p = (k --> y);

      reconsider p = (k --> y) as XFinSequence;

      reconsider p as XFinSequence of D;

      take p;

      thus thesis;

    end;

    theorem :: AFINSQ_1:15

    ( len p) = 0 iff p = {} ;

    theorem :: AFINSQ_1:16

    

     Th14: for D be set holds {} is XFinSequence of D

    proof

      let D be set;

      ( rng {} ) c= D;

      hence thesis by RELAT_1:def 19;

    end;

    registration

      let D be set;

      cluster empty for XFinSequence of D;

      existence

      proof

         {} is XFinSequence of D by Th14;

        hence thesis;

      end;

    end

    registration

      let D be non empty set;

      cluster non empty for XFinSequence of D;

      existence

      proof

        set k = 1;

        consider p be XFinSequence of D such that

         A1: ( len p) = k by Th12;

        p <> {} by A1;

        hence thesis;

      end;

    end

    definition

      let x;

      :: AFINSQ_1:def1

      func <%x%> -> set equals ( 0 .--> x);

      coherence ;

    end

    registration

      let x;

      cluster <%x%> -> non empty;

      coherence ;

    end

    definition

      let D be set;

      :: AFINSQ_1:def2

      func <%> D -> XFinSequence of D equals {} ;

      coherence by Th14;

    end

    registration

      let D be set;

      cluster ( <%> D) -> empty;

      coherence ;

    end

    definition

      let p, q;

      :: original: ^

      redefine

      :: AFINSQ_1:def3

      func p ^ q means

      : Def3: ( dom it ) = (( len p) + ( len q)) & (for k st k in ( dom p) holds (it . k) = (p . k)) & for k st k in ( dom q) holds (it . (( len p) + k)) = (q . k);

      compatibility

      proof

        let pq be Sequence;

        

         A1: (( len p) +^ ( len q)) = (( len p) + ( len q)) by CARD_2: 36;

        hereby

          assume

           A2: pq = (p ^ q);

          hence ( dom pq) = (( len p) + ( len q)) by A1, ORDINAL4:def 1;

          thus for k st k in ( dom p) holds (pq . k) = (p . k) by A2, ORDINAL4:def 1;

          let k;

          assume k in ( dom q);

          then (pq . (( len p) +^ k)) = (q . k) & k in NAT by A2, ORDINAL4:def 1;

          hence (pq . (( len p) + k)) = (q . k) by CARD_2: 36;

        end;

        assume that

         A3: ( dom pq) = (( len p) + ( len q)) and

         A4: for k st k in ( dom p) holds (pq . k) = (p . k) and

         A5: for k st k in ( dom q) holds (pq . (( len p) + k)) = (q . k);

         A6:

        now

          let a be Ordinal;

          assume

           A7: a in ( dom q);

          then

          reconsider k = a as Element of NAT ;

          

          thus (pq . (( dom p) +^ a)) = (pq . (( len p) + k)) by CARD_2: 36

          .= (q . a) by A5, A7;

        end;

        for a be Ordinal st a in ( dom p) holds (pq . a) = (p . a) by A4;

        hence thesis by A1, A3, A6, ORDINAL4:def 1;

      end;

    end

    registration

      let p, q;

      cluster (p ^ q) -> finite;

      coherence

      proof

        ( dom (p ^ q)) = (( dom p) +^ ( dom q)) by ORDINAL4:def 1;

        hence thesis by FINSET_1: 10;

      end;

    end

    theorem :: AFINSQ_1:17

    ( len (p ^ q)) = (( len p) + ( len q)) by Def3;

    theorem :: AFINSQ_1:18

    

     Th16: ( len p) <= k & k < (( len p) + ( len q)) implies ((p ^ q) . k) = (q . (k - ( len p)))

    proof

      assume that

       A1: ( len p) <= k and

       A2: k < (( len p) + ( len q));

      consider m be Nat such that

       A3: (( len p) + m) = k by A1, NAT_1: 10;

      (k - ( len p)) < ((( len p) + ( len q)) - ( len p)) by A2, XREAL_1: 14;

      then m in ( dom q) by A3, Lm1;

      hence thesis by A3, Def3;

    end;

    theorem :: AFINSQ_1:19

    

     Th17: ( len p) <= k & k < ( len (p ^ q)) implies ((p ^ q) . k) = (q . (k - ( len p)))

    proof

      assume that

       A1: ( len p) <= k and

       A2: k < ( len (p ^ q));

      k < (( len p) + ( len q)) by A2, Def3;

      hence thesis by A1, Th16;

    end;

    theorem :: AFINSQ_1:20

    

     Th18: k in ( dom (p ^ q)) implies (k in ( dom p) or ex n st n in ( dom q) & k = (( len p) + n))

    proof

      assume k in ( dom (p ^ q));

      then k in ( Segm (( len p) + ( len q))) by Def3;

      then

       A1: k < (( len p) + ( len q)) by NAT_1: 44;

      now

        assume ( len p) <= k;

        then

        consider n be Nat such that

         A2: k = (( len p) + n) by NAT_1: 10;

        ((n + ( len p)) - ( len p)) < ((( len q) + ( len p)) - ( len p)) by A1, A2, XREAL_1: 14;

        hence thesis by A2, Lm1;

      end;

      hence thesis by Lm1;

    end;

    theorem :: AFINSQ_1:21

    

     Th19: for p,q be Sequence holds ( dom p) c= ( dom (p ^ q))

    proof

      let p,q be Sequence;

      ( dom (p ^ q)) = (( dom p) +^ ( dom q)) by ORDINAL4:def 1;

      hence thesis by ORDINAL3: 24;

    end;

    theorem :: AFINSQ_1:22

    

     Th20: x in ( dom q) implies ex k st k = x & (( len p) + k) in ( dom (p ^ q))

    proof

      assume

       A1: x in ( dom q);

      then

      reconsider k = x as Element of NAT ;

      take k;

      (( len p) + k) < (( len p) + ( len q)) by XREAL_1: 8, A1, Lm1;

      then (( len p) + k) in ( Segm (( len p) + ( len q))) by NAT_1: 44;

      hence thesis by Def3;

    end;

    theorem :: AFINSQ_1:23

    

     Th21: k in ( dom q) implies (( len p) + k) in ( dom (p ^ q))

    proof

      assume k in ( dom q);

      then ex n st n = k & (( len p) + n) in ( dom (p ^ q)) by Th20;

      hence thesis;

    end;

    theorem :: AFINSQ_1:24

    ( rng p) c= ( rng (p ^ q))

    proof

      

       A1: ( dom p) c= ( dom (p ^ q)) by Th19;

      let x be object;

      assume x in ( rng p);

      then

      consider y be object such that

       A2: y in ( dom p) and

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

      reconsider k = y as Element of NAT by A2;

      ((p ^ q) . k) = (p . k) by A2, Def3;

      hence x in ( rng (p ^ q)) by A2, A3, A1, FUNCT_1: 3;

    end;

    theorem :: AFINSQ_1:25

    ( rng q) c= ( rng (p ^ q))

    proof

      let x be object;

      assume x in ( rng q);

      then

      consider y be object such that

       A1: y in ( dom q) and

       A2: x = (q . y) by FUNCT_1:def 3;

      reconsider k = y as Element of NAT by A1;

      (( len p) + k) in ( dom (p ^ q)) & ((p ^ q) . (( len p) + k)) = (q . k) by A1, Def3, Th21;

      hence x in ( rng (p ^ q)) by A2, FUNCT_1: 3;

    end;

    theorem :: AFINSQ_1:26

    

     Th24: ( rng (p ^ q)) = (( rng p) \/ ( rng q)) by ORDINAL4: 2;

    theorem :: AFINSQ_1:27

    

     Th25: ((p ^ q) ^ r) = (p ^ (q ^ r))

    proof

      

       A1: for k st k in ( dom p) holds (((p ^ q) ^ r) . k) = (p . k)

      proof

        let k;

        assume

         A2: k in ( dom p);

        ( dom p) c= ( dom (p ^ q)) by Th19;

        

        hence (((p ^ q) ^ r) . k) = ((p ^ q) . k) by A2, Def3

        .= (p . k) by A2, Def3;

      end;

      

       A3: for k st k in ( dom (q ^ r)) holds (((p ^ q) ^ r) . (( len p) + k)) = ((q ^ r) . k)

      proof

        let k;

        assume

         A4: k in ( dom (q ^ r));

         A5:

        now

          assume not k in ( dom q);

          then

          consider n such that

           A6: n in ( dom r) and

           A7: k = (( len q) + n) by A4, Th18;

          

          thus (((p ^ q) ^ r) . (( len p) + k)) = (((p ^ q) ^ r) . ((( len p) + ( len q)) + n)) by A7

          .= (((p ^ q) ^ r) . (( len (p ^ q)) + n)) by Def3

          .= (r . n) by A6, Def3

          .= ((q ^ r) . k) by A6, A7, Def3;

        end;

        now

          assume

           A8: k in ( dom q);

          then (( len p) + k) in ( dom (p ^ q)) by Th21;

          

          hence (((p ^ q) ^ r) . (( len p) + k)) = ((p ^ q) . (( len p) + k)) by Def3

          .= (q . k) by A8, Def3

          .= ((q ^ r) . k) by A8, Def3;

        end;

        hence thesis by A5;

      end;

      ( dom ((p ^ q) ^ r)) = (( len (p ^ q)) + ( len r)) by Def3

      .= ((( len p) + ( len q)) + ( len r)) by Def3

      .= (( len p) + (( len q) + ( len r)))

      .= (( len p) + ( len (q ^ r))) by Def3;

      hence thesis by A1, A3, Def3;

    end;

    theorem :: AFINSQ_1:28

    

     Th26: (p ^ r) = (q ^ r) or (r ^ p) = (r ^ q) implies p = q

    proof

       A1:

      now

        assume

         A2: (p ^ r) = (q ^ r);

        then (( len p) + ( len r)) = ( len (q ^ r)) by Def3;

        then

         A3: (( len p) + ( len r)) = (( len q) + ( len r)) by Def3;

        for k st k in ( dom p) holds (p . k) = (q . k)

        proof

          let k;

          assume

           A4: k in ( dom p);

          

          hence (p . k) = ((q ^ r) . k) by A2, Def3

          .= (q . k) by A3, A4, Def3;

        end;

        hence thesis by A3;

      end;

       A5:

      now

        assume

         A6: (r ^ p) = (r ^ q);

        

        then

         A7: (( len r) + ( len p)) = ( len (r ^ q)) by Def3

        .= (( len r) + ( len q)) by Def3;

        for k st k in ( dom p) holds (p . k) = (q . k)

        proof

          let k;

          assume

           A8: k in ( dom p);

          

          hence (p . k) = ((r ^ q) . (( len r) + k)) by A6, Def3

          .= (q . k) by A7, A8, Def3;

        end;

        hence thesis by A7;

      end;

      assume (p ^ r) = (q ^ r) or (r ^ p) = (r ^ q);

      hence thesis by A1, A5;

    end;

    registration

      let p;

      reduce (p ^ {} ) to p;

      reducibility

      proof

        

         A1: for k st k in ( dom p) holds (p . k) = ((p ^ {} ) . k) by Def3;

        ( dom (p ^ {} )) = (( len p) + ( len {} )) by Def3

        .= ( dom p);

        hence (p ^ {} ) = p by A1;

      end;

      reduce ( {} ^ p) to p;

      reducibility

      proof

        

         A2: for k st k in ( dom p) holds (p . k) = (( {} ^ p) . k)

        proof

          let k;

          assume

           A3: k in ( dom p);

          

          thus (( {} ^ p) . k) = (( {} ^ p) . (( len {} ) + k))

          .= (p . k) by A3, Def3;

        end;

        ( dom ( {} ^ p)) = (( len {} ) + ( len p)) by Def3

        .= ( dom p);

        hence thesis by A2;

      end;

    end

    ::$Canceled

    theorem :: AFINSQ_1:30

    

     Th27: (p ^ q) = {} implies p = {} & q = {}

    proof

      assume (p ^ q) = {} ;

      

      then 0 = ( len (p ^ q))

      .= (( len p) + ( len q)) by Def3;

      hence thesis;

    end;

    registration

      let D be set;

      let p,q be XFinSequence of D;

      cluster (p ^ q) -> D -valued;

      coherence

      proof

        

         A1: ( rng q) c= D by RELAT_1:def 19;

        ( rng (p ^ q)) = (( rng p) \/ ( rng q)) & ( rng p) c= D by Th24, RELAT_1:def 19;

        hence thesis by A1, XBOOLE_1: 8;

      end;

    end

    

     Lm2: for x1,y1 be set holds [x, y] in { [x1, y1]} implies x = x1 & y = y1

    proof

      let x1,y1 be set;

      assume [x, y] in { [x1, y1]};

      then [x, y] = [x1, y1] by TARSKI:def 1;

      hence thesis by XTUPLE_0: 1;

    end;

    definition

      let x;

      :: original: <%

      redefine

      :: AFINSQ_1:def4

      func <%x%> -> Function means

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

      coherence ;

      compatibility

      proof

        let f be Function;

        thus f = <%x%> implies ( dom f) = 1 & (f . 0 ) = x by CARD_1: 49, FUNCOP_1: 72;

        assume that

         A1: ( dom f) = 1 and

         A2: (f . 0 ) = x;

        reconsider g = { [ 0 , (f . 0 )]} as Function;

        for y,z be object holds [y, z] in f iff [y, z] in g

        proof

          let y,z be object;

          hereby

            assume

             A3: [y, z] in f;

            then y in { 0 } by A1, CARD_1: 49, XTUPLE_0:def 12;

            then

             A4: y = 0 by TARSKI:def 1;

            

             A5: ( rng f) = {(f . 0 )} by A1, CARD_1: 49, FUNCT_1: 4;

            z in ( rng f) by A3, XTUPLE_0:def 13;

            then z = (f . 0 ) by A5, TARSKI:def 1;

            hence [y, z] in g by A4, TARSKI:def 1;

          end;

          assume [y, z] in g;

          then

           A6: y = 0 & z = (f . 0 ) by Lm2;

           0 in ( dom f) by A1, CARD_1: 49, TARSKI:def 1;

          hence thesis by A6, FUNCT_1:def 2;

        end;

        then f = { [ 0 , (f . 0 )]};

        hence thesis by A2, FUNCT_4: 82;

      end;

    end

    registration

      let x;

      cluster <%x%> -> Function-like Relation-like;

      coherence ;

    end

    registration

      let x;

      cluster <%x%> -> finite Sequence-like;

      coherence by Def4;

    end

    theorem :: AFINSQ_1:31

    (p ^ q) is XFinSequence of D implies p is XFinSequence of D & q is XFinSequence of D

    proof

      assume (p ^ q) is XFinSequence of D;

      then ( rng (p ^ q)) c= D by RELAT_1:def 19;

      then

       A1: (( rng p) \/ ( rng q)) c= D by Th24;

      ( rng p) c= (( rng p) \/ ( rng q)) by XBOOLE_1: 7;

      then ( rng p) c= D by A1;

      hence p is XFinSequence of D by RELAT_1:def 19;

      ( rng q) c= (( rng p) \/ ( rng q)) by XBOOLE_1: 7;

      then ( rng q) c= D by A1;

      hence thesis by RELAT_1:def 19;

    end;

    definition

      let x, y;

      :: AFINSQ_1:def5

      func <%x,y%> -> set equals ( <%x%> ^ <%y%>);

      correctness ;

      let z;

      :: AFINSQ_1:def6

      func <%x,y,z%> -> set equals (( <%x%> ^ <%y%>) ^ <%z%>);

      correctness ;

    end

    registration

      let x, y;

      cluster <%x, y%> -> Function-like Relation-like;

      coherence ;

      let z;

      cluster <%x, y, z%> -> Function-like Relation-like;

      coherence ;

    end

    registration

      let x, y;

      cluster <%x, y%> -> finite Sequence-like;

      coherence ;

      let z;

      cluster <%x, y, z%> -> finite Sequence-like;

      coherence ;

    end

    theorem :: AFINSQ_1:32

     <%x%> = { [ 0 , x]} by FUNCT_4: 82;

    theorem :: AFINSQ_1:33

    

     Th30: p = <%x%> iff ( dom p) = ( Segm 1) & ( rng p) = {x}

    proof

      thus p = <%x%> implies ( dom p) = ( Segm 1) & ( rng p) = {x}

      proof

        assume

         A1: p = <%x%>;

        hence ( dom p) = ( Segm 1) by Def4;

        ( rng p) = {(p . 0 )} by FUNCT_1: 4, A1;

        hence thesis by A1, Def4;

      end;

      assume that

       A2: ( dom p) = ( Segm 1) and

       A3: ( rng p) = {x};

      1 = ( 0 + 1);

      then (p . 0 ) in {x} by A2, A3, FUNCT_1: 3, NAT_1: 45;

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

      hence thesis by A2, Def4;

    end;

    theorem :: AFINSQ_1:34

    

     Th31: p = <%x%> iff ( len p) = 1 & (p . 0 ) = x by Def4;

    registration

      let x;

      reduce ( <%x%> . 0 ) to x;

      reducibility by Th31;

    end

    theorem :: AFINSQ_1:35

    

     Th32: (( <%x%> ^ p) . 0 ) = x

    proof

       0 in 1 by CARD_1: 49, TARSKI:def 1;

      then 0 in ( dom <%x%>) by Def4;

      then (( <%x%> ^ p) . 0 ) = ( <%x%> . 0 ) by Def3;

      hence thesis;

    end;

    theorem :: AFINSQ_1:36

    

     Th33: ((p ^ <%x%>) . ( len p)) = x

    proof

      

       A1: ( dom <%x%>) = 1 & 0 in ( Segm ( 0 + 1)) by Def4, NAT_1: 45;

      (( len p) + 0 ) = ( len p);

      

      hence ((p ^ <%x%>) . ( len p)) = ( <%x%> . 0 ) by A1, Def3

      .= x;

    end;

    theorem :: AFINSQ_1:37

     <%x, y, z%> = ( <%x%> ^ <%y, z%>) & <%x, y, z%> = ( <%x, y%> ^ <%z%>) by Th25;

    theorem :: AFINSQ_1:38

    

     Th35: p = <%x, y%> iff ( len p) = 2 & (p . 0 ) = x & (p . 1) = y

    proof

      thus p = <%x, y%> implies ( len p) = 2 & (p . 0 ) = x & (p . 1) = y

      proof

        assume

         A1: p = <%x, y%>;

        

        hence ( len p) = (( len <%x%>) + ( len <%y%>)) by Def3

        .= (1 + ( len <%y%>)) by Th30

        .= (1 + 1) by Th30

        .= 2;

         0 in { 0 } by TARSKI:def 1;

        then

         A3: 0 in ( dom <%y%>);

         0 in ( dom <%x%>) by TARSKI:def 1;

        

        hence (p . 0 ) = ( <%x%> . 0 ) by A1, Def3

        .= x;

        

        thus (p . 1) = (( <%x%> ^ <%y%>) . (( len <%x%>) + 0 )) by A1, Th30

        .= ( <%y%> . 0 ) by A3, Def3

        .= y;

      end;

      assume that

       A4: ( len p) = 2 and

       A5: (p . 0 ) = x and

       A6: (p . 1) = y;

      

       A7: for k st k in ( dom <%y%>) holds (p . (( len <%x%>) + k)) = ( <%y%> . k)

      proof

        let k;

        assume

         a8: k in ( dom <%y%>);

        

        thus (p . (( len <%x%>) + k)) = (p . (1 + k)) by Th30

        .= (p . (1 + 0 )) by a8, TARSKI:def 1

        .= ( <%y%> . 0 ) by A6

        .= ( <%y%> . k) by a8, TARSKI:def 1;

      end;

      

       A9: for k st k in ( dom <%x%>) holds (p . k) = ( <%x%> . k)

      proof

        let k;

        assume k in ( dom <%x%>);

        then k = 0 by TARSKI:def 1;

        hence thesis by A5;

      end;

      ( dom p) = (1 + 1) by A4

      .= (( len <%x%>) + 1) by Th30

      .= (( len <%x%>) + ( len <%y%>)) by Th30;

      hence thesis by A9, A7, Def3;

    end;

    registration

      let x, y;

      reduce ( <%x, y%> . 0 ) to x;

      reducibility by Th35;

      reduce ( <%x, y%> . 1) to y;

      reducibility by Th35;

    end

    theorem :: AFINSQ_1:39

    

     Th36: p = <%x, y, z%> iff ( len p) = 3 & (p . 0 ) = x & (p . 1) = y & (p . 2) = z

    proof

      thus p = <%x, y, z%> implies ( len p) = 3 & (p . 0 ) = x & (p . 1) = y & (p . 2) = z

      proof

        

         A2: 0 in ( dom <%x%>) by TARSKI:def 1;

        

         A3: 0 in ( dom <%z%>) by TARSKI:def 1;

        assume

         A4: p = <%x, y, z%>;

        

        hence ( len p) = (( len <%x, y%>) + ( len <%z%>)) by Def3

        .= (2 + ( len <%z%>)) by Th35

        .= (2 + 1) by Th30

        .= 3;

        

        thus (p . 0 ) = (( <%x%> ^ <%y, z%>) . 0 ) by A4, Th25

        .= ( <%x%> . 0 ) by A2, Def3

        .= x;

        1 in ( Segm (1 + 1)) & ( len <%x, y%>) = 2 by Th35, NAT_1: 45;

        

        hence (p . 1) = ( <%x, y%> . 1) by A4, Def3

        .= y;

        

        thus (p . 2) = (( <%x, y%> ^ <%z%>) . (( len <%x, y%>) + 0 )) by A4, Th35

        .= ( <%z%> . 0 ) by A3, Def3

        .= z;

      end;

      assume that

       A5: ( len p) = 3 and

       A6: (p . 0 ) = x and

       A7: (p . 1) = y and

       A8: (p . 2) = z;

      

       A9: for k st k in ( dom <%x, y%>) holds (p . k) = ( <%x, y%> . k)

      proof

        

         A10: ( len <%x, y%>) = 2 by Th35;

        let k such that

         A11: k in ( dom <%x, y%>);

        

         A12: k = 1 implies (p . k) = ( <%x, y%> . k) by A7;

        k = 0 implies (p . k) = ( <%x, y%> . k) by A6;

        hence thesis by A11, A10, A12, CARD_1: 50, TARSKI:def 2;

      end;

      

       A13: for k st k in ( dom <%z%>) holds (p . (( len <%x, y%>) + k)) = ( <%z%> . k)

      proof

        let k;

        assume k in ( dom <%z%>);

        then

         A14: k = 0 by TARSKI:def 1;

        

        hence (p . (( len <%x, y%>) + k)) = (p . (2 + 0 )) by Th35

        .= ( <%z%> . k) by A8, A14;

      end;

      ( dom p) = (2 + 1) by A5

      .= (( len <%x, y%>) + 1) by Th35

      .= (( len <%x, y%>) + ( len <%z%>)) by Th30;

      hence thesis by A9, A13, Def3;

    end;

    registration

      let x, y, z;

      reduce ( <%x, y, z%> . 0 ) to x;

      reducibility by Th36;

      reduce ( <%x, y, z%> . 1) to y;

      reducibility by Th36;

      reduce ( <%x, y, z%> . 2) to z;

      reducibility by Th36;

    end

    registration

      let x;

      cluster <%x%> -> 1 -element;

      coherence by Th30;

      let y;

      cluster <%x, y%> -> 2 -element;

      coherence by Th35;

      let z;

      cluster <%x, y, z%> -> 3 -element;

      coherence by Th36;

    end

    registration

      let n be Nat;

      cluster n -element -> n -defined for XFinSequence;

      coherence ;

    end

    registration

      let n be Nat, x be object;

      cluster (n --> x) -> finite Sequence-like;

      coherence ;

    end

    registration

      let n be Nat;

      cluster n -element for XFinSequence;

      existence

      proof

        take (n --> 0 );

        thus ( card (n --> 0 )) = n;

      end;

    end

    registration

      let n be Nat;

      cluster -> total for n -elementn -defined XFinSequence;

      coherence

      proof

        let s be n -element XFinSequence;

        thus ( dom s) = n by CARD_1:def 7;

      end;

    end

    theorem :: AFINSQ_1:40

    

     Th37: p <> {} implies ex q, x st p = (q ^ <%x%>)

    proof

      assume p <> {} ;

      then

      consider n be Nat such that

       A1: ( len p) = (n + 1) by NAT_1: 6;

      

       A2: ( dom p) = ( Segm (n + 1)) by A1;

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

      set q = (p | n);

      ( dom q) = (( len p) /\ n) & ( Segm n) c= ( Segm ( len p)) by A1, NAT_1: 11, NAT_1: 39, RELAT_1: 61;

      then

       A3: ( dom q) = n by XBOOLE_1: 28;

      

       A4: for x be object st x in ( dom p) holds (p . x) = ((q ^ <%(p . (( len p) - 1))%>) . x)

      proof

        let x be object;

        assume

         A5: x in ( dom p);

        then

        reconsider k = x as Element of NAT ;

         A6:

        now

          assume

           A7: k in n;

          

          hence (p . k) = (q . k) by A3, FUNCT_1: 47

          .= ((q ^ <%(p . (( len p) - 1))%>) . k) by A3, A7, Def3;

        end;

         A8:

        now

           0 in ( Segm ( 0 + 1)) by NAT_1: 45;

          then

           A9: 0 in ( dom <%(p . (( len p) - 1))%>) by Def4;

          assume

           A10: k in {n};

          

          hence ((q ^ <%(p . (( len p) - 1))%>) . k) = ((q ^ <%(p . (( len p) - 1))%>) . (( len q) + 0 )) by A3, TARSKI:def 1

          .= ( <%(p . (( len p) - 1))%> . 0 ) by A9, Def3

          .= (p . k) by A1, A10, TARSKI:def 1;

        end;

        k in (( Segm n) \/ {n}) by A5, Th1, A2;

        hence thesis by A6, A8, XBOOLE_0:def 3;

      end;

      take q;

      take (p . (( len p) - 1));

      ( dom (q ^ <%(p . (( len p) - 1))%>)) = (( len q) + ( len <%(p . (( len p) - 1))%>)) by Def3

      .= ( dom p) by A1, A3, Th30;

      hence (q ^ <%(p . (( len p) - 1))%>) = p by A4;

    end;

    registration

      let D be non empty set;

      let d1 be Element of D;

      cluster <%d1%> -> D -valued;

      coherence ;

      let d2 be Element of D;

      cluster <%d1, d2%> -> D -valued;

      coherence ;

      let d3 be Element of D;

      cluster <%d1, d2, d3%> -> D -valued;

      coherence ;

    end

    scheme :: AFINSQ_1:sch3

    IndXSeq { P[ XFinSequence] } :

for p holds P[p]

      provided

       A1: P[ {} ]

       and

       A2: for p, x st P[p] holds P[(p ^ <%x%>)];

      defpred P1[ Real] means for p st ( len p) = $1 holds P[p];

      let p;

      consider X be Subset of REAL such that

       A3: for x be Element of REAL holds x in X iff P1[x] from SUBSET_1:sch 3;

      for k holds k in X

      proof

        

         A4: 0 in REAL by XREAL_0:def 1;

        defpred R[ Nat] means $1 in X;

        for p st ( len p) = 0 holds P[p]

        proof

          let p;

          assume ( len p) = 0 ;

          then p = {} ;

          hence thesis by A1;

        end;

        then

         A5: R[ 0 ] by A3, A4;

        

         A6: for n st R[n] holds R[(n + 1)]

        proof

          let n;

          assume

           A7: R[n];

          

           A8: (n + 1) in REAL by XREAL_0:def 1;

           P1[(n + 1)]

          proof

            let p;

            assume

             A9: ( len p) = (n + 1);

            then p <> {} ;

            then

            consider w be XFinSequence, x such that

             A10: p = (w ^ <%x%>) by Th37;

            ( len p) = (( len w) + ( len <%x%>)) by A10, Def3

            .= (( len w) + 1) by Def4;

            hence P[p] by A10, A2, A3, A7, A9;

          end;

          hence thesis by A3, A8;

        end;

        thus for k holds R[k] from NAT_1:sch 2( A5, A6);

      end;

      then ( len p) in X;

      hence thesis by A3;

    end;

    theorem :: AFINSQ_1:41

    for p,q,r,s be XFinSequence st (p ^ q) = (r ^ s) & ( len p) <= ( len r) holds ex t be XFinSequence st (p ^ t) = r

    proof

      defpred P[ XFinSequence] means for p, q, s st (p ^ q) = ($1 ^ s) & ( len p) <= ( len $1) holds ex t be XFinSequence st (p ^ t) = $1;

      

       A1: for r, x st P[r] holds P[(r ^ <%x%>)]

      proof

        let r, x;

        assume

         A2: for p, q, s st (p ^ q) = (r ^ s) & ( len p) <= ( len r) holds ex t st (p ^ t) = r;

        let p, q, s;

        assume that

         A3: (p ^ q) = ((r ^ <%x%>) ^ s) and

         A4: ( len p) <= ( len (r ^ <%x%>));

         A5:

        now

          assume ( len p) <> ( len (r ^ <%x%>));

          then ( len p) <> (( len r) + ( len <%x%>)) by Def3;

          then

           A6: ( len p) <> (( len r) + 1) by Th30;

          ( len p) <= (( len r) + ( len <%x%>)) by A4, Def3;

          then

           A7: ( len p) <= (( len r) + 1) by Th30;

          (p ^ q) = (r ^ ( <%x%> ^ s)) by A3, Th25;

          then

          consider t be XFinSequence such that

           A8: (p ^ t) = r by A2, A6, A7, NAT_1: 8;

          (p ^ (t ^ <%x%>)) = (r ^ <%x%>) by A8, Th25;

          hence thesis;

        end;

        now

          assume

           A9: ( len p) = ( len (r ^ <%x%>));

          

           A10: for k st k in ( dom p) holds (p . k) = ((r ^ <%x%>) . k)

          proof

            let k;

            assume

             A11: k in ( dom p);

            

            hence (p . k) = (((r ^ <%x%>) ^ s) . k) by A3, Def3

            .= ((r ^ <%x%>) . k) by A9, A11, Def3;

          end;

          (p ^ {} ) = (r ^ <%x%>) by A9, A10;

          hence thesis;

        end;

        hence thesis by A5;

      end;

      

       A12: P[ {} ]

      proof

        let p, q, s;

        assume that (p ^ q) = ( {} ^ s) and

         A13: ( len p) <= ( len {} );

        take {} ;

        thus (p ^ {} ) = {} by A13;

      end;

      for r holds P[r] from IndXSeq( A12, A1);

      hence thesis;

    end;

    definition

      let D be set;

      :: AFINSQ_1:def7

      func D ^omega -> set means

      : Def7: x in it iff x is XFinSequence of D;

      existence

      proof

        defpred P[ object] means $1 is XFinSequence of D;

        consider X such that

         A1: x in X iff x in ( bool [: NAT , D:]) & P[x] from XBOOLE_0:sch 1;

        take X;

        let x;

        thus x in X implies x is XFinSequence of D by A1;

        assume x is XFinSequence of D;

        then

        reconsider p = x as XFinSequence of D;

        reconsider p as PartFunc of NAT , D by Th11;

        p c= [: NAT , D:];

        hence thesis by A1;

      end;

      uniqueness

      proof

        defpred P[ object] means $1 is XFinSequence of D;

        thus for X1,X2 be set st (for x be object holds x in X1 iff P[x]) & (for x be object holds x in X2 iff P[x]) holds X1 = X2 from XBOOLE_0:sch 3;

      end;

    end

    registration

      let D be set;

      cluster (D ^omega ) -> non empty;

      coherence

      proof

        set f = the XFinSequence of D;

        f in (D ^omega ) by Def7;

        hence thesis;

      end;

    end

    theorem :: AFINSQ_1:42

    x in (D ^omega ) iff x is XFinSequence of D by Def7;

    theorem :: AFINSQ_1:43

     {} in (D ^omega )

    proof

       {} = ( <%> D);

      hence thesis by Def7;

    end;

    scheme :: AFINSQ_1:sch4

    SepXSeq { D() -> non empty set , P[ XFinSequence] } :

ex X st for x holds x in X iff ex p st p in (D() ^omega ) & P[p] & x = p;

      defpred P1[ object] means ex p st P[p] & $1 = p;

      consider Y such that

       A1: for x be object holds x in Y iff x in (D() ^omega ) & P1[x] from XBOOLE_0:sch 1;

      take Y;

      x in Y implies ex p st p in (D() ^omega ) & P[p] & x = p

      proof

        assume x in Y;

        then x in (D() ^omega ) & ex p st P[p] & x = p by A1;

        hence thesis;

      end;

      hence thesis by A1;

    end;

    notation

      let p be XFinSequence;

      let i,x be set;

      synonym Replace (p,i,x) for p +* (i,x);

    end

    registration

      let p be XFinSequence;

      let i,x be object;

      cluster (p +* (i,x)) -> finite Sequence-like;

      coherence

      proof

        ( dom (p +* (i,x))) = ( dom p) by FUNCT_7: 30;

        hence thesis by FINSET_1: 10;

      end;

    end

    theorem :: AFINSQ_1:44

    for p be XFinSequence, i be Element of NAT , x be set holds ( len ( Replace (p,i,x))) = ( len p) & (i < ( len p) implies (( Replace (p,i,x)) . i) = x) & for j be Element of NAT st j <> i holds (( Replace (p,i,x)) . j) = (p . j)

    proof

      let p be XFinSequence;

      let i be Element of NAT , x be set;

      set f = ( Replace (p,i,x));

      thus ( len f) = ( len p) by FUNCT_7: 30;

      i < ( len p) implies not ( Segm ( len p)) c= ( Segm i) by NAT_1: 39;

      hence i < ( len p) implies (f . i) = x by FUNCT_7: 31, ORDINAL1: 16;

      thus thesis by FUNCT_7: 32;

    end;

    registration

      let D be non empty set;

      let p be XFinSequence of D;

      let i be Element of NAT , a be Element of D;

      cluster ( Replace (p,i,a)) -> D -valued;

      coherence

      proof

        per cases ;

          suppose i in ( dom p);

          then ( Replace (p,i,a)) = (p +* (i .--> a)) by FUNCT_7:def 3;

          then

           A1: ( rng ( Replace (p,i,a))) c= (( rng p) \/ ( rng (i .--> a))) by FUNCT_4: 17;

          ( rng (i .--> a)) = {a} by FUNCOP_1: 8;

          then

           A2: ( rng (i .--> a)) c= D by ZFMISC_1: 31;

          ( rng p) c= D by RELAT_1:def 19;

          then (( rng p) \/ ( rng (i .--> a))) c= D by A2, XBOOLE_1: 8;

          hence ( rng ( Replace (p,i,a))) c= D by A1;

        end;

          suppose not i in ( dom p);

          then ( Replace (p,i,a)) = p by FUNCT_7:def 3;

          hence ( rng ( Replace (p,i,a))) c= D by RELAT_1:def 19;

        end;

      end;

    end

    registration

      cluster -> real-valued for XFinSequence of REAL ;

      coherence

      proof

        let F be XFinSequence of REAL ;

        ( rng F) c= REAL by RELAT_1:def 19;

        hence thesis by VALUED_0:def 3;

      end;

    end

    registration

      cluster -> natural-valued for XFinSequence of NAT ;

      coherence

      proof

        let F be XFinSequence of NAT ;

        ( rng F) c= NAT by RELAT_1:def 19;

        hence thesis by VALUED_0:def 6;

      end;

    end

    registration

      cluster non empty natural-valued for XFinSequence;

      existence

      proof

         <% 0 %> is natural-valued & <% 0 %> is non empty;

        hence thesis;

      end;

    end

    theorem :: AFINSQ_1:45

    

     Th42: for x1,x2,x3,x4 be set st p = ((( <%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) holds ( len p) = 4 & (p . 0 ) = x1 & (p . 1) = x2 & (p . 2) = x3 & (p . 3) = x4

    proof

      let x1,x2,x3,x4 be set;

      assume

       A1: p = ((( <%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>);

      set p13 = (( <%x1%> ^ <%x2%>) ^ <%x3%>);

      

       A2: p13 = <%x1, x2, x3%>;

      then

       A3: ( len p13) = 3 by Th36;

      

       A4: (p13 . 0 ) = x1 & (p13 . 1) = x2 by A2;

      

       A5: (p13 . 2) = x3 by A2;

      

      thus ( len p) = (( len p13) + ( len <%x4%>)) by A1, Def3

      .= (3 + 1) by A3, Th30

      .= 4;

       0 in 3 & 1 in 3 & 2 in 3 by CARD_1: 51, ENUMSET1:def 1;

      hence (p . 0 ) = x1 & (p . 1) = x2 & (p . 2) = x3 by A1, A4, A5, Def3, A3;

      

      thus (p . 3) = (p . ( len p13)) by A2, Th36

      .= x4 by A1, Th33;

    end;

    theorem :: AFINSQ_1:46

    

     Th43: for x1,x2,x3,x4,x5 be set st p = (((( <%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) holds ( len p) = 5 & (p . 0 ) = x1 & (p . 1) = x2 & (p . 2) = x3 & (p . 3) = x4 & (p . 4) = x5

    proof

      let x1,x2,x3,x4,x5 be set;

      assume

       A1: p = (((( <%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>);

      set p14 = ((( <%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>);

      

       A2: ( len p14) = 4 by Th42;

      

       A3: (p14 . 0 ) = x1 & (p14 . 1) = x2 by Th42;

      

       A4: (p14 . 2) = x3 & (p14 . 3) = x4 by Th42;

      

      thus ( len p) = (( len p14) + ( len <%x5%>)) by A1, Def3

      .= (4 + 1) by A2, Th30

      .= 5;

       0 in 4 & ... & 3 in 4 by CARD_1: 52, ENUMSET1:def 2;

      hence (p . 0 ) = x1 & (p . 1) = x2 & (p . 2) = x3 & (p . 3) = x4 by A1, A3, A4, Def3, A2;

      

      thus (p . 4) = (p . ( len p14)) by Th42

      .= x5 by A1, Th33;

    end;

    theorem :: AFINSQ_1:47

    

     Th44: for x1,x2,x3,x4,x5,x6 be set st p = ((((( <%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) holds ( len p) = 6 & (p . 0 ) = x1 & (p . 1) = x2 & (p . 2) = x3 & (p . 3) = x4 & (p . 4) = x5 & (p . 5) = x6

    proof

      let x1,x2,x3,x4,x5,x6 be set;

      assume

       A1: p = ((((( <%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>);

      set p15 = (((( <%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>);

      

       A2: ( len p15) = 5 by Th43;

      

       A3: (p15 . 0 ) = x1 & (p15 . 1) = x2 by Th43;

      

       A4: (p15 . 2) = x3 & (p15 . 3) = x4 by Th43;

      

       A5: (p15 . 4) = x5 by Th43;

      

      thus ( len p) = (( len p15) + ( len <%x6%>)) by A1, Def3

      .= (5 + 1) by A2, Th30

      .= 6;

       0 in 5 & ... & 4 in 5 by CARD_1: 53, ENUMSET1:def 3;

      hence (p . 0 ) = x1 & (p . 1) = x2 & (p . 2) = x3 & (p . 3) = x4 & (p . 4) = x5 by A1, A3, A4, A5, Def3, A2;

      

      thus (p . 5) = (p . ( len p15)) by Th43

      .= x6 by A1, Th33;

    end;

    theorem :: AFINSQ_1:48

    

     Th45: for x1,x2,x3,x4,x5,x6,x7 be set st p = (((((( <%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) ^ <%x7%>) holds ( len p) = 7 & (p . 0 ) = x1 & (p . 1) = x2 & (p . 2) = x3 & (p . 3) = x4 & (p . 4) = x5 & (p . 5) = x6 & (p . 6) = x7

    proof

      let x1,x2,x3,x4,x5,x6,x7 be set;

      assume

       A1: p = (((((( <%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) ^ <%x7%>);

      set p16 = ((((( <%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>);

      

       A2: ( len p16) = 6 by Th44;

      

       A3: (p16 . 0 ) = x1 & (p16 . 1) = x2 by Th44;

      

       A4: (p16 . 2) = x3 & (p16 . 3) = x4 by Th44;

      

       A5: (p16 . 4) = x5 & (p16 . 5) = x6 by Th44;

      

      thus ( len p) = (( len p16) + ( len <%x7%>)) by A1, Def3

      .= (6 + 1) by A2, Th30

      .= 7;

       0 in 6 & ... & 5 in 6 by CARD_1: 54, ENUMSET1:def 4;

      hence (p . 0 ) = x1 & (p . 1) = x2 & (p . 2) = x3 & (p . 3) = x4 & (p . 4) = x5 & (p . 5) = x6 by A1, A3, A4, A5, Def3, A2;

      

      thus (p . 6) = (p . ( len p16)) by Th44

      .= x7 by A1, Th33;

    end;

    theorem :: AFINSQ_1:49

    

     Th46: for x1,x2,x3,x4,x5,x6,x7,x8 be set st p = ((((((( <%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) ^ <%x7%>) ^ <%x8%>) holds ( len p) = 8 & (p . 0 ) = x1 & (p . 1) = x2 & (p . 2) = x3 & (p . 3) = x4 & (p . 4) = x5 & (p . 5) = x6 & (p . 6) = x7 & (p . 7) = x8

    proof

      let x1,x2,x3,x4,x5,x6,x7,x8 be set;

      assume

       A1: p = ((((((( <%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) ^ <%x7%>) ^ <%x8%>);

      set p17 = (((((( <%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) ^ <%x7%>);

      

       A2: ( len p17) = 7 by Th45;

      

       A3: (p17 . 0 ) = x1 & (p17 . 1) = x2 by Th45;

      

       A4: (p17 . 2) = x3 & (p17 . 3) = x4 by Th45;

      

       A5: (p17 . 4) = x5 & (p17 . 5) = x6 by Th45;

      

       A6: (p17 . 6) = x7 by Th45;

      

      thus ( len p) = (( len p17) + ( len <%x8%>)) by A1, Def3

      .= (7 + 1) by A2, Th30

      .= 8;

       0 in 7 & ... & 6 in 7 by CARD_1: 55, ENUMSET1:def 5;

      hence (p . 0 ) = x1 & (p . 1) = x2 & (p . 2) = x3 & (p . 3) = x4 & (p . 4) = x5 & (p . 5) = x6 & (p . 6) = x7 by A1, A3, A4, A5, A6, Def3, A2;

      

      thus (p . 7) = (p . ( len p17)) by Th45

      .= x8 by A1, Th33;

    end;

    theorem :: AFINSQ_1:50

    for x1,x2,x3,x4,x5,x6,x7,x8,x9 be set st p = (((((((( <%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) ^ <%x7%>) ^ <%x8%>) ^ <%x9%>) holds ( len p) = 9 & (p . 0 ) = x1 & (p . 1) = x2 & (p . 2) = x3 & (p . 3) = x4 & (p . 4) = x5 & (p . 5) = x6 & (p . 6) = x7 & (p . 7) = x8 & (p . 8) = x9

    proof

      let x1,x2,x3,x4,x5,x6,x7,x8,x9 be set;

      assume

       A1: p = (((((((( <%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) ^ <%x7%>) ^ <%x8%>) ^ <%x9%>);

      set p17 = ((((((( <%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) ^ <%x7%>) ^ <%x8%>);

      

       A2: ( len p17) = 8 by Th46;

      

       A3: (p17 . 0 ) = x1 & (p17 . 1) = x2 by Th46;

      

       A4: (p17 . 2) = x3 & (p17 . 3) = x4 by Th46;

      

       A5: (p17 . 4) = x5 & (p17 . 5) = x6 by Th46;

      

       A6: (p17 . 6) = x7 & (p17 . 7) = x8 by Th46;

      

      thus ( len p) = (( len p17) + ( len <%x9%>)) by A1, Def3

      .= (8 + 1) by A2, Th30

      .= 9;

       0 in 8 & ... & 7 in 8 by CARD_1: 56, ENUMSET1:def 6;

      hence (p . 0 ) = x1 & (p . 1) = x2 & (p . 2) = x3 & (p . 3) = x4 & (p . 4) = x5 & (p . 5) = x6 & (p . 6) = x7 & (p . 7) = x8 by A1, A3, A4, A5, A6, Def3, A2;

      

      thus (p . 8) = (p . ( len p17)) by Th46

      .= x9 by A1, Th33;

    end;

    theorem :: AFINSQ_1:51

    n < ( len p) implies ((p ^ q) . n) = (p . n)

    proof

      assume n < ( len p);

      then n in ( dom p) by Lm1;

      hence thesis by Def3;

    end;

    theorem :: AFINSQ_1:52

    ( len p) <= n implies (p | n) = p

    proof

      assume ( len p) <= n;

      then ( Segm ( len p)) c= ( Segm n) by NAT_1: 39;

      hence thesis by RELAT_1: 68;

    end;

    theorem :: AFINSQ_1:53

    

     Th50: n <= ( len p) & k in n implies ((p | n) . k) = (p . k) & k in ( dom p)

    proof

      assume that

       A1: n <= ( len p) and

       A2: k in n;

      

       A3: ( Segm n) c= ( Segm ( len p)) by A1, NAT_1: 39;

      

      then n = (( dom p) /\ n) by XBOOLE_1: 28

      .= ( dom (p | n)) by RELAT_1: 61;

      hence thesis by A2, A3, FUNCT_1: 47;

    end;

    theorem :: AFINSQ_1:54

    

     Th51: n <= ( len p) implies ( len (p | n)) = n

    proof

      assume n <= ( len p);

      then ( Segm n) c= ( Segm ( len p)) by NAT_1: 39;

      hence thesis by RELAT_1: 62;

    end;

    theorem :: AFINSQ_1:55

    ( len (p | n)) <= n

    proof

      ( Segm ( len (p | n))) c= ( Segm n) by RELAT_1: 58;

      hence thesis by NAT_1: 39;

    end;

    theorem :: AFINSQ_1:56

    

     Th53: ( len p) = (n + 1) implies p = ((p | n) ^ <%(p . n)%>)

    proof

      set pn = (p | n);

      set x = (p . n);

      assume

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

      then

       A2: n < ( len p) by NAT_1: 13;

      then

       A3: ( len pn) = n by Th51;

       A4:

      now

        let m be Nat;

        assume m in ( dom p);

        then m < ( len p) by Lm1;

        then

         A5: m <= ( len pn) by A1, A3, NAT_1: 13;

        now

          per cases ;

            case m = ( len pn);

            hence (p . m) = ((pn ^ <%x%>) . m) by A3, Th33;

          end;

            case m <> ( len pn);

            then m < ( len pn) by A5, XXREAL_0: 1;

            then

             A6: m in ( dom pn) by Lm1;

            

            hence ((pn ^ <%x%>) . m) = (pn . m) by Def3

            .= (p . m) by A2, A3, A6, Th50;

          end;

        end;

        hence (p . m) = ((pn ^ <%x%>) . m);

      end;

      ( len (pn ^ <%x%>)) = (n + ( len <%x%>)) by A3, Def3

      .= ( len p) by A1, Def4;

      hence thesis by A4;

    end;

    theorem :: AFINSQ_1:57

    

     Th54: ((p ^ q) | ( dom p)) = p

    proof

      set r = ((p ^ q) | ( dom p));

       A1:

      now

        let k such that

         A2: k < ( len p);

        

         A3: k in ( dom p) by A2, Lm1;

        then

         A4: ((p ^ q) . k) = (p . k) by Def3;

        (k + 0 ) < (( len p) + ( len q)) by A2, XREAL_1: 8;

        then k in ( Segm (( len p) + ( len q))) by NAT_1: 44;

        then k in ( dom (p ^ q)) by Def3;

        then k in (( dom (p ^ q)) /\ ( dom p)) by A3, XBOOLE_0:def 4;

        hence (r . k) = (p . k) by A4, FUNCT_1: 48;

      end;

      ( dom p) c= ( dom (p ^ q)) by Th19;

      then ( len r) = ( len p) by RELAT_1: 62;

      hence thesis by A1, Th8;

    end;

    theorem :: AFINSQ_1:58

    n <= ( dom p) implies ((p ^ q) | n) = (p | n)

    proof

      assume n <= ( dom p);

      then ( Segm n) c= ( Segm ( len p)) by NAT_1: 39;

      then (((p ^ q) | ( dom p)) | n) = ((p ^ q) | n) by RELAT_1: 74;

      hence thesis by Th54;

    end;

    theorem :: AFINSQ_1:59

    n = (( dom p) + k) implies ((p ^ q) | n) = (p ^ (q | k))

    proof

      assume

       A1: n = (( dom p) + k);

      now

        per cases ;

          suppose

           A2: n >= ( len (p ^ q));

          then n >= (( len p) + ( len q)) by Def3;

          then ( Segm ( len q)) c= ( Segm k) by NAT_1: 39, A1, XREAL_1: 8;

          then

           A3: (q | k) = q by RELAT_1: 68;

          ( Segm ( len (p ^ q))) c= ( Segm n) by A2, NAT_1: 39;

          hence thesis by A3, RELAT_1: 68;

        end;

          suppose

           A4: n < ( len (p ^ q));

          then

           A5: ( len ((p ^ q) | n)) = n by Th10;

          n < (( len p) + ( len q)) by A4, Def3;

          then k < ( len q) by A1, XREAL_1: 6;

          then ( len (q | k)) = k by Th10;

          then

           A6: ( len (p ^ (q | k))) = (( len p) + k) by Def3;

          now

            let m be Nat such that

             A7: m in ( dom ((p ^ q) | n));

            

             A8: m < ( len ((p ^ q) | n)) by A7, Lm1;

            then m < ( len (p ^ q)) by A4, A5, XXREAL_0: 2;

            then

             A9: m in ( len (p ^ q)) by Lm1;

            m in n by A4, Th10, A7;

            then

             A10: m in (( dom (p ^ q)) /\ n) by A9, XBOOLE_0:def 4;

            then

             A11: (((p ^ q) | n) . m) = ((p ^ q) . m) by FUNCT_1: 48;

            now

              per cases ;

                suppose m < ( len p);

                then m in ( dom p) by Lm1;

                then ((p ^ (q | k)) . m) = (p . m) & ((p ^ q) . m) = (p . m) by Def3;

                hence (((p ^ q) | n) . m) = ((p ^ (q | k)) . m) by A10, FUNCT_1: 48;

              end;

                suppose

                 A12: m >= ( len p);

                m < ( len (p ^ q)) by A4, A5, A8, XXREAL_0: 2;

                then

                 A13: (q . (m - ( len p))) = ((p ^ q) . m) by A12, Th17;

                

                 A14: ((m - ( len p)) + ( len p)) < ( len (p ^ q)) by A4, A5, A8, XXREAL_0: 2;

                

                 A15: (m - ( len p)) is Nat by A12, NAT_1: 21;

                ( len (p ^ q)) = (( len p) + ( len q)) by Def3;

                then (m - ( len p)) < ( len q) by A14, XREAL_1: 6;

                then

                 A16: (m - ( len p)) in ( len q) by A15, Lm1;

                (m - ( len p)) < k by A1, A5, A14, A8, XREAL_1: 6;

                then (m - ( len p)) in ( Segm k) by A15, NAT_1: 44;

                then

                 A17: (m - ( len p)) in (k /\ ( dom q)) by A16, XBOOLE_0:def 4;

                ((p ^ (q | k)) . m) = ((q | k) . (m - ( len p))) by A1, A6, A5, A12, A8, Th17;

                hence (((p ^ q) | n) . m) = ((p ^ (q | k)) . m) by A11, A13, A17, FUNCT_1: 48;

              end;

            end;

            hence (((p ^ q) | n) . m) = ((p ^ (q | k)) . m);

          end;

          hence thesis by A6, A1, A4, Th10;

        end;

      end;

      hence thesis;

    end;

    theorem :: AFINSQ_1:60

    ex q st p = ((p | n) ^ q)

    proof

      now

        per cases ;

          suppose n > ( len p);

          then ( Segm ( len p)) c= ( Segm n) by NAT_1: 39;

          then

           A1: (p | n) = p by RELAT_1: 68;

          (p ^ {} ) = p;

          hence thesis by A1;

        end;

          suppose n <= ( len p);

          then

          reconsider n1 = (( len p) - n) as Element of NAT by NAT_1: 21;

          defpred P[ Nat] means for k st k = (( len p) - $1) holds ex q st p = ((p | k) ^ q);

          

           A2: for m be Nat st P[m] holds P[(m + 1)]

          proof

            let m be Nat such that

             A3: P[m];

            let k such that

             A4: k = (( len p) - (m + 1));

            consider q such that

             A5: p = ((p | (k + 1)) ^ q) by A3, A4;

            ( Segm k) c= ( Segm (k + 1)) by NAT_1: 39, NAT_1: 11;

            then

             A6: ((p | (k + 1)) | k) = (p | k) by RELAT_1: 74;

            (( len p) - m) <= (( len p) - 0 ) by XREAL_1: 10;

            then ( len (p | (k + 1))) = (k + 1) by Th51, A4;

            then (p | (k + 1)) = (((p | (k + 1)) | k) ^ <%((p | (k + 1)) . k)%>) by Th53;

            then p = ((p | k) ^ ( <%((p | (k + 1)) . k)%> ^ q)) by A5, A6, Th25;

            hence thesis;

          end;

          (p | (( len p) - 0 )) = p & (p ^ {} ) = p;

          then

           A7: P[ 0 ];

          

           A8: for m be Nat holds P[m] from NAT_1:sch 2( A7, A2);

          n = (( len p) - n1);

          hence thesis by A8;

        end;

      end;

      hence thesis;

    end;

    theorem :: AFINSQ_1:61

    ( len p) = (n + k) implies ex q1,q2 be XFinSequence st ( len q1) = n & ( len q2) = k & p = (q1 ^ q2)

    proof

      defpred P[ Nat] means for p be XFinSequence, i,j be Nat st ( len p) = $1 & ( len p) = (i + j) holds ex q1,q2 be XFinSequence st ( len q1) = i & ( len q2) = j & p = (q1 ^ q2);

       A1:

      now

        let n;

        assume

         A2: P[n];

        thus P[(n + 1)]

        proof

          let p be XFinSequence;

          let i,j be Nat;

          assume that

           A3: ( len p) = (n + 1) and

           A4: ( len p) = (i + j);

          per cases ;

            suppose

             A5: j = 0 ;

            take q1 = p;

            take q2 = {} ;

            thus thesis by A4, A5;

          end;

            suppose j > 0 ;

            then

            consider k such that

             A6: j = (k + 1) by NAT_1: 6;

            p <> {} by A3;

            then

            consider q be XFinSequence, x such that

             A7: p = (q ^ <%x%>) by Th37;

            

             A8: (n + 1) = (( len q) + ( len <%x%>)) by A3, A7, Def3

            .= (( len q) + 1) by Th30;

            n = (i + k) by A3, A4, A6;

            then

            consider q1,q2 be XFinSequence such that

             A9: ( len q1) = i and

             A10: ( len q2) = k and

             A11: q = (q1 ^ q2) by A2, A8;

            

             A12: ( len (q2 ^ <%x%>)) = (( len q2) + ( len <%x%>)) by Def3

            .= j by A6, A10, Th30;

            p = (q1 ^ (q2 ^ <%x%>)) by A7, A11, Th25;

            hence thesis by A9, A12;

          end;

        end;

      end;

      

       A13: P[ 0 ]

      proof

        let p be XFinSequence;

        let i,j be Nat;

        assume that

         A14: ( len p) = 0 and

         A15: ( len p) = (i + j);

        

         A16: p = ( {} ^ {} ) by A14;

        ( len {} ) = i by A14, A15;

        hence thesis by A15, A16;

      end;

      for n holds P[n] from NAT_1:sch 2( A13, A1);

      hence thesis;

    end;

    theorem :: AFINSQ_1:62

    ( <%x%> ^ p) = ( <%y%> ^ q) implies x = y & p = q

    proof

      assume

       A1: ( <%x%> ^ p) = ( <%y%> ^ q);

      (( <%x%> ^ p) . 0 ) = x by Th32;

      then x = y by A1, Th32;

      hence thesis by A1, Th26;

    end;

    definition

      let D be set, q be FinSequence of D;

      :: AFINSQ_1:def8

      func FS2XFS q -> XFinSequence of D means

      : Def8: ( len it ) = ( len q) & for i be Nat st i < ( len q) holds (q . (i + 1)) = (it . i);

      existence

      proof

        deffunc F( Nat) = (q . ($1 + 1));

        ex p be XFinSequence st ( len p) = ( len q) & for k be Nat st k in ( len q) holds (p . k) = F(k) from XSeqLambda;

        then

        consider p be XFinSequence such that

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

         A2: for k be Nat st k in ( Segm ( len q)) holds (p . k) = F(k);

        ( rng p) c= D

        proof

          let y be object;

          

           A3: ( rng q) c= D by FINSEQ_1:def 4;

          assume y in ( rng p);

          then

          consider x be object such that

           A4: x in ( dom p) and

           A5: y = (p . x) by FUNCT_1:def 3;

          reconsider nx = x as Element of NAT by A4;

          

           A6: (nx + 1) <= ( len q) by NAT_1: 13, A1, A4, Lm1;

          ( 0 + 1) <= (nx + 1) by NAT_1: 13;

          then (nx + 1) in ( Seg ( len q)) by A6, FINSEQ_1: 1;

          then (nx + 1) in ( dom q) by FINSEQ_1:def 3;

          then

           A7: (q . (nx + 1)) in ( rng q) by FUNCT_1:def 3;

          (p . nx) = (q . (nx + 1)) by A1, A2, A4;

          hence thesis by A5, A7, A3;

        end;

        then

         A8: p is XFinSequence of D by RELAT_1:def 19;

        for i be Nat st i < ( len q) holds (q . (i + 1)) = (p . i) by A2, NAT_1: 44;

        hence thesis by A1, A8;

      end;

      uniqueness

      proof

        thus for p1,p2 be XFinSequence of D st (( len p1) = ( len q) & for i be Nat st i < ( len q) holds (q . (i + 1)) = (p1 . i)) & (( len p2) = ( len q) & for i be Nat st i < ( len q) holds (q . (i + 1)) = (p2 . i)) holds p1 = p2

        proof

          let p1,p2 be XFinSequence of D;

          assume that

           A9: ( len p1) = ( len q) and

           A10: for i be Nat st i < ( len q) holds (q . (i + 1)) = (p1 . i) and

           A11: ( len p2) = ( len q) and

           A12: for i be Nat st i < ( len q) holds (q . (i + 1)) = (p2 . i);

          for i be Nat st i < ( len p1) holds (p1 . i) = (p2 . i)

          proof

            let i be Nat;

            assume

             A13: i < ( len p1);

            then (q . (i + 1)) = (p1 . i) by A9, A10;

            hence thesis by A9, A12, A13;

          end;

          hence thesis by A9, A11, Th8;

        end;

      end;

    end

    reserve i for Nat;

    definition

      let q be XFinSequence;

      :: AFINSQ_1:def9

      func XFS2FS q -> FinSequence means

      : Def9A: ( len it ) = ( len q) & for i be Nat st 1 <= i & i <= ( len q) holds (q . (i -' 1)) = (it . i);

      existence

      proof

        deffunc F( Nat) = (q . ($1 -' 1));

        ex p be FinSequence st ( len p) = ( len q) & for k be Nat st k in ( dom p) holds (p . k) = F(k) from FINSEQ_1:sch 2;

        then

        consider p be FinSequence such that

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

         A2: for k be Nat st k in ( dom p) holds (p . k) = F(k);

        

         A11: ( dom p) = ( Seg ( len q)) by A1, FINSEQ_1:def 3;

        for i be Nat st 1 <= i & i <= ( len q) holds (q . (i -' 1)) = (p . i) by A2, A11, FINSEQ_1: 1;

        hence thesis by A1;

      end;

      uniqueness

      proof

        thus for p1,p2 be FinSequence st (( len p1) = ( len q) & for i st 1 <= i & i <= ( len q) holds (q . (i -' 1)) = (p1 . i)) & (( len p2) = ( len q) & for i st 1 <= i & i <= ( len q) holds (q . (i -' 1)) = (p2 . i)) holds p1 = p2

        proof

          let p1,p2 be FinSequence;

          assume that

           A12: ( len p1) = ( len q) and

           A13: for i st 1 <= i & i <= ( len q) holds (q . (i -' 1)) = (p1 . i) and

           A14: ( len p2) = ( len q) and

           A15: for i st 1 <= i & i <= ( len q) holds (q . (i -' 1)) = (p2 . i);

          for i be Nat st 1 <= i & i <= ( len p1) holds (p1 . i) = (p2 . i)

          proof

            let i be Nat;

            assume

             A16: 1 <= i & i <= ( len p1);

            then (q . (i -' 1)) = (p1 . i) by A12, A13;

            hence thesis by A12, A15, A16;

          end;

          hence thesis by A12, A14, FINSEQ_1: 14;

        end;

      end;

    end

    definition

      let D be set, q be XFinSequence of D;

      :: original: XFS2FS

      redefine

      func XFS2FS q -> FinSequence of D ;

      coherence

      proof

        set p = ( XFS2FS q);

        

         A1: ( len p) = ( len q) by Def9A;

        ( rng p) c= D

        proof

          let y be object;

          

           A3: ( rng q) c= D by RELAT_1:def 19;

          assume y in ( rng p);

          then

          consider x be object such that

           A4: x in ( dom p) and

           A5: y = (p . x) by FUNCT_1:def 3;

          reconsider nx = x as Element of NAT by A4;

          

           A6: nx in ( Seg ( len q)) by A1, A4, FINSEQ_1:def 3;

          then

           f: 1 <= nx by FINSEQ_1: 1;

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

          then

           A7: (nx - 1) = (nx -' 1) by XREAL_0:def 2;

          

           A8: (nx -' 1) < ((nx -' 1) + 1) by NAT_1: 13;

          

           F: nx <= ( len q) by A6, FINSEQ_1: 1;

          then (nx -' 1) < ( len q) by A7, A8, XXREAL_0: 2;

          then

           a9: (nx -' 1) in ( dom q) by Lm1;

          

           AA: 1 <= nx & nx <= ( len q) by F, f;

          

           A9: (q . (nx -' 1)) in ( rng q) by FUNCT_1:def 3, a9;

          (p . nx) = (q . (nx -' 1)) by Def9A, AA;

          hence thesis by A5, A9, A3;

        end;

        hence thesis by FINSEQ_1:def 4;

      end;

    end

    theorem :: AFINSQ_1:63

    for D be set, n be Nat, r be set st r in D holds (n --> r) is XFinSequence of D;

    definition

      let D be non empty set;

      let q be FinSequence of D, n be Nat;

      assume that

       A1: n > ( len q) and

       A2: NAT c= D;

      :: AFINSQ_1:def10

      func FS2XFS* (q,n) -> non empty XFinSequence of D means ( len q) = (it . 0 ) & ( len it ) = n & (for i be Nat st 1 <= i & i <= ( len q) holds (it . i) = (q . i)) & for j be Nat st ( len q) < j & j < n holds (it . j) = 0 ;

      existence

      proof

        reconsider x = ( len q) as Element of D by A2;

        reconsider r = 0 as Element of D by A2;

        reconsider q5 = (((n -' ( len q)) -' 1) --> r) as XFinSequence of D;

        ( <%x%> ^ ( FS2XFS q)) <> {} by Th27;

        then

        reconsider p0 = (( <%x%> ^ ( FS2XFS q)) ^ q5) as non empty XFinSequence of D by Th27;

        

         A3: 0 in ( dom <%x%>) by Lm1;

        

         A4: ( len <%x%>) = 1 by Def4;

         0 in ( Segm (( len <%x%>) + ( len ( FS2XFS q)))) by NAT_1: 44;

        then 0 in ( len ( <%x%> ^ ( FS2XFS q))) by Def3;

        

        then

         A5: (p0 . 0 ) = (( <%x%> ^ ( FS2XFS q)) . 0 ) by Def3

        .= ( <%x%> . 0 ) by A3, Def3

        .= x;

        

         A6: for i st 1 <= i & i <= ( len q) holds (p0 . i) = (q . i)

        proof

          let i;

          assume that

           A7: 1 <= i and

           A8: i <= ( len q);

          

           A9: (i -' 1) = (i - 1) by XREAL_0:def 2, A7, XREAL_1: 48;

          i < (i + 1) by NAT_1: 13;

          then (i - 1) < ((i + 1) - 1) by XREAL_1: 9;

          then

           A10: (i -' 1) < ( len q) by A8, A9, XXREAL_0: 2;

          then (i -' 1) in ( Segm ( len q)) by NAT_1: 44;

          then

           A11: (i -' 1) in ( len ( FS2XFS q)) by Def8;

          i < (1 + ( len q)) by A8, NAT_1: 13;

          then i < (( len <%x%>) + ( len ( FS2XFS q))) by A4, Def8;

          then i in ( Segm (( len <%x%>) + ( len ( FS2XFS q)))) by NAT_1: 44;

          then i in ( len ( <%x%> ^ ( FS2XFS q))) by Def3;

          

          then (p0 . i) = (( <%x%> ^ ( FS2XFS q)) . (1 + (i -' 1))) by A9, Def3

          .= (( FS2XFS q) . (i -' 1)) by A4, A11, Def3

          .= (q . ((i -' 1) + 1)) by A10, Def8

          .= (q . i) by A9;

          hence thesis;

        end;

        

         A12: (n - ( len q)) > 0 by A1, XREAL_1: 50;

        then

         A13: (n -' ( len q)) = (n - ( len q)) by XREAL_0:def 2;

        then (n -' ( len q)) >= ( 0 + 1) by A12, NAT_1: 13;

        then

         A14: ((n -' ( len q)) - 1) >= 0 by XREAL_1: 48;

        

         A15: ( len q5) = ((n -' ( len q)) -' 1);

        

         A16: for j be Nat st ( len q) < j & j < n holds (p0 . j) = 0

        proof

          let j be Nat;

          assume that

           A17: ( len q) < j and

           A18: j < n;

          

           A19: ( len ( <%x%> ^ ( FS2XFS q))) = (( len <%x%>) + ( len ( FS2XFS q))) by Def3

          .= (1 + ( len q)) by A4, Def8;

          ( len q) < n by A17, A18, XXREAL_0: 2;

          then

           A20: (n - ( len q)) > 0 by XREAL_1: 50;

          then

           A21: (n -' ( len q)) = (n - ( len q)) by XREAL_0:def 2;

          then (n - ( len q)) >= ( 0 + 1) by A20, NAT_1: 13;

          then ((n -' ( len q)) - 1) >= 0 by A21, XREAL_1: 48;

          then

           A22: ((n -' ( len q)) -' 1) = (n - (( len q) + 1)) by A21, XREAL_0:def 2;

          (1 + ( len q)) <= j by A17, NAT_1: 13;

          then

           A23: (j -' (1 + ( len q))) = (j - (1 + ( len q))) by XREAL_0:def 2, XREAL_1: 48;

          (j - (( len q) + 1)) < (n - (( len q) + 1)) by A18, XREAL_1: 9;

          then

           A24: (j -' ( len ( <%x%> ^ ( FS2XFS q)))) in ( Segm ((n -' ( len q)) -' 1)) by A19, A23, A22, NAT_1: 44;

          j = (( len ( <%x%> ^ ( FS2XFS q))) + (j -' ( len ( <%x%> ^ ( FS2XFS q))))) by A19, A23;

          

          then (p0 . j) = (q5 . (j -' ( len ( <%x%> ^ ( FS2XFS q))))) by A15, A24, Def3

          .= 0 ;

          hence thesis;

        end;

        ( len p0) = (( len ( <%x%> ^ ( FS2XFS q))) + ( len q5)) by Def3

        .= ((( len <%x%>) + ( len ( FS2XFS q))) + ( len q5)) by Def3

        .= ((1 + ( len ( FS2XFS q))) + ( len q5)) by Th30

        .= ((1 + ( len q)) + ( len q5)) by Def8

        .= ((1 + ( len q)) + ((n -' ( len q)) -' 1))

        .= ((n - (( len q) + 1)) + (( len q) + 1)) by A13, A14, XREAL_0:def 2

        .= n;

        hence thesis by A5, A6, A16;

      end;

      uniqueness

      proof

        let p1,p2 be non empty XFinSequence of D;

        assume that

         A25: ( len q) = (p1 . 0 ) and

         A26: ( len p1) = n and

         A27: for i st 1 <= i & i <= ( len q) holds (p1 . i) = (q . i) and

         A28: for j be Nat st ( len q) < j & j < n holds (p1 . j) = 0 and

         A29: ( len q) = (p2 . 0 ) and

         A30: ( len p2) = n and

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

         A32: for j be Nat st ( len q) < j & j < n holds (p2 . j) = 0 ;

        for i be Nat st i < n holds (p1 . i) = (p2 . i)

        proof

          let i be Nat;

          assume i < n;

          then

           A33: i < ( 0 + 1) or 1 <= i & i <= ( len q) or ( len q) < i & i < n;

          now

            per cases by A33, NAT_1: 13;

              case i = 0 ;

              hence thesis by A25, A29;

            end;

              case

               A34: 1 <= i & i <= ( len q);

              then (p1 . i) = (q . i) by A27;

              hence thesis by A31, A34;

            end;

              case

               A35: ( len q) < i & i < n;

              then (p1 . i) = 0 by A28;

              hence thesis by A32, A35;

            end;

          end;

          hence thesis;

        end;

        hence thesis by A26, A30, Th8;

      end;

    end

    reserve m for Nat,

D for non empty set;

    definition

      let D be non empty set;

      let p be XFinSequence of D;

      assume that

       A1: (p . 0 ) is Nat and

       A2: (p . 0 ) in ( len p);

      :: AFINSQ_1:def11

      func XFS2FS* (p) -> FinSequence of D means

      : Def11: for m be Nat st m = (p . 0 ) holds ( len it ) = m & for i st 1 <= i & i <= m holds (it . i) = (p . i);

      existence

      proof

        reconsider m0 = (p . 0 ) as Element of NAT by A1, ORDINAL1:def 12;

        deffunc F( set) = (p . $1);

        ex q be FinSequence st ( len q) = m0 & for k be Nat st k in ( dom q) holds (q . k) = F(k) from FINSEQ_1:sch 2;

        then

        consider q be FinSequence such that

         A3: ( len q) = m0 and

         A4: for k be Nat st k in ( dom q) holds (q . k) = F(k);

        ( rng q) c= D

        proof

          

           A5: m0 < ( len p) by A2, Lm1;

          let y be object;

          assume y in ( rng q);

          then

          consider x be object such that

           A6: x in ( dom q) and

           A7: y = (q . x) by FUNCT_1:def 3;

          reconsider k0 = x as Element of NAT by A6;

          k0 in ( Seg m0) by A3, A6, FINSEQ_1:def 3;

          then k0 <= m0 by FINSEQ_1: 1;

          then k0 < ( len p) by A5, XXREAL_0: 2;

          then

           A8: k0 in ( dom p) by Lm1;

          y = (p . k0) by A4, A6, A7;

          then ( rng p) c= D & y in ( rng p) by A8, FUNCT_1:def 3, RELAT_1:def 19;

          hence thesis;

        end;

        then

        reconsider q0 = q as FinSequence of D by FINSEQ_1:def 4;

        

         A9: ( dom q) = ( Seg m0) by A3, FINSEQ_1:def 3;

        for m be Nat st m = (p . 0 ) holds ( len q0) = m & for i st 1 <= i & i <= m holds (q0 . i) = (p . i) by A4, A9, FINSEQ_1: 1, A3;

        hence thesis;

      end;

      uniqueness

      proof

        reconsider m2 = (p . 0 ) as Nat by A1;

        let g1,g2 be FinSequence of D;

        assume that

         A10: for m st m = (p . 0 ) holds ( len g1) = m & for i st 1 <= i & i <= m holds (g1 . i) = (p . i) and

         A11: for m st m = (p . 0 ) holds ( len g2) = m & for i st 1 <= i & i <= m holds (g2 . i) = (p . i);

        

         A12: ( len g1) = m2 by A10;

        

         A13: for i be Nat st 1 <= i & i <= ( len g1) holds (g1 . i) = (g2 . i)

        proof

          let i be Nat;

          assume

           A14: 1 <= i & i <= ( len g1);

          then (g1 . i) = (p . i) by A10, A12;

          hence thesis by A11, A12, A14;

        end;

        ( len g2) = m2 by A11;

        hence thesis by A10, A13, FINSEQ_1: 14;

      end;

    end

    theorem :: AFINSQ_1:64

    for p be XFinSequence of D st (p . 0 ) = 0 & 0 < ( len p) holds ( XFS2FS* p) = {}

    proof

      let p be XFinSequence of D;

      assume that

       A1: (p . 0 ) = 0 and

       A2: 0 < ( len p);

      set q = ( XFS2FS* p);

       0 in ( len p) by A2, Lm1;

      then ( len q) = 0 by A1, Def11;

      hence thesis;

    end;

    definition

      let F be Function;

      :: AFINSQ_1:def12

      attr F is initial means

      : Def12: for m,n be Nat st n in ( dom F) & m < n holds m in ( dom F);

    end

    registration

      cluster empty -> initial for Function;

      coherence ;

    end

    registration

      cluster -> initial for XFinSequence;

      coherence

      proof

        let p be XFinSequence;

        let m,n be Nat such that

         A1: n in ( dom p);

        assume m < n;

        then m in ( Segm n) by NAT_1: 44;

        hence m in ( dom p) by A1, ORDINAL1: 10;

      end;

    end

    registration

      cluster -> NAT -defined for XFinSequence;

      coherence

      proof

        let f be XFinSequence;

        thus ( dom f) c= NAT ;

      end;

    end

    theorem :: AFINSQ_1:65

    

     Th62: for F be non empty initial NAT -defined Function holds 0 in ( dom F)

    proof

      let F be non empty initial NAT -defined Function;

      consider x be object such that

       A1: x in ( dom F) by XBOOLE_0:def 1;

      ( dom F) c= NAT by RELAT_1:def 18;

      then

      reconsider x as Element of NAT by A1;

      x = 0 or 0 < x;

      hence 0 in ( dom F) by A1, Def12;

    end;

    registration

      cluster initial finite NAT -defined -> Sequence-like for Function;

      coherence

      proof

        let F be Function;

        assume

         A1: F is initial finite NAT -defined;

        thus ( dom F) is epsilon-transitive

        proof

          let x be set;

          assume

           A2: x in ( dom F);

          then

          reconsider i = x as Nat by A1;

          let y be object;

          assume y in x;

          then

           A3: y in ( Segm i);

          then

          reconsider j = y as Nat;

          thus y in ( dom F) by A1, A2, NAT_1: 44, A3;

        end;

        let x,y be set;

        assume x in ( dom F) & y in ( dom F);

        then

        reconsider x, y as Ordinal by A1;

        x in y or x = y or y in x by ORDINAL1: 14;

        hence thesis;

      end;

    end

    theorem :: AFINSQ_1:66

    for F be finite initial NAT -defined Function holds for n be Nat holds n in ( dom F) iff n < ( card F) by Lm1;

    theorem :: AFINSQ_1:67

    for F be initial NAT -defined Function, G be NAT -defined Function st ( dom F) = ( dom G) holds G is initial by Def12;

    theorem :: AFINSQ_1:68

    for F be initial NAT -defined finite Function holds ( dom F) = { k where k be Element of NAT : k < ( card F) }

    proof

      let F be initial NAT -defined finite Function;

      hereby

        let x be object;

        assume

         A1: x in ( dom F);

        then

        reconsider f = x as Element of NAT ;

        f < ( card F) by A1, Lm1;

        hence x in { k where k be Element of NAT : k < ( card F) };

      end;

      let x be object;

      assume x in { k where k be Element of NAT : k < ( card F) };

      then ex k be Element of NAT st x = k & k < ( card F);

      hence thesis by Lm1;

    end;

    theorem :: AFINSQ_1:69

    for F be non empty XFinSequence, G be non empty NAT -defined finite Function st F c= G & ( LastLoc F) = ( LastLoc G) holds F = G

    proof

      let F be initial non empty NAT -defined finite Function, G be non empty NAT -defined finite Function such that

       A1: F c= G and

       A2: ( LastLoc F) = ( LastLoc G);

      ( dom F) = ( dom G)

      proof

        thus ( dom F) c= ( dom G) by A1, GRFUNC_1: 2;

        let x be object;

        assume

         A3: x in ( dom G);

        ( dom G) c= NAT by RELAT_1:def 18;

        then

        reconsider x as Element of NAT by A3;

        

         A4: ( LastLoc F) in ( dom F) by VALUED_1: 30;

        x <= ( LastLoc F) by A2, A3, VALUED_1: 32;

        then x < ( LastLoc F) or x = ( LastLoc F) by XXREAL_0: 1;

        hence thesis by A4, Def12;

      end;

      hence thesis by A1, GRFUNC_1: 3;

    end;

    theorem :: AFINSQ_1:70

    

     Th67: for F be non empty XFinSequence holds ( LastLoc F) = (( card F) -' 1)

    proof

      let F be initial non empty NAT -defined finite Function;

      consider k be Nat such that

       A1: ( LastLoc F) = k;

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

      k < ( card F) by A1, Lm1, VALUED_1: 30;

      then

       A2: k <= (( card F) -' 1) by NAT_D: 49;

      per cases by A2, XXREAL_0: 1;

        suppose k < (( card F) -' 1);

        then (k + 1) < ((( card F) -' 1) + 1) by XREAL_1: 6;

        then (k + 1) < ( card F) by NAT_1: 14, XREAL_1: 235;

        then

         A3: (k + 1) <= k by A1, VALUED_1: 32, Lm1;

        k <= (k + 1) by NAT_1: 11;

        then (k + 0 ) = (k + 1) by A3, XXREAL_0: 1;

        hence thesis;

      end;

        suppose k = (( card F) -' 1);

        hence thesis by A1;

      end;

    end;

    theorem :: AFINSQ_1:71

    for F be initial non empty NAT -defined finite Function holds ( FirstLoc F) = 0 by Th62, VALUED_1: 35;

    registration

      let F be initial non empty NAT -defined finite Function;

      cluster ( CutLastLoc F) -> initial;

      coherence

      proof

        set G = ( CutLastLoc F);

        per cases ;

          suppose G is empty;

          then

          reconsider H = G as empty finite Function;

          H is initial;

          hence thesis;

        end;

          suppose G is non empty;

          then

          reconsider G as non empty finite Function;

          G is initial

          proof

            let m,l be Nat such that

             A1: l in ( dom G) and

             A2: m < l;

            set M = ( dom F);

            reconsider R = { [( LastLoc F), (F . ( LastLoc F))]} as Relation;

            

             a3: R = (( LastLoc F) .--> (F . ( LastLoc F))) by FUNCT_4: 82;

            then

             A4: (( dom F) \ ( dom R)) = ( dom G) by VALUED_1: 36;

            then l in ( dom F) by A1, XBOOLE_0:def 5;

            then

             A5: m in ( dom F) by A2, Def12;

            l in M by A4, A1, XBOOLE_0:def 5;

            then m <> ( LastLoc F) by A2, XXREAL_2:def 8;

            then not m in {( LastLoc F)} by TARSKI:def 1;

            hence thesis by a3, A4, A5, XBOOLE_0:def 5;

          end;

          hence thesis;

        end;

      end;

    end

    reserve l for Nat;

    theorem :: AFINSQ_1:72

    for I be finite initial NAT -defined Function, J be Function holds ( dom I) misses ( dom ( Shift (J,( card I))))

    proof

      let I be finite initial NAT -defined Function, J be Function;

      assume

       A1: ( dom I) meets ( dom ( Shift (J,( card I))));

      ( dom ( Shift (J,( card I)))) = { (l + ( card I)) : l in ( dom J) } by VALUED_1:def 12;

      then

      consider x be object such that

       A2: x in ( dom I) and

       A3: x in { (l + ( card I)) : l in ( dom J) } by A1, XBOOLE_0: 3;

      consider l such that

       A4: x = (l + ( card I)) and l in ( dom J) by A3;

      thus contradiction by NAT_1: 11, A2, A4, Lm1;

    end;

    theorem :: AFINSQ_1:73

     not m in ( dom p) implies not (m + 1) in ( dom p)

    proof

      assume not m in ( dom p);

      then

       A1: m >= ( card p) by Lm1;

      (m + 1) >= m by NAT_1: 11;

      hence thesis by Lm1, A1, XXREAL_0: 2;

    end;

    registration

      let D be set;

      cluster (D ^omega ) -> functional;

      coherence by Def7;

    end

    registration

      let D be set;

      cluster -> finite Sequence-like for Element of (D ^omega );

      coherence by Def7;

    end

    definition

      let D be set;

      let f be XFinSequence of D;

      :: AFINSQ_1:def13

      func Down f -> Element of (D ^omega ) equals f;

      coherence by Def7;

    end

    definition

      let D be set;

      let f be XFinSequence of D, g be Element of (D ^omega );

      :: original: ^

      redefine

      func f ^ g -> Element of (D ^omega ) ;

      coherence

      proof

        reconsider g as XFinSequence of D by Def7;

        (f ^ g) is XFinSequence of D;

        hence thesis by Def7;

      end;

    end

    definition

      let D be set;

      let f,g be Element of (D ^omega );

      :: original: ^

      redefine

      func f ^ g -> Element of (D ^omega ) ;

      coherence

      proof

        reconsider f, g as XFinSequence of D by Def7;

        (f ^ g) is XFinSequence of D;

        hence thesis by Def7;

      end;

    end

    theorem :: AFINSQ_1:74

    

     Th71: p c= (p ^ q)

    proof

      

       A1: ( dom p) c= ( dom (p ^ q)) by Th19;

      for x be object st x in ( dom p) holds ((p ^ q) . x) = (p . x) by Def3;

      hence thesis by A1, GRFUNC_1: 2;

    end;

    theorem :: AFINSQ_1:75

    

     Th72: ( len (p ^ <%x%>)) = (( len p) + 1)

    proof

      

      thus ( len (p ^ <%x%>)) = (( len p) + ( len <%x%>)) by Def3

      .= (( len p) + 1) by Th30;

    end;

    theorem :: AFINSQ_1:76

     <%x, y%> = (( 0 ,1) --> (x,y))

    proof

      

       A1: ( dom <%x, y%>) = ( len <%x, y%>)

      .= { 0 , 1} by Th35, CARD_1: 50;

      

       A2: ( <%x, y%> . 0 ) = x;

      ( <%x, y%> . 1) = y;

      hence <%x, y%> = (( 0 ,1) --> (x,y)) by A1, A2, FUNCT_4: 66;

    end;

    reserve M for Nat;

    theorem :: AFINSQ_1:77

    

     Th74: (p ^ q) = (p +* ( Shift (q,( card p))))

    proof

      

       A1: ( dom ( Shift (q,( card p)))) = { (M + ( card p)) : M in ( dom q) } by VALUED_1:def 12;

      for x be object holds x in ( dom (p ^ q)) iff x in ( dom p) or x in ( dom ( Shift (q,( card p))))

      proof

        let x be object;

        thus x in ( dom (p ^ q)) implies x in ( dom p) or x in ( dom ( Shift (q,( card p))))

        proof

          assume

           A2: x in ( dom (p ^ q));

          then

          reconsider k = x as Nat;

          per cases by A2, Th18;

            suppose k in ( dom p);

            hence x in ( dom p) or x in ( dom ( Shift (q,( card p))));

          end;

            suppose ex n st n in ( dom q) & k = (( len p) + n);

            hence x in ( dom p) or x in ( dom ( Shift (q,( card p)))) by A1;

          end;

        end;

        assume

         A3: x in ( dom p) or x in ( dom ( Shift (q,( card p))));

        per cases by A3;

          suppose

           A4: x in ( dom p);

          ( dom p) c= ( dom (p ^ q)) by Th19;

          hence x in ( dom (p ^ q)) by A4;

        end;

          suppose x in ( dom ( Shift (q,( card p))));

          then ex M st x = (M + ( card p)) & M in ( dom q) by A1;

          hence x in ( dom (p ^ q)) by Th21;

        end;

      end;

      then

       A5: ( dom (p ^ q)) = (( dom p) \/ ( dom ( Shift (q,( card p))))) by XBOOLE_0:def 3;

      for x be object st x in (( dom p) \/ ( dom ( Shift (q,( card p))))) holds (x in ( dom ( Shift (q,( card p)))) implies ((p ^ q) . x) = (( Shift (q,( card p))) . x)) & ( not x in ( dom ( Shift (q,( card p)))) implies ((p ^ q) . x) = (p . x))

      proof

        let x be object such that

         A6: x in (( dom p) \/ ( dom ( Shift (q,( card p)))));

        hereby

          assume

           A7: x in ( dom ( Shift (q,( card p))));

          then

          reconsider k = x as Nat;

          consider M such that

           A8: x = (M + ( card p)) and

           A9: M in ( dom q) by A7, A1;

          set m = (k -' ( len p));

          

           A10: (( len p) + m) = k by A8, NAT_D: 34;

          

          hence ((p ^ q) . x) = (q . m) by A8, A9, Def3

          .= (( Shift (q,( card p))) . x) by A8, A9, A10, VALUED_1:def 12;

        end;

        assume not x in ( dom ( Shift (q,( card p))));

        then x in ( dom p) by A6, XBOOLE_0:def 3;

        hence ((p ^ q) . x) = (p . x) by Def3;

      end;

      hence (p ^ q) = (p +* ( Shift (q,( card p)))) by A5, FUNCT_4:def 1;

    end;

    theorem :: AFINSQ_1:78

    (p +* (p ^ q)) = (p ^ q) & ((p ^ q) +* p) = (p ^ q) by Th71, FUNCT_4: 97, FUNCT_4: 98;

    reserve m,n for Nat;

    theorem :: AFINSQ_1:79

    

     Th76: for I be finite initial NAT -defined Function, J be Function holds ( dom ( Shift (I,n))) misses ( dom ( Shift (J,(n + ( card I)))))

    proof

      let I be finite initial NAT -defined Function, J be Function;

      assume

       A1: ( dom ( Shift (I,n))) meets ( dom ( Shift (J,(n + ( card I)))));

      ( dom ( Shift (J,(n + ( card I))))) = { (l + (n + ( card I))) : l in ( dom J) } by VALUED_1:def 12;

      then

      consider x be object such that

       A2: x in ( dom ( Shift (I,n))) and

       A3: x in { (l + (n + ( card I))) : l in ( dom J) } by A1, XBOOLE_0: 3;

      ( dom ( Shift (I,n))) = { (m + n) : m in ( dom I) } by VALUED_1:def 12;

      then

      consider m such that

       A4: x = (m + n) and

       A5: m in ( dom I) by A2;

      consider l such that

       A6: x = (l + (n + ( card I))) and l in ( dom J) by A3;

      m < ( card I) by A5, Lm1;

      hence contradiction by NAT_1: 11, A4, A6, XREAL_1: 6;

    end;

    theorem :: AFINSQ_1:80

    

     Th77: ( Shift (p,n)) c= ( Shift ((p ^ q),n))

    proof

      (p ^ q) = (p +* ( Shift (q,( card p)))) by Th74;

      then

       A1: ( Shift ((p ^ q),n)) = (( Shift (p,n)) +* ( Shift (( Shift (q,( card p))),n))) by VALUED_1: 23;

      ( Shift (( Shift (q,( card p))),n)) = ( Shift (q,(n + ( card p)))) by VALUED_1: 21;

      then ( dom ( Shift (p,n))) misses ( dom ( Shift (( Shift (q,( card p))),n))) by Th76;

      hence ( Shift (p,n)) c= ( Shift ((p ^ q),n)) by A1, FUNCT_4: 32;

    end;

    theorem :: AFINSQ_1:81

    

     Th78: ( Shift (q,(n + ( card p)))) c= ( Shift ((p ^ q),n))

    proof

      

       A1: ( Shift (( Shift (q,( card p))),n)) = ( Shift (q,(n + ( card p)))) by VALUED_1: 21;

      (p ^ q) = (p +* ( Shift (q,( card p)))) by Th74;

      then ( Shift ((p ^ q),n)) = (( Shift (p,n)) +* ( Shift (( Shift (q,( card p))),n))) by VALUED_1: 23;

      hence thesis by A1, FUNCT_4: 25;

    end;

    theorem :: AFINSQ_1:82

    ( Shift ((p ^ q),n)) c= X implies ( Shift (p,n)) c= X

    proof

      assume

       A1: ( Shift ((p ^ q),n)) c= X;

      ( Shift (p,n)) c= ( Shift ((p ^ q),n)) by Th77;

      hence ( Shift (p,n)) c= X by A1;

    end;

    theorem :: AFINSQ_1:83

    ( Shift ((p ^ q),n)) c= X implies ( Shift (q,(n + ( card p)))) c= X

    proof

      assume

       A1: ( Shift ((p ^ q),n)) c= X;

      ( Shift (q,(n + ( card p)))) c= ( Shift ((p ^ q),n)) by Th78;

      hence thesis by A1;

    end;

    registration

      let F be initial non empty NAT -defined finite Function;

      cluster ( CutLastLoc F) -> initial;

      coherence ;

    end

    definition

      let x1,x2,x3,x4 be object;

      :: AFINSQ_1:def14

      func <%x1,x2,x3,x4%> -> set equals ((( <%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>);

      coherence ;

    end

    registration

      let x1,x2,x3,x4 be object;

      cluster <%x1, x2, x3, x4%> -> Function-like Relation-like;

      coherence ;

    end

    registration

      let x1,x2,x3,x4 be object;

      cluster <%x1, x2, x3, x4%> -> finite Sequence-like;

      coherence ;

    end

    reserve x1,x2,x3,x4 for object;

    theorem :: AFINSQ_1:84

    ( len <%x1, x2, x3, x4%>) = 4

    proof

      

      thus ( len <%x1, x2, x3, x4%>) = (( len <%x1, x2, x3%>) + 1) by Th72

      .= (3 + 1) by Th36

      .= 4;

    end;

    

     Lm3: ( <%x1, x2, x3, x4%> . 1) = x2 & ( <%x1, x2, x3, x4%> . 2) = x3 & ( <%x1, x2, x3, x4%> . 3) = x4

    proof

      

       A1: ( len <%x1, x2, x3%>) = 3 by Th36;

      then

       A2: 1 in ( dom <%x1, x2, x3%>) by Lm1;

      

      thus ( <%x1, x2, x3, x4%> . 1) = ( <%x1, x2, x3%> . 1) by A2, Def3

      .= x2;

      

       A3: 2 in ( dom <%x1, x2, x3%>) by A1, Lm1;

      

      thus ( <%x1, x2, x3, x4%> . 2) = ( <%x1, x2, x3%> . 2) by A3, Def3

      .= x3;

      thus ( <%x1, x2, x3, x4%> . 3) = x4 by A1, Th33;

    end;

    registration

      let x1,x2,x3,x4 be object;

      reduce ( <%x1, x2, x3, x4%> . 0 ) to x1;

      reducibility

      proof

        

        thus ( <%x1, x2, x3, x4%> . 0 ) = ((( <%x1%> ^ <%x2, x3%>) ^ <%x4%>) . 0 ) by Th25

        .= (( <%x1%> ^ <%x2, x3, x4%>) . 0 ) by Th25

        .= x1 by Th32;

      end;

      reduce ( <%x1, x2, x3, x4%> . 1) to x2;

      reducibility by Lm3;

      reduce ( <%x1, x2, x3, x4%> . 2) to x3;

      reducibility by Lm3;

      reduce ( <%x1, x2, x3, x4%> . 3) to x4;

      reducibility by Lm3;

    end

    ::$Canceled

    theorem :: AFINSQ_1:86

    k < ( len p) iff k in ( dom p) by Lm1;

    reserve e,u for object;

    theorem :: AFINSQ_1:87

    (( Segm (n + 1)) --> e) = ((( Segm n) --> e) ^ <%e%>)

    proof

      set p = (( Segm n) --> e), q = (( Segm (n + 1)) --> e);

      

       A2: ( dom q) = (n + 1)

      .= (( len p) + ( len <%e%>)) by Th31;

      

       A3: for k st k in ( dom p) holds (q . k) = (p . k)

      proof

        let k;

        assume

         A4: k in ( dom p);

        p c= q by FUNCT_4: 4, NAT_1: 63;

        hence (q . k) = (p . k) by A4, GRFUNC_1: 2;

      end;

      for k st k in ( dom <%e%>) holds (q . (( len p) + k)) = ( <%e%> . k)

      proof

        let k such that

         A5: k in ( dom <%e%>);

        

         A6: k = 0 by A5, TARSKI:def 1;

        ( len p) < (n + 1) by NAT_1: 13;

        then (( len p) + 0 ) in ( Segm (n + 1)) by NAT_1: 44;

        hence (q . (( len p) + k)) = ( <%e%> . k) by A6, FUNCOP_1: 7;

      end;

      hence thesis by A2, A3, Def3;

    end;

    theorem :: AFINSQ_1:88

    

     Th84: ( dom ( Shift ( <%e%>,( card p)))) = {( card p)}

    proof

      for u holds u in ( dom ( Shift ( <%e%>,( card p)))) iff u = ( card p)

      proof

        let u;

        thus u in ( dom ( Shift ( <%e%>,( card p)))) implies u = ( card p)

        proof

          assume u in ( dom ( Shift ( <%e%>,( card p))));

          then u in { (m + ( card p)) where m be Nat : m in ( dom <%e%>) } by VALUED_1:def 12;

          then

          consider m be Nat such that

           A1: u = (m + ( card p)) and

           A2: m in ( dom <%e%>);

          m = 0 by A2, TARSKI:def 1;

          hence u = ( card p) by A1;

        end;

         0 in 1 by CARD_1: 49, TARSKI:def 1;

        then 0 in ( dom <%e%>) by Def4;

        then ( 0 + ( card p)) in ( dom ( Shift ( <%e%>,( card p)))) by VALUED_1: 24;

        hence thesis;

      end;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: AFINSQ_1:89

    ( dom (p ^ <%e%>)) = (( dom p) \/ {( card p)})

    proof

      

      thus ( dom (p ^ <%e%>)) = ( dom (p +* ( Shift ( <%e%>,( card p))))) by Th74

      .= (( dom p) \/ ( dom ( Shift ( <%e%>,( card p))))) by FUNCT_4:def 1

      .= (( dom p) \/ {( card p)}) by Th84;

    end;

    theorem :: AFINSQ_1:90

    ( <%x%> +~ (x,y)) = <%y%>

    proof

      

       A1: ( dom ( <%x%> +~ (x,y))) = ( dom <%x%>) by FUNCT_4: 99

      .= ( Segm 1) by Th30;

      then ( <%x%> +~ (x,y)) is finite by FINSET_1: 10;

      then

      reconsider p = ( <%x%> +~ (x,y)) as XFinSequence by A1, ORDINAL1:def 7;

      

       A2: ( rng <%x%>) = {x} by Th30;

      then ( rng p) c= (( {x} \ {x}) \/ {y}) by FUNCT_4: 104;

      then ( rng p) c= ( {} \/ {y}) by XBOOLE_1: 37;

      then

       A3: ( rng p) c= {y};

      x in ( rng <%x%>) by A2, TARSKI:def 1;

      then y in ( rng p) by FUNCT_4: 101;

      hence ( <%x%> +~ (x,y)) = <%y%> by A1, Th30, A3, ZFMISC_1: 33;

    end;

    theorem :: AFINSQ_1:91

    for I be non empty XFinSequence holds ( LastLoc I) = (( card I) - 1)

    proof

      let I be non empty XFinSequence;

      

       A1: ( card I) >= ( 0 + 1) by NAT_1: 13;

      

      thus ( LastLoc I) = (( card I) -' 1) by Th67

      .= (( card I) - 1) by A1, XREAL_1: 233;

    end;

    begin

    theorem :: AFINSQ_1:92

    for p be XFinSequence, x be object holds ( last (p ^ <%x%>)) = x

    proof

      let p be XFinSequence, x be object;

      ( dom (p ^ <%x%>)) = ( len (p ^ <%x%>))

      .= (( len p) + 1) by Th72

      .= (( len p) +^ 1) by CARD_2: 36

      .= ( succ ( len p)) by ORDINAL2: 31;

      

      hence ( last (p ^ <%x%>)) = ((p ^ <%x%>) . ( len p)) by ORDINAL2: 6

      .= x by Th33;

    end;

    theorem :: AFINSQ_1:93

    

     Th12: for D be set, p be XFinSequence of D holds ( FS2XFS ( XFS2FS p)) = p

    proof

      let D be set, p be XFinSequence of D;

      

       A1: ( len p) = ( len ( XFS2FS p)) by Def9A;

      

       A2: ( len ( XFS2FS p)) = ( len ( FS2XFS ( XFS2FS p))) by Def8;

      for k be Nat st k < ( len p) holds (p . k) = (( FS2XFS ( XFS2FS p)) . k)

      proof

        let k be Nat;

        assume

         A3: k < ( len p);

        then ( 0 + 1) <= (k + 1) & (k + 1) < (( len p) + 1) by XREAL_1: 6;

        then

         A4: 1 <= (k + 1) & (k + 1) <= ( len p) by NAT_1: 13;

        

        thus (p . k) = (p . ((k + 1) -' 1)) by NAT_D: 34

        .= (( XFS2FS p) . (k + 1)) by A4, Def9A

        .= (( FS2XFS ( XFS2FS p)) . k) by A1, A3, Def8;

      end;

      hence thesis by A1, A2, Th8;

    end;

    registration

      let D be set, f be XFinSequence of D;

      reduce ( FS2XFS ( XFS2FS f)) to f;

      reducibility by Th12;

    end

    theorem :: AFINSQ_1:94

    

     Th13: for D be set, p be FinSequence of D, n be Nat holds (n + 1) in ( dom p) iff n in ( dom ( FS2XFS p))

    proof

      let D be set, p be FinSequence of D, n be Nat;

      hereby

        assume (n + 1) in ( dom p);

        then (n + 1) <= ( len p) by FINSEQ_3: 25;

        then ((n + 1) - 1) < (( len p) - 0 ) by XREAL_1: 15;

        then n < ( len ( FS2XFS p)) by Def8;

        then n in ( Segm ( dom ( FS2XFS p))) by NAT_1: 44;

        hence n in ( dom ( FS2XFS p));

      end;

      assume n in ( dom ( FS2XFS p));

      then n in ( Segm ( dom ( FS2XFS p)));

      then 0 <= n & n < ( len ( FS2XFS p)) by NAT_1: 44;

      then ( 0 + 1) <= (n + 1) & n < ( len p) by Def8, XREAL_1: 6;

      then 1 <= (n + 1) & (n + 1) <= ( len p) by NAT_1: 13;

      hence (n + 1) in ( dom p) by FINSEQ_3: 25;

    end;

    theorem :: AFINSQ_1:95

    

     Th14: for D be set, p be XFinSequence of D, n be Nat holds n in ( dom p) iff (n + 1) in ( dom ( XFS2FS p))

    proof

      let D be set, p be XFinSequence of D, n be Nat;

      hereby

        assume n in ( dom p);

        then n in ( dom ( FS2XFS ( XFS2FS p)));

        hence (n + 1) in ( dom ( XFS2FS p)) by Th13;

      end;

      assume (n + 1) in ( dom ( XFS2FS p));

      then n in ( dom ( FS2XFS ( XFS2FS p))) by Th13;

      hence thesis;

    end;

    registration

      let D be set, p be one-to-one FinSequence of D;

      cluster ( FS2XFS p) -> one-to-one;

      coherence

      proof

        now

          let x1,x2 be object;

          assume that

           A1: x1 in ( dom ( FS2XFS p)) & x2 in ( dom ( FS2XFS p)) and

           A2: (( FS2XFS p) . x1) = (( FS2XFS p) . x2);

          reconsider n1 = x1, n2 = x2 as Nat by A1;

          

           A3: (n1 + 1) in ( dom p) & (n2 + 1) in ( dom p) by A1, Th13;

          then (n1 + 1) <= ( len p) & (n2 + 1) <= ( len p) by FINSEQ_3: 25;

          then

           A4: n1 < ( len p) & n2 < ( len p) by NAT_1: 13;

          (p . (n1 + 1)) = (( FS2XFS p) . n1) by A4, Def8

          .= (p . (n2 + 1)) by A2, A4, Def8;

          then (n1 + 1) = (n2 + 1) by A3, FUNCT_1:def 4;

          hence x1 = x2;

        end;

        hence thesis;

      end;

    end

    registration

      let D be set, p be one-to-one XFinSequence of D;

      cluster ( XFS2FS p) -> one-to-one;

      coherence

      proof

        now

          let x1,x2 be object;

          assume that

           A1: x1 in ( dom ( XFS2FS p)) & x2 in ( dom ( XFS2FS p)) and

           A2: (( XFS2FS p) . x1) = (( XFS2FS p) . x2);

          reconsider n1 = x1, n2 = x2 as Nat by A1;

          1 <= n1 & n1 <= ( len ( XFS2FS p)) & 1 <= n2 & n2 <= ( len ( XFS2FS p)) by A1, FINSEQ_3: 25;

          then

           A3: 1 <= n1 & n1 <= ( len p) & 1 <= n2 & n2 <= ( len p) by Def9A;

          then

           A4: (p . (n1 -' 1)) = (( XFS2FS p) . n1) & (p . (n2 -' 1)) = (( XFS2FS p) . n2) by Def9A;

          

           A5: ((n1 -' 1) + 1) = n1 & ((n2 -' 1) + 1) = n2 by A3, XREAL_1: 235;

          then (n1 -' 1) in ( dom p) & (n2 -' 1) in ( dom p) by A1, Th14;

          hence x1 = x2 by A2, A4, A5, FUNCT_1:def 4;

        end;

        hence thesis;

      end;

    end

    theorem :: AFINSQ_1:96

    

     Th15: for D be set, p be FinSequence of D holds ( rng p) = ( rng ( FS2XFS p))

    proof

      let D be set, p be FinSequence of D;

      for y be object holds y in ( rng ( FS2XFS p)) iff ex x be object st x in ( dom p) & (p . x) = y

      proof

        let y be object;

        thus y in ( rng ( FS2XFS p)) implies ex x be object st x in ( dom p) & (p . x) = y

        proof

          assume y in ( rng ( FS2XFS p));

          then

          consider n be object such that

           A1: n in ( dom ( FS2XFS p)) & (( FS2XFS p) . n) = y by FUNCT_1:def 3;

          reconsider n as Nat by A1;

          take (n + 1);

          thus (n + 1) in ( dom p) by A1, Th13;

          n < ( len ( FS2XFS p)) by A1, Lm1;

          then n < ( len p) by Def8;

          hence (p . (n + 1)) = y by A1, Def8;

        end;

        given x be object such that

         A2: x in ( dom p) & (p . x) = y;

        reconsider n1 = x as Nat by A2;

        

         A3: 1 <= n1 & n1 <= ( len p) by A2, FINSEQ_3: 25;

        then

        reconsider n = (n1 - 1) as Nat by Th0;

        n < (( len p) - 0 ) by A3, XREAL_1: 15;

        then

         A4: (p . (n + 1)) = (( FS2XFS p) . n) by Def8;

        (n + 1) in ( dom p) by A2;

        then n in ( dom ( FS2XFS p)) by Th13;

        hence thesis by A2, A4, FUNCT_1: 3;

      end;

      hence thesis by FUNCT_1:def 3;

    end;

    theorem :: AFINSQ_1:97

    for D be set, p be XFinSequence of D holds ( rng p) = ( rng ( XFS2FS p))

    proof

      let D be set, p be XFinSequence of D;

      

      thus ( rng p) = ( rng ( FS2XFS ( XFS2FS p)))

      .= ( rng ( XFS2FS p)) by Th15;

    end;

    registration

      let D be set, p be empty XFinSequence of D;

      cluster ( XFS2FS p) -> empty;

      coherence

      proof

        ( len p) = {} ;

        then ( len ( XFS2FS p)) = {} by Def9A;

        hence thesis;

      end;

    end

    registration

      let D be set, p be empty FinSequence of D;

      cluster ( FS2XFS p) -> empty;

      coherence

      proof

        ( len p) = {} ;

        then ( len ( FS2XFS p)) = {} by Def8;

        hence thesis;

      end;

    end