afinsq_2.miz



    begin

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

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

X,Y,D for set,

p,q for XFinSequence;

    

     Lm1: for X,Y be finite set, F be Function of X, Y st ( card X) = ( card Y) holds F is onto iff F is one-to-one

    proof

      let X,Y be finite set, F be Function of X, Y such that

       A1: ( card X) = ( card Y);

      thus F is onto implies F is one-to-one

      proof

        assume

         A2: F is onto;

        assume not F is one-to-one;

        then

        consider x1,x2 be object such that

         A3: x1 in ( dom F) and

         A4: x2 in ( dom F) and

         A5: (F . x1) = (F . x2) and

         A6: x1 <> x2;

        reconsider Xx = (X \ {x1}) as finite set;

        Y c= (F .: Xx)

        proof

          let Fy be object;

          assume Fy in Y;

          then Fy in ( rng F) by A2, FUNCT_2:def 3;

          then

          consider y be object such that

           A7: y in ( dom F) and

           A8: (F . y) = Fy by FUNCT_1:def 3;

          now

            per cases ;

              suppose

               A9: y = x1;

              x2 in Xx by A4, A6, ZFMISC_1: 56;

              hence thesis by A4, A5, A8, A9, FUNCT_1:def 6;

            end;

              suppose y <> x1;

              then y in Xx by A7, ZFMISC_1: 56;

              hence thesis by A7, A8, FUNCT_1:def 6;

            end;

          end;

          hence thesis;

        end;

        then

         A10: ( Segm ( card Y)) c= ( Segm ( card Xx)) by CARD_1: 66;

         {x1} meets X by A3, ZFMISC_1: 48;

        then

         A11: Xx <> X by XBOOLE_1: 83;

        Xx c< X by A11;

        hence thesis by A1, A10, NAT_1: 39, CARD_2: 48;

      end;

      thus F is one-to-one implies F is onto

      proof

        assume F is one-to-one;

        then

         A12: ( card ( dom F)) = ( card (F .: ( dom F))) by CARD_1: 5, CARD_1: 33;

        assume not F is onto;

        then not ( rng F) = Y by FUNCT_2:def 3;

        then not Y c= ( rng F);

        then

        consider y be object such that

         A13: y in Y and

         A14: not y in ( rng F);

        

         A15: ( card ( rng F)) <= ( card (Y \ {y})) by A14, NAT_1: 43, ZFMISC_1: 34;

        

         A16: (F .: ( dom F)) = ( rng F) by RELAT_1: 113;

         {y} meets Y by A13, ZFMISC_1: 48;

        then

         A17: (Y \ {y}) <> Y by XBOOLE_1: 83;

        (Y \ {y}) c< Y by A17;

        then ( card (Y \ {y})) < ( card Y) by CARD_2: 48;

        hence thesis by A1, A13, A15, A12, A16, FUNCT_2:def 1;

      end;

    end;

    theorem :: AFINSQ_2:1

    

     Th1: x in i implies x is Element of NAT

    proof

      i c= NAT ;

      hence thesis;

    end;

    begin

    theorem :: AFINSQ_2:2

    

     Th2: for X0 be finite natural-membered set holds ex n st X0 c= ( Segm n)

    proof

      let X0 be finite natural-membered set;

      consider p be Function such that

       A1: ( rng p) = X0 and

       A2: ( dom p) in NAT by FINSET_1:def 1;

      reconsider np = ( dom p) as Element of NAT by A2;

      np = ( dom p);

      then

      reconsider p as XFinSequence by AFINSQ_1: 5;

      X0 c= NAT by MEMBERED: 6;

      then

      reconsider p as XFinSequence of NAT by A1, RELAT_1:def 19;

      defpred P[ Nat] means ex n st for i st i in ( Segm $1) & ($1 -' 1) in ( dom p) holds (p . i) in n;

      

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

      proof

        let k;

        assume P[k];

        then

        consider n such that

         A4: for i st i in k & (k -' 1) in ( dom p) holds (p . i) in n;

        per cases ;

          suppose

           A5: ((k + 1) - 1) < ( len p);

          set m = (p . k);

          set m2 = ( max (n,(m + 1)));

          (k -' 1) <= k by NAT_D: 35;

          then (k -' 1) < ( len p) by A5, XXREAL_0: 2;

          then

           A6: (k -' 1) in ( dom p) by AFINSQ_1: 86;

          for i st i in ( Segm (k + 1)) & ((k + 1) -' 1) in ( dom p) holds (p . i) in ( Segm m2)

          proof

            let i;

            assume that

             A7: i in ( Segm (k + 1)) and ((k + 1) -' 1) in ( dom p);

            

             A8: i < (k + 1) by A7, NAT_1: 44;

            per cases ;

              suppose

               A9: i < k;

              set k0 = (p . i);

              i in ( Segm k) by A9, NAT_1: 44;

              then (p . i) in ( Segm n) by A4, A6;

              then k0 < n by NAT_1: 44;

              hence thesis by NAT_1: 44, XXREAL_0: 30;

            end;

              suppose

               A10: i >= k;

              m < (m + 1) by XREAL_1: 29;

              then

               A11: m < m2 by XXREAL_0: 30;

              i <= k by A8, NAT_1: 13;

              then (p . i) = m by A10, XXREAL_0: 1;

              hence thesis by A11, NAT_1: 44;

            end;

          end;

          hence thesis;

        end;

          suppose

           A12: ((k + 1) - 1) >= ( len p);

          ((k + 1) -' 1) = k by NAT_D: 34;

          then for i st i in (k + 1) & ((k + 1) -' 1) in ( dom p) holds (p . i) in 2 by A12, AFINSQ_1: 86;

          hence thesis;

        end;

      end;

      for i st i in 0 & ( 0 -' 1) in ( dom p) holds (p . i) in 0 ;

      then

       A13: P[ 0 ];

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

      then

      consider n such that

       A14: for i st i in ( Segm ( len p)) & (( len p) -' 1) in ( dom p) holds (p . i) in n;

      ( rng p) c= ( Segm n)

      proof

        let y be object;

        assume y in ( rng p);

        then

        consider x be object such that

         A15: x in ( dom p) and

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

        

         A17: (( len p) - 1) < ( len p) by XREAL_1: 44;

         0 < ( len p) by A15;

        then ( 0 qua Element of NAT + 1) <= ( len p) by NAT_1: 13;

        then (( len p) -' 1) = (( len p) - 1) by XREAL_1: 233;

        then (( len p) -' 1) in ( dom p) by A17, AFINSQ_1: 86;

        hence thesis by A14, A15, A16;

      end;

      hence thesis by A1;

    end;

    theorem :: AFINSQ_2:3

    

     Th3: x in ( rng p) implies ex i be Element of NAT st i in ( dom p) & (p . i) = x

    proof

      assume x in ( rng p);

      then ex a be object st a in ( dom p) & x = (p . a) by FUNCT_1:def 3;

      hence thesis;

    end;

    theorem :: AFINSQ_2:4

    

     Th4: for p st for i st i in ( dom p) holds (p . i) in D holds p is XFinSequence of D

    proof

      let p;

      assume

       A1: for i st i in ( dom p) holds (p . i) in D;

      ( rng p) c= D

      proof

        let x be object;

        assume x in ( rng p);

        then ex i be Element of NAT st i in ( dom p) & (p . i) = x by Th3;

        hence thesis by A1;

      end;

      hence thesis by RELAT_1:def 19;

    end;

    scheme :: AFINSQ_2:sch1

    XSeqLambdaD { i() -> Nat , D() -> non empty set , F( set) -> Element of D() } :

ex p be XFinSequence of D() st ( len p) = i() & for j st j in i() holds (p . j) = F(j);

      consider z be XFinSequence such that

       A1: ( len z) = i() and

       A2: for i st i in i() holds (z . i) = F(i) from AFINSQ_1:sch 2;

      for j be Nat st j in i() holds (z . j) in D()

      proof

        let j be Nat;

        reconsider j0 = j as Element of NAT by ORDINAL1:def 12;

        assume j in i();

        then (z . j0) = F(j0) by A2;

        hence thesis;

      end;

      then

      reconsider z as XFinSequence of D() by A1, Th4;

      take z;

      thus ( len z) = i() by A1;

      let j be Nat;

      thus thesis by A2;

    end;

    registration

      cluster empty natural-valued for XFinSequence;

      existence

      proof

        take the empty XFinSequence of NAT ;

        thus thesis;

      end;

      let p be complex-valued Sequence-like Function;

      cluster ( - p) -> Sequence-like;

      coherence

      proof

        ( dom p) = ( dom ( - p)) & ( dom p) is ordinal by VALUED_1: 8;

        hence thesis;

      end;

      cluster (p " ) -> Sequence-like;

      coherence

      proof

        ( dom p) = ( dom (p " )) by VALUED_1:def 7;

        hence thesis;

      end;

      cluster (p ^2 ) -> Sequence-like;

      coherence

      proof

        ( dom p) = ( dom (p ^2 )) by VALUED_1: 11;

        hence thesis;

      end;

      cluster ( abs p) -> Sequence-like;

      coherence

      proof

        ( dom p) = ( dom ( abs p)) by VALUED_1:def 11;

        hence thesis;

      end;

      let q be complex-valued Sequence-like Function;

      cluster (p + q) -> Sequence-like;

      coherence

      proof

        ( dom (p + q)) = (( dom p) /\ ( dom q)) & ( dom p) is ordinal & ( dom q) is ordinal by VALUED_1:def 1;

        hence thesis;

      end;

      cluster (p - q) -> Sequence-like;

      coherence ;

      cluster (p (#) q) -> Sequence-like;

      coherence

      proof

        ( dom (p (#) q)) = (( dom p) /\ ( dom q)) & ( dom p) is ordinal & ( dom q) is ordinal by VALUED_1:def 4;

        hence thesis;

      end;

      cluster (p /" q) -> Sequence-like;

      coherence ;

    end

    registration

      let p be complex-valued finite Function;

      cluster ( - p) -> finite;

      coherence

      proof

        ( dom p) = ( dom ( - p)) by VALUED_1: 8;

        hence thesis by FINSET_1: 10;

      end;

      cluster (p " ) -> finite;

      coherence

      proof

        ( dom p) = ( dom (p " )) by VALUED_1:def 7;

        hence thesis by FINSET_1: 10;

      end;

      cluster (p ^2 ) -> finite;

      coherence

      proof

        ( dom p) = ( dom (p ^2 )) by VALUED_1: 11;

        hence thesis by FINSET_1: 10;

      end;

      cluster ( abs p) -> finite;

      coherence

      proof

        ( dom p) = ( dom ( abs p)) by VALUED_1:def 11;

        hence thesis by FINSET_1: 10;

      end;

      let q be complex-valued Function;

      cluster (p + q) -> finite;

      coherence

      proof

        ( dom (p + q)) = (( dom p) /\ ( dom q)) by VALUED_1:def 1;

        hence thesis by FINSET_1: 10;

      end;

      cluster (p - q) -> finite;

      coherence ;

      cluster (p (#) q) -> finite;

      coherence

      proof

        ( dom (p (#) q)) = (( dom p) /\ ( dom q)) by VALUED_1:def 4;

        hence thesis by FINSET_1: 10;

      end;

      cluster (p /" q) -> finite;

      coherence ;

      cluster (q /" p) -> finite;

      coherence ;

    end

    registration

      let p be complex-valued Sequence-like Function;

      let c be Complex;

      cluster (c + p) -> Sequence-like;

      coherence

      proof

        ( dom p) = ( dom (c + p)) by VALUED_1:def 2;

        hence thesis;

      end;

      cluster (p - c) -> Sequence-like;

      coherence ;

      cluster (c (#) p) -> Sequence-like;

      coherence

      proof

        ( dom p) = ( dom (c (#) p)) by VALUED_1:def 5;

        hence thesis;

      end;

    end

    registration

      let p be complex-valued finite Function;

      let c be Complex;

      cluster (c + p) -> finite;

      coherence

      proof

        ( dom p) = ( dom (c + p)) by VALUED_1:def 2;

        hence thesis by FINSET_1: 10;

      end;

      cluster (p - c) -> finite;

      coherence ;

      cluster (c (#) p) -> finite;

      coherence

      proof

        ( dom p) = ( dom (c (#) p)) by VALUED_1:def 5;

        hence thesis by FINSET_1: 10;

      end;

    end

    definition

      let p;

      :: AFINSQ_2:def1

      func Rev p -> XFinSequence means

      : Def1: ( len it ) = ( len p) & for i st i in ( dom it ) holds (it . i) = (p . (( len p) - (i + 1)));

      existence

      proof

        deffunc F( Nat) = (p . (( len p) - ($1 + 1)));

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

        hence thesis;

      end;

      uniqueness

      proof

        let f1,f2 be XFinSequence such that

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

         A2: for i st i in ( dom f1) holds (f1 . i) = (p . (( len p) - (i + 1))) and

         A3: ( len f2) = ( len p) and

         A4: for i st i in ( dom f2) holds (f2 . i) = (p . (( len p) - (i + 1)));

        now

          let i;

          assume

           A5: i in ( dom p);

          then (f1 . i) = (p . (( len p) - (i + 1))) by A1, A2;

          hence (f1 . i) = (f2 . i) by A3, A4, A5;

        end;

        hence thesis by A1, A3;

      end;

    end

    theorem :: AFINSQ_2:5

    

     Th5: ( dom p) = ( dom ( Rev p)) & ( rng p) = ( rng ( Rev p))

    proof

      

      thus

       A1: ( dom p) = ( len p)

      .= ( len ( Rev p)) by Def1

      .= ( dom ( Rev p));

      

       A2: ( len p) = ( len ( Rev p)) by Def1;

      hereby

        let x be object;

        assume x in ( rng p);

        then

        consider z be object such that

         A3: z in ( dom p) and

         A4: (p . z) = x by FUNCT_1:def 3;

        reconsider i = z as Element of NAT by A3;

        (i + 1) <= ( len p) by NAT_1: 13, A3, AFINSQ_1: 86;

        then (( len p) -' (i + 1)) = (( len p) - (i + 1)) by XREAL_1: 233;

        then

        reconsider j = (( len p) - (i + 1)) as Element of NAT ;

        

         A5: j in ( len ( Rev p)) by A2, AFINSQ_1: 86, XREAL_1: 44;

        then (( Rev p) . j) = (p . (( len p) - (j + 1))) by Def1;

        hence x in ( rng ( Rev p)) by A4, A5, FUNCT_1:def 3;

      end;

      let x be object;

      assume x in ( rng ( Rev p));

      then

      consider z be object such that

       A6: z in ( dom ( Rev p)) and

       A7: (( Rev p) . z) = x by FUNCT_1:def 3;

      reconsider i = z as Element of NAT by A6;

      i < ( len p) by A2, A6, AFINSQ_1: 86;

      then (i + 1) <= ( len p) by NAT_1: 13;

      then (( len p) -' (i + 1)) = (( len p) - (i + 1)) by XREAL_1: 233;

      then

      reconsider j = (( len p) - (i + 1)) as Element of NAT ;

      (( len p) - (i + 1)) < ( len p) by XREAL_1: 44;

      then

       A8: j in ( len ( Rev p)) by A2, AFINSQ_1: 86;

      (( Rev p) . i) = (p . (( len p) - (i + 1))) by A6, Def1;

      hence thesis by A1, A7, A8, FUNCT_1:def 3;

    end;

    registration

      let D be set, f be XFinSequence of D;

      cluster ( Rev f) -> D -valued;

      coherence

      proof

        ( rng f) = ( rng ( Rev f)) by Th5;

        hence thesis by RELAT_1:def 19;

      end;

    end

    definition

      let p, n;

      :: AFINSQ_2:def2

      func p /^ n -> XFinSequence means

      : Def2: ( len it ) = (( len p) -' n) & for m st m in ( dom it ) holds (it . m) = (p . (m + n));

      existence

      proof

        thus ex p1 be XFinSequence st ( len p1) = (( len p) -' n) & for m st m in ( dom p1) holds (p1 . m) = (p . (m + n))

        proof

          deffunc F( Nat) = (p . ($1 + n));

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

          consider q such that

           A1: ( len q) = k & for m2 be Nat st m2 in k holds (q . m2) = F(m2) from AFINSQ_1:sch 2;

          take q;

          thus thesis by A1;

        end;

      end;

      uniqueness

      proof

        let p1,p2 be XFinSequence;

        thus (( len p1) = (( len p) -' n) & for m be Nat st m in ( dom p1) holds (p1 . m) = (p . (m + n))) & (( len p2) = (( len p) -' n) & for m be Nat st m in ( dom p2) holds (p2 . m) = (p . (m + n))) implies p1 = p2

        proof

          assume that

           A2: ( len p1) = (( len p) -' n) and

           A3: for m st m in ( dom p1) holds (p1 . m) = (p . (m + n)) and

           A4: ( len p2) = (( len p) -' n) and

           A5: for m st m in ( dom p2) holds (p2 . m) = (p . (m + n));

          now

            let m;

            assume

             A6: m in ( dom p1);

            then (p1 . m) = (p . (m + n)) by A3;

            hence (p1 . m) = (p2 . m) by A2, A4, A5, A6;

          end;

          hence thesis by A2, A4;

        end;

      end;

    end

    theorem :: AFINSQ_2:6

    

     Th6: n >= ( len p) implies (p /^ n) = {}

    proof

      assume n >= ( len p);

      then (( len p) -' n) = 0 by NAT_2: 8;

      then ( len (p /^ n)) = 0 by Def2;

      hence thesis;

    end;

    theorem :: AFINSQ_2:7

    

     Th7: n < ( len p) implies ( len (p /^ n)) = (( len p) - n)

    proof

      assume n < ( len p);

      then (( len p) -' n) = (( len p) - n) by XREAL_0:def 2, XREAL_1: 48;

      hence thesis by Def2;

    end;

    theorem :: AFINSQ_2:8

    

     Th8: (m + n) < ( len p) implies ((p /^ n) . m) = (p . (m + n))

    proof

      assume

       A1: (m + n) < ( len p);

      then

       A2: m < (( len p) - n) by XREAL_1: 20;

      ( len (p /^ n)) = (( len p) - n) by A1, Th7, NAT_1: 12;

      hence thesis by Def2, A2, AFINSQ_1: 86;

    end;

    registration

      let f be one-to-one XFinSequence, n;

      cluster (f /^ n) -> one-to-one;

      coherence

      proof

        let x,y be object;

        assume that

         A1: x in ( dom (f /^ n)) and

         A2: y in ( dom (f /^ n)) and

         A3: ((f /^ n) . x) = ((f /^ n) . y);

        reconsider nx = x, ny = y as Nat by A1, A2;

        

         A4: nx < ( len (f /^ n)) by A1, AFINSQ_1: 86;

        

         A5: ( len (f /^ n)) = (( len f) -' n) by Def2;

        

         A6: ny < ( len (f /^ n)) by A2, AFINSQ_1: 86;

        per cases ;

          suppose n <= ( len f);

          then

           A7: (( len f) -' n) = (( len f) - n) by XREAL_1: 233;

          then

           A8: (nx + n) < ( len f) by A4, A5, XREAL_1: 20;

          then

           A9: (nx + n) in ( dom f) by AFINSQ_1: 86;

          

           A10: (ny + n) < ( len f) by A6, A5, A7, XREAL_1: 20;

          then

           A11: (ny + n) in ( dom f) by AFINSQ_1: 86;

          

           A12: ((f /^ n) . ny) = (f . (ny + n)) by A10, Th8;

          ((f /^ n) . nx) = (f . (nx + n)) by A8, Th8;

          then (nx + n) = (ny + n) by A3, A9, A12, A11, FUNCT_1:def 4;

          hence thesis;

        end;

          suppose n > ( len f);

          then (f /^ n) = {} by Th6;

          hence thesis by A1;

        end;

      end;

    end

    theorem :: AFINSQ_2:9

    

     Th9: ( rng (p /^ n)) c= ( rng p)

    proof

      thus ( rng (p /^ n)) c= ( rng p)

      proof

        let z be object;

        assume z in ( rng (p /^ n));

        then

        consider x be object such that

         A1: x in ( dom (p /^ n)) and

         A2: z = ((p /^ n) . x) by FUNCT_1:def 3;

        reconsider nx = x as Element of NAT by A1;

        nx < ( len (p /^ n)) by A1, AFINSQ_1: 86;

        then

         A3: nx < (( len p) -' n) by Def2;

        per cases ;

          suppose n < ( len p);

          then (( len p) -' n) = (( len p) - n) by XREAL_1: 233;

          then

           A4: (nx + n) in ( dom p) by AFINSQ_1: 86, A3, XREAL_1: 20;

          ((p /^ n) . nx) = (p . (nx + n)) by A1, Def2;

          hence thesis by A2, A4, FUNCT_1:def 3;

        end;

          suppose n >= ( len p);

          then (p /^ n) = {} by Th6;

          hence thesis by A1;

        end;

      end;

    end;

    theorem :: AFINSQ_2:10

    

     Th10: (p /^ 0 ) = p

    proof

      per cases ;

        suppose

         A1: 0 < ( len p);

         A2:

        now

          let i;

          assume i < ( len (p /^ 0 ));

          

          hence ((p /^ 0 ) . i) = (p . (i + 0 qua Element of NAT )) by Def2, AFINSQ_1: 86

          .= (p . i);

        end;

        ( len (p /^ 0 )) = (( len p) - 0 ) by A1, Th7

        .= ( len p);

        hence thesis by A2, AFINSQ_1: 9;

      end;

        suppose

         A3: 0 >= ( len p);

        then (p /^ 0 ) = {} by Th6;

        hence thesis by A3;

      end;

    end;

    theorem :: AFINSQ_2:11

    

     Th11: ((p ^ q) /^ (( len p) + i)) = (q /^ i)

    proof

      

       A1: ( len (p ^ q)) = (( len p) + ( len q)) by AFINSQ_1: 17;

      per cases ;

        suppose

         A2: i < ( len q);

        then (( len p) + i) < (( len p) + ( len q)) by XREAL_1: 6;

        then (( len p) + i) < ( len (p ^ q)) by AFINSQ_1: 17;

        

        then

         A3: ( len ((p ^ q) /^ (( len p) + i))) = (( len (p ^ q)) - (( len p) + i)) by Th7

        .= ((( len q) + ( len p)) - (( len p) + i)) by AFINSQ_1: 17

        .= (( len q) - i)

        .= ( len (q /^ i)) by A2, Th7;

        now

          let k;

          assume

           A4: k < ( len (q /^ i));

          then

           A5: k in ( dom (q /^ i)) by AFINSQ_1: 86;

          k < (( len q) - i) by A2, A4, Th7;

          then

           A6: (i + k) in ( dom q) by AFINSQ_1: 86, XREAL_1: 20;

          k in ( dom ((p ^ q) /^ (( len p) + i))) by A3, A4, AFINSQ_1: 86;

          

          hence (((p ^ q) /^ (( len p) + i)) . k) = ((p ^ q) . ((( len p) + i) + k)) by Def2

          .= ((p ^ q) . (( len p) + (i + k)))

          .= (q . (i + k)) by A6, AFINSQ_1:def 3

          .= ((q /^ i) . k) by A5, Def2;

        end;

        hence thesis by A3, AFINSQ_1: 9;

      end;

        suppose

         A7: i >= ( len q);

        

        hence ((p ^ q) /^ (( len p) + i)) = {} by Th6, A1, XREAL_1: 6

        .= (q /^ i) by A7, Th6;

      end;

    end;

    theorem :: AFINSQ_2:12

    

     Th12: ((p ^ q) /^ ( len p)) = q

    proof

      

      thus ((p ^ q) /^ ( len p)) = ((p ^ q) /^ (( len p) + 0 qua Element of NAT ))

      .= (q /^ 0 ) by Th11

      .= q by Th10;

    end;

    theorem :: AFINSQ_2:13

    

     Th13: ((p | n) ^ (p /^ n)) = p

    proof

      set pn = (p /^ n);

      now

        per cases ;

          case

           A1: ( len p) <= n;

          (p /^ n) = {} by A1, Th6;

          hence thesis by A1, AFINSQ_1: 52;

        end;

          case

           A2: n < ( len p);

          set g = (p | n);

          

           A3: ( len g) = n by A2, AFINSQ_1: 54;

          

           A4: ( len pn) = (( len p) - n) by A2, Th7;

           A5:

          now

            let m;

            assume

             A6: m < ( len p);

            now

              per cases ;

                case m < n;

                then

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

                

                hence (((p | n) ^ (p /^ n)) . m) = ((p | n) . m) by A3, AFINSQ_1:def 3

                .= (p . m) by A2, A7, AFINSQ_1: 53;

              end;

                case n <= m;

                then ( max ( 0 ,(m - n))) = (m - n) by FINSEQ_2: 4;

                then

                reconsider k = (m - n) as Element of NAT by FINSEQ_2: 5;

                k < ( len pn) by A4, A6, XREAL_1: 9;

                then

                 A8: k in ( dom pn) by AFINSQ_1: 86;

                m = (( len (p | n)) + k) by A3;

                

                hence (((p | n) ^ (p /^ n)) . m) = (pn . k) by A8, AFINSQ_1:def 3

                .= (p . (k + n)) by A8, Def2

                .= (p . m);

              end;

            end;

            hence (((p | n) ^ (p /^ n)) . m) = (p . m);

          end;

          ( len (g ^ (p /^ n))) = (n + (( len p) - n)) by A4, A3, AFINSQ_1: 17

          .= ( len p);

          hence thesis by A5, AFINSQ_1: 9;

        end;

      end;

      hence thesis;

    end;

    registration

      let f be XFinSequence;

      cluster (f | 0 ) -> empty;

      coherence ;

      let n be Nat;

      cluster (f /^ (( dom f) + n)) -> empty;

      coherence

      proof

        ( len f) <= ((( len f) + n) + 0 ) by NAT_1: 11;

        then (( len f) - (( len f) + n)) <= 0 by XREAL_1: 20;

        then (( len f) -' (( len f) + n)) = 0 by XREAL_0:def 2;

        then ( len (f /^ (( dom f) + n))) = 0 by Def2;

        hence thesis;

      end;

      reduce (f | (( len f) + n)) to f;

      reducibility

      proof

        (( len f) + n) >= (( len f) + 0 ) by XREAL_1: 6;

        hence thesis by AFINSQ_1: 52;

      end;

      reduce ((f | n) ^ (f /^ n)) to f;

      reducibility by Th13;

    end

    registration

      let D be set, f be XFinSequence of D, n;

      cluster (f /^ n) -> D -valued;

      coherence

      proof

        deffunc F( Element of NAT ) = (f . ($1 + n));

        set p = (f /^ n);

        per cases ;

          suppose

           A1: n < ( len f);

          then

          reconsider k = (( len f) - n) as Nat by NAT_1: 21;

          

           A2: ( len p) = k by A1, Th7;

          

           A3: ( rng p) c= ( rng f)

          proof

            let x be object;

            assume x in ( rng p);

            then

            consider m be Element of NAT such that

             A4: m in ( dom p) and

             A5: (p . m) = x by Th3;

            (m + n) < (k + n) by A2, XREAL_1: 6, A4, AFINSQ_1: 86;

            then

             A6: (m + n) in ( dom f) by AFINSQ_1: 86;

            (p . m) = (f . (m + n)) by A4, Def2;

            hence thesis by A5, A6, FUNCT_1:def 3;

          end;

          for f2 be XFinSequence st ( rng f2) c= D holds f2 is XFinSequence of D by RELAT_1:def 19;

          hence thesis by A3, XBOOLE_1: 1;

        end;

          suppose ( len f) <= n;

          then (f /^ n) = ( <%> D) by Th6;

          hence thesis;

        end;

      end;

    end

    reserve k1,k2 for Nat;

    definition

      let p, k1, k2;

      :: AFINSQ_2:def3

      func mid (p,k1,k2) -> XFinSequence equals ((p | k2) /^ (k1 -' 1));

      coherence ;

    end

    theorem :: AFINSQ_2:14

    

     Th14: k1 > k2 implies ( mid (p,k1,k2)) = {}

    proof

      set k21 = k2;

      

       A1: ( len (p | k21)) <= k21 by AFINSQ_1: 55;

      assume

       A2: k1 > k2;

      then k1 >= ( 0 qua Nat + 1) by NAT_1: 13;

      then

       A3: (k1 -' 1) = (k1 - 1) by XREAL_1: 233;

      k1 >= (k2 + 1) by A2, NAT_1: 13;

      then (k1 - 1) >= ((k2 + 1) - 1) by XREAL_1: 9;

      hence thesis by A3, A1, Th6, XXREAL_0: 2;

    end;

    theorem :: AFINSQ_2:15

    1 <= k1 & k2 <= ( len p) implies ( mid (p,k1,k2)) = ((p /^ (k1 -' 1)) | ((k2 + 1) -' k1))

    proof

      assume that

       A1: 1 <= k1 and

       A2: k2 <= ( len p);

      set k11 = k1, k21 = k2;

      

       A3: ( len (p | k21)) = k21 by A2, AFINSQ_1: 54;

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

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

      then

       A4: (k1 -' 1) < k1 by A1, XREAL_1: 233;

      per cases ;

        suppose

         A5: k1 <= k2;

        

         A6: k2 < (k2 + 1) by XREAL_1: 29;

        

        then

         A7: ((k2 + 1) -' k1) = ((k2 + 1) - k1) by A5, XREAL_1: 233, XXREAL_0: 2

        .= (k2 - (k1 - 1));

        

         A8: (k11 -' 1) = (k11 - 1) by A1, XREAL_1: 233;

        (k11 - 1) < k11 by XREAL_1: 44;

        then (k11 - 1) < k21 by A5, XXREAL_0: 2;

        then

         A9: ( len ( mid (p,k1,k2))) = (k21 - (k11 - 1)) by A3, A8, Th7;

        then

         A10: ( len ( mid (p,k1,k2))) = ((k21 + 1) - k11);

        (k1 -' 1) < k2 by A4, A5, XXREAL_0: 2;

        then (k1 -' 1) < ( len p) by A2, XXREAL_0: 2;

        then ( len (p /^ (k1 -' 1))) = (( len p) - (k1 -' 1)) by Th7;

        then

         A11: ((k2 + 1) -' k1) <= ( len (p /^ (k1 -' 1))) by A2, A8, A7, XREAL_1: 9;

        

         A12: i < ( len ( mid (p,k1,k2))) implies (( mid (p,k1,k2)) . i) = (((p /^ (k1 -' 1)) | ((k2 + 1) -' k1)) . i)

        proof

          assume

           A13: i < ( len ( mid (p,k1,k2)));

          then

           A14: (i + (k11 -' 1)) in ( Segm k21) by NAT_1: 44, A8, A9, XREAL_1: 20;

          (i + (k1 -' 1)) < ((k21 - (k11 - 1)) + (k1 -' 1)) by A9, A13, XREAL_1: 6;

          then

           A15: (i + (k1 -' 1)) < ( len p) by A2, A8, XXREAL_0: 2;

          (i + (k11 - 1)) < k21 by A9, A13, XREAL_1: 20;

          then

           A16: (((p | k21) /^ (k11 -' 1)) . i) = ((p | k21) . (i + (k11 -' 1))) by A3, A8, Th8;

          i in ((k2 + 1) -' k1) by A7, A9, A13, AFINSQ_1: 86;

          

          then (((p /^ (k1 -' 1)) | ((k2 + 1) -' k1)) . i) = ((p /^ (k1 -' 1)) . i) by A11, AFINSQ_1: 53

          .= (p . (i + (k1 -' 1))) by A15, Th8;

          hence thesis by A2, A16, A14, AFINSQ_1: 53;

        end;

        ( len ((p /^ (k1 -' 1)) | ((k2 + 1) -' k1))) = ((k2 + 1) -' k1) by A11, AFINSQ_1: 54;

        then ( len ( mid (p,k1,k2))) = ( len ((p /^ (k1 -' 1)) | ((k2 + 1) -' k1))) by A5, A6, A10, XREAL_1: 233, XXREAL_0: 2;

        hence thesis by A12, AFINSQ_1: 9;

      end;

        suppose

         A17: k1 > k2;

        then (k2 + 1) <= k1 by NAT_1: 13;

        then

         A18: ((k2 + 1) -' k1) = 0 by NAT_2: 8;

        ( mid (p,k1,k2)) = {} by A17, Th14;

        hence thesis by A18;

      end;

    end;

    theorem :: AFINSQ_2:16

    

     Th16: ( mid (p,1,k)) = (p | k)

    proof

      (1 -' 1) = 0 by XREAL_1: 232;

      hence thesis by Th10;

    end;

    theorem :: AFINSQ_2:17

    ( len p) <= k implies ( mid (p,1,k)) = p

    proof

      assume

       A1: ( len p) <= k;

      

      thus ( mid (p,1,k)) = (p | k) by Th16

      .= p by A1, AFINSQ_1: 52;

    end;

    theorem :: AFINSQ_2:18

    ( mid (p, 0 ,k)) = ( mid (p,1,k))

    proof

      

       A1: ( 0 -' 1) = 0 by NAT_2: 8;

      ( mid (p,1,k)) = (p | k) by Th16;

      hence thesis by A1, Th10;

    end;

    theorem :: AFINSQ_2:19

    ( mid ((p ^ q),(( len p) + 1),(( len p) + ( len q)))) = q

    proof

      

       A1: ((( len p) + 1) -' 1) = ( len p) by NAT_D: 34;

      ( len (p ^ q)) = (( len p) + ( len q)) by AFINSQ_1: 17;

      hence thesis by A1, Th12;

    end;

    registration

      let D be set, f be XFinSequence of D, k1, k2;

      cluster ( mid (f,k1,k2)) -> D -valued;

      coherence ;

    end

    begin

    definition

      let X be finite natural-membered set;

      :: AFINSQ_2:def4

      func Sgm0 X -> XFinSequence of NAT means

      : Def4: ( rng it ) = X & for l,m,k1,k2 be Nat st l < m & m < ( len it ) & k1 = (it . l) & k2 = (it . m) holds k1 < k2;

      existence

      proof

        defpred P[ Nat] means for X be set st X c= ( Segm $1) holds ex p be XFinSequence of NAT st ( rng p) = X & for l,m,k1,k2 be Nat st (l < m & m < ( len p) & k1 = (p . l) & k2 = (p . m)) holds k1 < k2;

        

         A1: ex k be Nat st X c= ( Segm k) by Th2;

        

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

        proof

          let k be Nat such that

           A3: for X be set st X c= ( Segm k) holds ex p be XFinSequence of NAT st ( rng p) = X & for l,m,k1,k2 be Nat st l < m & m < ( len p) & k1 = (p . l) & k2 = (p . m) holds k1 < k2;

          let X be set;

          assume

           A4: X c= ( Segm (k + 1));

          now

            set Y = (X \ {k});

            assume not X c= k;

            then

            consider x be object such that

             A5: x in X and

             A6: not x in ( Segm k);

            reconsider n = x as Element of NAT by A4, A5, Th1;

            n < (k + 1) by A4, A5, NAT_1: 44;

            then

             A7: n <= k by NAT_1: 13;

             not n < k by A6, NAT_1: 44;

            then

             A8: n = k by A7, XXREAL_0: 1;

            

             A9: Y c= ( Segm k)

            proof

              let x be object;

              assume

               A10: x in Y;

              then

              reconsider m = x as Element of NAT by A4, Th1;

               not x in {k} by A10, XBOOLE_0:def 5;

              then

               A12: m <> k by TARSKI:def 1;

              m < (k + 1) by A4, A10, NAT_1: 44;

              then m <= k by NAT_1: 13;

              then m < k by A12, XXREAL_0: 1;

              hence thesis by NAT_1: 44;

            end;

            then

            consider p be XFinSequence of NAT such that

             A13: ( rng p) = Y and

             A14: for l,m,k1,k2 be Nat st l < m & m < ( len p) & k1 = (p . l) & k2 = (p . m) holds k1 < k2 by A3;

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

            consider q be XFinSequence of NAT such that

             A15: q = (p ^ <%k%>);

            

             A16: for l,m,k1,k2 be Nat st l < m & m < ( len q) & k1 = (q . l) & k2 = (q . m) holds k1 < k2

            proof

              let l,m,k1,k2 be Nat;

              assume that

               A17: l < m and

               A18: m < ( len q) and

               A19: k1 = (q . l) and

               A20: k2 = (q . m);

              (m + 1) <= ( len q) by A18, NAT_1: 13;

              then

               A21: m <= (( len q) - 1) by XREAL_1: 19;

              then l < (( len (p ^ <%k%>)) - 1) by A15, A17, XXREAL_0: 2;

              then l < ((( len p) + ( len <%k%>)) - 1) by AFINSQ_1: 17;

              then l < ((( len p) + 1) - 1) by AFINSQ_1: 34;

              then

               A22: l in ( dom p) by AFINSQ_1: 86;

              

               A23: m <= (( len q) -' 1) by A21, XREAL_0:def 2;

               A24:

              now

                

                 A25: k1 = (p . l) by A15, A19, A22, AFINSQ_1:def 3;

                assume m <> (( len q) -' 1);

                then m < (( len (p ^ <%k%>)) -' 1) by A15, A23, XXREAL_0: 1;

                then m < ((( len p) + ( len <%k%>)) -' 1) by AFINSQ_1: 17;

                then m < ((( len p) + 1) -' 1) by AFINSQ_1: 34;

                then

                 A26: m < ( len p) by NAT_D: 34;

                then m in ( dom p) by AFINSQ_1: 86;

                then k2 = (p . m) by A15, A20, AFINSQ_1:def 3;

                hence thesis by A14, A17, A26, A25;

              end;

              now

                assume m = (( len q) -' 1);

                

                then

                 A27: (q . m) = ((p ^ <%k%>) . ((( len p) + ( len <%k%>)) -' 1)) by A15, AFINSQ_1: 17

                .= ((p ^ <%k%>) . ((( len p) + 1) -' 1)) by AFINSQ_1: 34

                .= ((p ^ <%k%>) . ( len p)) by NAT_D: 34

                .= k by AFINSQ_1: 36;

                k1 = (p . l) by A15, A19, A22, AFINSQ_1:def 3;

                then k1 in Y by A13, A22, FUNCT_1:def 3;

                hence thesis by A9, A20, A27, NAT_1: 44;

              end;

              hence thesis by A24;

            end;

            

             A28: {k} c= X by A5, A8, ZFMISC_1: 31;

            ( rng q) = (( rng p) \/ ( rng <%k%>)) by A15, AFINSQ_1: 26

            .= (Y \/ {k}) by A13, AFINSQ_1: 33

            .= (X \/ {k}) by XBOOLE_1: 39

            .= X by A28, XBOOLE_1: 12;

            hence thesis by A16;

          end;

          hence thesis by A3;

        end;

        

         A29: P[ 0 ]

        proof

          let X be set;

          assume

           A30: X c= ( Segm 0 );

          take ( <%> NAT );

          thus ( rng ( <%> NAT )) = X by A30;

          thus thesis;

        end;

        for k2 be Nat holds P[k2] from NAT_1:sch 2( A29, A2);

        hence thesis by A1;

      end;

      uniqueness

      proof

        defpred S[ XFinSequence] means for X st ex k be Nat st X c= k holds ($1 is XFinSequence of NAT & ( rng $1) = X & for l,m,k1,k2 be Nat st (l < m & m < ( len $1) & k1 = ($1 . l) & k2 = ($1 . m)) holds k1 < k2) implies for q be XFinSequence of NAT st ( rng q) = X & for l,m,k1,k2 be Nat st (l < m & m < ( len q) & k1 = (q . l) & k2 = (q . m)) holds k1 < k2 holds q = $1;

        let p,q be XFinSequence of NAT such that

         A31: ( rng p) = X and

         A32: for l,m,k1,k2 be Nat st l < m & m < ( len p) & k1 = (p . l) & k2 = (p . m) holds k1 < k2 and

         A33: ( rng q) = X and

         A34: for l,m,k1,k2 be Nat st l < m & m < ( len q) & k1 = (q . l) & k2 = (q . m) holds k1 < k2;

        

         A35: for p be XFinSequence, x be object st S[p] holds S[(p ^ <%x%>)]

        proof

          let p be XFinSequence, x be object;

          assume

           A36: S[p];

          let X be set;

          given k be Nat such that

           A37: X c= k;

          assume that

           A38: (p ^ <%x%>) is XFinSequence of NAT and

           A39: ( rng (p ^ <%x%>)) = X and

           A40: for l,m,k1,k2 be Nat st l < m & m < ( len (p ^ <%x%>)) & k1 = ((p ^ <%x%>) . l) & k2 = ((p ^ <%x%>) . m) holds k1 < k2;

          let q be XFinSequence of NAT ;

          assume that

           A41: ( rng q) = X and

           A42: for l,m,k1,k2 be Nat st l < m & m < ( len q) & k1 = (q . l) & k2 = (q . m) holds k1 < k2;

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

          ( len q) <> 0

          proof

            assume ( len q) = 0 ;

            then (p ^ <%x%>) = {} by A39, A41, AFINSQ_1: 15, RELAT_1: 38;

            

            then 0 = ( len (p ^ <%x%>))

            .= (( len p) + ( len <%x%>)) by AFINSQ_1: 17

            .= (1 + ( len p)) by AFINSQ_1: 34;

            hence contradiction;

          end;

          then

          consider n be Nat such that

           A43: ( len q) = (n + 1) by NAT_1: 6;

          

           A44: ex m be Nat st m = x & for l be Nat st l in X & l <> x holds l < m

          proof

             <%x%> is XFinSequence of NAT by A38, AFINSQ_1: 31;

            then ( rng <%x%>) c= NAT by RELAT_1:def 19;

            then {x} c= NAT by AFINSQ_1: 33;

            then

            reconsider m = x as Element of NAT by ZFMISC_1: 31;

            take m;

            thus m = x;

            thus for l be Nat st l in X & l <> x holds l < m

            proof

              ( len <%x%>) = 1 by AFINSQ_1: 34;

              

              then

               A45: m = ((p ^ <%x%>) . ((( len p) + ( len <%x%>)) - 1)) by AFINSQ_1: 36

              .= ((p ^ <%x%>) . (( len (p ^ <%x%>)) - 1)) by AFINSQ_1: 17;

              ( len (p ^ <%x%>)) < (( len (p ^ <%x%>)) + 1) by XREAL_1: 29;

              then

               A46: (( len (p ^ <%x%>)) - 1) < ( len (p ^ <%x%>)) by XREAL_1: 19;

              let l be Nat;

              assume that

               A47: l in X and

               A48: l <> x;

              consider y be object such that

               A49: y in ( dom (p ^ <%x%>)) and

               A50: l = ((p ^ <%x%>) . y) by A39, A47, FUNCT_1:def 3;

              reconsider k = y as Element of NAT by A49;

              k < ( len (p ^ <%x%>)) by A49, AFINSQ_1: 86;

              then k < (( len p) + ( len <%x%>)) by AFINSQ_1: 17;

              then k < (( len p) + 1) by AFINSQ_1: 34;

              then

               A51: k <= ( len p) by NAT_1: 13;

              k <> ( len p) by A48, A50, AFINSQ_1: 36;

              then k < ((( len p) + 1) - 1) by A51, XXREAL_0: 1;

              then k < ((( len p) + ( len <%x%>)) - 1) by AFINSQ_1: 34;

              then

               A52: k < (( len (p ^ <%x%>)) - 1) by AFINSQ_1: 17;

              then (( len (p ^ <%x%>)) -' 1) = (( len (p ^ <%x%>)) - 1) by XREAL_0:def 2;

              hence thesis by A40, A50, A52, A46, A45;

            end;

          end;

          then

          reconsider m = x as Nat;

          

           A53: not x in ( rng p)

          proof

            (( len p) + 1) = (( len p) + ( len <%x%>)) by AFINSQ_1: 34

            .= ( len (p ^ <%x%>)) by AFINSQ_1: 17;

            then

             A54: ( len p) < ( len (p ^ <%x%>)) by XREAL_1: 29;

            

             A55: m = ((p ^ <%x%>) . ( len p)) by AFINSQ_1: 36;

            assume x in ( rng p);

            then

            consider y be object such that

             A56: y in ( dom p) and

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

            reconsider y as Element of NAT by A56;

            

             A58: y < ( len p) by A56, AFINSQ_1: 86;

            m = ((p ^ <%x%>) . y) by A56, A57, AFINSQ_1:def 3;

            hence contradiction by A40, A58, A54, A55;

          end;

          

           A59: for z be object holds z in ((( rng p) \/ {x}) \ {x}) iff z in ( rng p)

          proof

            let z be object;

            thus z in ((( rng p) \/ {x}) \ {x}) implies z in ( rng p)

            proof

              assume

               A60: z in ((( rng p) \/ {x}) \ {x});

              then not z in {x} by XBOOLE_0:def 5;

              hence thesis by A60, XBOOLE_0:def 3;

            end;

            assume

             A61: z in ( rng p);

            then

             A62: z in (( rng p) \/ {x}) by XBOOLE_0:def 3;

             not z in {x} by A53, A61, TARSKI:def 1;

            hence thesis by A62, XBOOLE_0:def 5;

          end;

          deffunc Q( set) = (q . $1);

          consider q9 be XFinSequence such that

           A63: ( len q9) = n and

           A64: for m be Nat st m in n holds (q9 . m) = Q(m) from AFINSQ_1:sch 2;

          now

            let x be object;

            assume x in ( rng q9);

            then

            consider y be object such that

             A65: y in ( dom q9) and

             A66: x = (q9 . y) by FUNCT_1:def 3;

            reconsider y as Element of NAT by A65;

            (q . y) in NAT ;

            hence x in NAT by A63, A64, A65, A66;

          end;

          then ( rng q9) c= NAT ;

          then

          reconsider f = q9 as XFinSequence of NAT by RELAT_1:def 19;

          

           A67: p is XFinSequence of NAT by A38, AFINSQ_1: 31;

          

           A68: for m be Nat st m in ( dom <%x%>) holds (q . (( len q9) + m)) = ( <%x%> . m)

          proof

            let m be Nat;

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

            then m in ( len <%x%>);

            then

             A69: m in 1 by AFINSQ_1: 34;

            ( Segm ( 0 + 1)) = (( Segm 0 ) \/ { 0 }) by AFINSQ_1: 2;

            then

             A70: m = 0 by A69, TARSKI:def 1;

            (q . (( len q9) + m)) = x

            proof

              x in {x} by TARSKI:def 1;

              then x in ( rng <%x%>) by AFINSQ_1: 33;

              then x in (( rng p) \/ ( rng <%x%>)) by XBOOLE_0:def 3;

              then x in ( rng q) by A39, A41, AFINSQ_1: 26;

              then

              consider y be object such that

               A71: y in ( dom q) and

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

              reconsider y as Element of NAT by A71;

              (y + 1) <= ( len q) by NAT_1: 13, A71, AFINSQ_1: 86;

              then

               A73: y <= (( len q) - 1) by XREAL_1: 19;

              ( len q) < (( len q) + 1) by XREAL_1: 29;

              then (( len q) - 1) in ( dom q) by A43, AFINSQ_1: 86, XREAL_1: 19;

              then

               A74: (q . (( len q) - 1)) in X by A41, FUNCT_1:def 3;

              ( len q) < (( len q) + 1) by XREAL_1: 29;

              then

               A75: y < (( len q) - 1) & (( len q) - 1) < ( len q) or y = (( len q) - 1) by A73, XREAL_1: 19, XXREAL_0: 1;

              set k = (q . (( len q) - 1));

              consider d be Nat such that

               A76: d = x and

               A77: for l be Nat st l in X & l <> x holds l < d by A44;

              assume (q . (( len q9) + m)) <> x;

              then k < d by A43, A63, A70, A77, A74;

              hence contradiction by A42, A43, A76, A72, A75;

            end;

            hence thesis by A70;

          end;

          

           A78: ( dom q) = (( len q9) + ( len <%x%>)) by A43, A63, AFINSQ_1: 34;

          then

           A79: (q9 ^ <%x%>) = q by A63, A64, A68, AFINSQ_1:def 3;

          

           A80: not x in ( rng f)

          proof

            (( len f) + 1) = (( len f) + ( len <%x%>)) by AFINSQ_1: 34

            .= ( len (f ^ <%x%>)) by AFINSQ_1: 17;

            then

             A81: ( len f) < ( len (f ^ <%x%>)) by XREAL_1: 29;

            

             A82: m = (q . ( len f)) by A79, AFINSQ_1: 36;

            assume x in ( rng f);

            then

            consider y be object such that

             A83: y in ( dom f) and

             A84: x = (f . y) by FUNCT_1:def 3;

            reconsider y as Element of NAT by A83;

            

             A85: y < ( len f) by A83, AFINSQ_1: 86;

            m = (q . y) by A63, A64, A83, A84;

            hence contradiction by A42, A79, A85, A81, A82;

          end;

          

           A86: for z be object holds z in ((( rng f) \/ {x}) \ {x}) iff z in ( rng f)

          proof

            let z be object;

            thus z in ((( rng f) \/ {x}) \ {x}) implies z in ( rng f)

            proof

              assume

               A87: z in ((( rng f) \/ {x}) \ {x});

              then not z in {x} by XBOOLE_0:def 5;

              hence thesis by A87, XBOOLE_0:def 3;

            end;

            assume

             A88: z in ( rng f);

            then

             A89: z in (( rng f) \/ {x}) by XBOOLE_0:def 3;

             not z in {x} by A80, A88, TARSKI:def 1;

            hence thesis by A89, XBOOLE_0:def 5;

          end;

          X = (( rng p) \/ ( rng <%x%>)) by A39, AFINSQ_1: 26

          .= (( rng p) \/ {x}) by AFINSQ_1: 33;

          then

           A90: ( rng p) = (X \ {x}) by A59, TARSKI: 2;

          

           A91: for l,m,k1,k2 be Nat st l < m & m < ( len p) & k1 = (p . l) & k2 = (p . m) holds k1 < k2

          proof

            let l,m,k1,k2 be Nat;

            assume that

             A92: l < m and

             A93: m < ( len p) and

             A94: k1 = (p . l) and

             A95: k2 = (p . m);

            l < ( len p) by A92, A93, XXREAL_0: 2;

            then l in ( dom p) by AFINSQ_1: 86;

            then

             A96: k1 = ((p ^ <%x%>) . l) by A94, AFINSQ_1:def 3;

            ( len p) < (( len p) + 1) by XREAL_1: 29;

            then m < (( len p) + 1) by A93, XXREAL_0: 2;

            then m < (( len p) + ( len <%x%>)) by AFINSQ_1: 34;

            then

             A97: m < ( len (p ^ <%x%>)) by AFINSQ_1: 17;

            m in ( dom p) by A93, AFINSQ_1: 86;

            then k2 = ((p ^ <%x%>) . m) by A95, AFINSQ_1:def 3;

            hence thesis by A40, A92, A96, A97;

          end;

          

           A98: for l,m,k1,k2 be Nat st l < m & m < ( len f) & k1 = (f . l) & k2 = (f . m) holds k1 < k2

          proof

            let l,m,k1,k2 be Nat;

            assume that

             A99: l < m and

             A100: m < ( len f) and

             A101: k1 = (f . l) and

             A102: k2 = (f . m);

            

             A103: k2 = (q . m) by A64, A102, A63, A100, AFINSQ_1: 86;

            l < n by A63, A99, A100, XXREAL_0: 2;

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

            then

             A104: k1 = (q . l) by A64, A101;

            m < ( len q) by A43, A63, A100, NAT_1: 13;

            hence thesis by A42, A99, A104, A103;

          end;

          X = (( rng f) \/ ( rng <%x%>)) by A41, A79, AFINSQ_1: 26

          .= (( rng f) \/ {x}) by AFINSQ_1: 33;

          then

           A105: ( rng f) = (X \ {x}) by A86, TARSKI: 2;

          ex m be Nat st (X \ {x}) c= m by A37, XBOOLE_1: 1;

          then q9 = p by A36, A91, A67, A90, A98, A105;

          hence thesis by A63, A64, A78, A68, AFINSQ_1:def 3;

        end;

        

         A106: S[ {} ];

        

         A107: for p be XFinSequence holds S[p] from AFINSQ_1:sch 3( A106, A35);

        ex k be Nat st X c= ( Segm k) by Th2;

        hence thesis by A31, A32, A33, A34, A107;

      end;

    end

    registration

      let A be finite natural-membered set;

      cluster ( Sgm0 A) -> one-to-one;

      coherence

      proof

        for x,y be object st x in ( dom ( Sgm0 A)) & y in ( dom ( Sgm0 A)) & (( Sgm0 A) . x) = (( Sgm0 A) . y) & x <> y holds contradiction

        proof

          let x,y be object;

          assume that

           A1: x in ( dom ( Sgm0 A)) and

           A2: y in ( dom ( Sgm0 A)) and

           A3: (( Sgm0 A) . x) = (( Sgm0 A) . y) and

           A4: x <> y;

          reconsider i = x, j = y as Element of NAT by A1, A2;

          per cases by A4, XXREAL_0: 1;

            suppose

             A5: i < j;

            j < ( len ( Sgm0 A)) by A2, AFINSQ_1: 86;

            hence contradiction by A3, A5, Def4;

          end;

            suppose

             A6: j < i;

            i < ( len ( Sgm0 A)) by A1, AFINSQ_1: 86;

            hence contradiction by A3, A6, Def4;

          end;

        end;

        hence thesis;

      end;

    end

    theorem :: AFINSQ_2:20

    

     Th20: for A be finite natural-membered set holds ( len ( Sgm0 A)) = ( card A)

    proof

      let A be finite natural-membered set;

      ( rng ( Sgm0 A)) = A by Def4;

      then (( len ( Sgm0 A)),A) are_equipotent by WELLORD2:def 4;

      then ( card A) = ( card ( len ( Sgm0 A))) by CARD_1: 5;

      hence thesis;

    end;

    theorem :: AFINSQ_2:21

    

     Th21: for X,Y be finite natural-membered set st X c= Y & X <> {} holds (( Sgm0 Y) . 0 ) <= (( Sgm0 X) . 0 )

    proof

      let X,Y be finite natural-membered set;

      assume that

       A1: X c= Y and

       A2: X <> {} ;

      reconsider X0 = X as finite set;

       0 <> ( card X0) by A2;

      then 0 < ( len ( Sgm0 X)) by Th20;

      then

       A3: 0 in ( dom ( Sgm0 X)) by AFINSQ_1: 86;

      

       A4: ( rng ( Sgm0 Y)) = Y by Def4;

      ( rng ( Sgm0 X)) = X by Def4;

      then (( Sgm0 X) . 0 ) in X by A3, FUNCT_1:def 3;

      then

      consider x be object such that

       A5: x in ( dom ( Sgm0 Y)) and

       A6: (( Sgm0 Y) . x) = (( Sgm0 X) . 0 ) by A1, A4, FUNCT_1:def 3;

      reconsider nx = x as Nat by A5;

      

       A7: nx < ( len ( Sgm0 Y)) by A5, AFINSQ_1: 86;

      now

        per cases ;

          case 0 <> nx;

          hence thesis by A6, A7, Def4;

        end;

          case 0 = nx;

          hence thesis by A6;

        end;

      end;

      hence thesis;

    end;

    theorem :: AFINSQ_2:22

    

     Th22: (( Sgm0 {n}) . 0 ) = n

    proof

      ( len ( Sgm0 {n})) = ( card {n}) by Th20;

      then 0 in ( dom ( Sgm0 {n})) by AFINSQ_1: 86;

      then

       A1: (( Sgm0 {n}) . 0 ) in ( rng ( Sgm0 {n})) by FUNCT_1:def 3;

      ( rng ( Sgm0 {n})) = {n} by Def4;

      hence thesis by A1, TARSKI:def 1;

    end;

    definition

      let B1,B2 be set;

      :: AFINSQ_2:def5

      pred B1 <N< B2 means for n,m be Nat st n in B1 & m in B2 holds n < m;

    end

    definition

      let B1,B2 be set;

      :: AFINSQ_2:def6

      pred B1 <N= B2 means for n, m st n in B1 & m in B2 holds n <= m;

    end

    theorem :: AFINSQ_2:23

    

     Th23: for B1,B2 be set st B1 <N< B2 holds ((B1 /\ B2) /\ NAT ) = {}

    proof

      let B1,B2 be set;

      assume

       A1: B1 <N< B2;

      now

        set x = the Element of ((B1 /\ B2) /\ NAT );

        reconsider nx = x as Nat;

        assume ((B1 /\ B2) /\ NAT ) <> {} ;

        then

         A2: x in (B1 /\ B2) by XBOOLE_0:def 4;

        then

         A3: nx in B2 by XBOOLE_0:def 4;

        nx in B1 by A2, XBOOLE_0:def 4;

        hence contradiction by A1, A3;

      end;

      hence thesis;

    end;

    theorem :: AFINSQ_2:24

    for B1,B2 be finite natural-membered set st B1 <N< B2 holds B1 misses B2

    proof

      let B1,B2 be finite natural-membered set;

      assume

       A1: B1 <N< B2;

      now

        set x = the Element of (B1 /\ B2);

        assume

         a2: B1 meets B2;

        then

         A3: x in B2 by XBOOLE_0:def 4;

        x in B1 by a2, XBOOLE_0:def 4;

        hence contradiction by A1, A3;

      end;

      hence thesis;

    end;

    theorem :: AFINSQ_2:25

    

     Th25: for A,B1,B2 be set st B1 <N< B2 holds (A /\ B1) <N< (A /\ B2)

    proof

      let A,B1,B2 be set;

      assume

       A1: B1 <N< B2;

      for n, m st n in (A /\ B1) & m in (A /\ B2) holds n < m

      proof

        let n, m;

        assume that

         A2: n in (A /\ B1) and

         A3: m in (A /\ B2);

        

         A4: m in B2 by A3, XBOOLE_0:def 4;

        n in B1 by A2, XBOOLE_0:def 4;

        hence thesis by A1, A4;

      end;

      hence thesis;

    end;

    theorem :: AFINSQ_2:26

    for X,Y be finite natural-membered set st Y <> {} & (ex x be set st x in X & {x} <N= Y) holds (( Sgm0 X) . 0 ) <= (( Sgm0 Y) . 0 )

    proof

      let X,Y be finite natural-membered set;

      assume that

       A1: Y <> {} and

       A2: ex x be set st x in X & {x} <N= Y;

      consider x be set such that

       A3: x in X and

       A4: {x} <N= Y by A2;

       0 <> ( card Y) by A1;

      then 0 < ( len ( Sgm0 Y)) by Th20;

      then

       A5: 0 in ( dom ( Sgm0 Y)) by AFINSQ_1: 86;

      ( rng ( Sgm0 Y)) = Y by Def4;

      then

       A6: (( Sgm0 Y) . 0 ) in Y by A5, FUNCT_1:def 3;

      reconsider x0 = x as Element of NAT by A3, ORDINAL1:def 12;

      set nx = x0;

      nx in {x0} by TARSKI:def 1;

      then

       A7: nx <= (( Sgm0 Y) . 0 ) by A4, A6;

       {x0} c= X by A3, TARSKI:def 1;

      then

       A8: (( Sgm0 X) . 0 ) <= (( Sgm0 {x0}) . 0 ) by Th21;

      (( Sgm0 {x0}) . 0 ) = nx by Th22;

      hence thesis by A8, A7, XXREAL_0: 2;

    end;

    theorem :: AFINSQ_2:27

    

     Th27: for X0,Y0 be finite natural-membered set st X0 <N< Y0 & i < ( card X0) holds ( rng (( Sgm0 (X0 \/ Y0)) | ( card X0))) = X0 & ((( Sgm0 (X0 \/ Y0)) | ( card X0)) . i) = (( Sgm0 (X0 \/ Y0)) . i)

    proof

      let X0,Y0 be finite natural-membered set;

      assume that

       A1: X0 <N< Y0 and

       A2: i < ( card X0);

      

       A3: i in ( Segm ( card X0)) by A2, NAT_1: 44;

      set f = (( Sgm0 (X0 \/ Y0)) | ( card X0));

      set f0 = ( Sgm0 (X0 \/ Y0));

      set Z = { v where v be Element of (X0 \/ Y0) : ex k2 be Nat st v = (f . k2) & k2 in ( card X0) };

      

       A4: X0 c= (X0 \/ Y0) by XBOOLE_1: 7;

      

       A5: ( len ( Sgm0 (X0 \/ Y0))) = ( card (X0 \/ Y0)) by Th20;

      then

       A6: ( len f) = ( card X0) by A4, AFINSQ_1: 54, NAT_1: 43;

      

       A7: Z c= ( rng f)

      proof

        let y be object;

        assume y in Z;

        then ex v0 be Element of (X0 \/ Y0) st y = v0 & ex k2 be Nat st v0 = (f . k2) & k2 in ( card X0);

        hence thesis by A6, FUNCT_1:def 3;

      end;

      then

      reconsider Z0 = Z as finite set;

      f is one-to-one by FUNCT_1: 52;

      then

       A8: (( dom f),(f .: ( dom f))) are_equipotent by CARD_1: 33;

      

       A9: (f .: ( dom f)) = ( rng f) by RELAT_1: 113;

      

       A10: ( len f0) = ( card (X0 \/ Y0)) by Th20;

      

       A11: ( rng f0) = (X0 \/ Y0) by Def4;

      

       A12: ( rng f) c= Z

      proof

        let y be object;

        assume

         A13: y in ( rng f);

        then

        consider x be object such that

         A14: x in ( dom f) and

         A15: y = (f . x) by FUNCT_1:def 3;

        reconsider y0 = y as Element of (X0 \/ Y0) by Def4, A13;

        ex k2 be Nat st y0 = (f . k2) & k2 in ( card X0) by A14, A15;

        hence thesis;

      end;

      then ( rng f) = Z by A7;

      then ( card Z) = ( card ( len f)) by A8, A9, CARD_1: 5;

      then

       A16: ( card Z) = ( card X0) by A5, A4, AFINSQ_1: 54, NAT_1: 43;

      

       A17: (X0 \/ Y0) <> {} by A2, CARD_1: 27, XBOOLE_1: 15;

       A18:

      now

        assume that

         A19: not Z c= X0 and

         A20: not X0 c= Z;

        consider v1 be object such that

         A21: v1 in Z and

         A22: not v1 in X0 by A19;

        consider v10 be Element of (X0 \/ Y0) such that

         A23: v1 = v10 and

         A24: ex k2 be Nat st v10 = (f . k2) & k2 in ( card X0) by A21;

        

         A25: v10 in Y0 by A17, A22, A23, XBOOLE_0:def 3;

        reconsider nv10 = v10 as Nat;

        consider v2 be object such that

         A26: v2 in X0 and

         A27: not v2 in Z by A20;

        X0 c= (X0 \/ Y0) by XBOOLE_1: 7;

        then

        consider x2 be object such that

         A28: x2 in ( dom f0) and

         A29: v2 = (f0 . x2) by A11, A26, FUNCT_1:def 3;

        reconsider x20 = x2 as Nat by A28;

        reconsider nv2 = v2 as Nat by A29;

        

         A30: x20 < ( len f0) by A28, AFINSQ_1: 86;

         A31:

        now

          assume x20 < ( card X0);

          then

           A32: x20 in ( Segm ( card X0)) by NAT_1: 44;

          ( card X0) <= ( card (X0 \/ Y0)) by NAT_1: 43, XBOOLE_1: 7;

          then ( card X0) <= ( len f0) by Th20;

          then (f . x20) = (f0 . x20) by A32, AFINSQ_1: 53;

          hence contradiction by A4, A26, A27, A29, A32;

        end;

        consider k20 be Nat such that

         A33: v10 = (f . k20) and

         A34: k20 in ( card X0) by A24;

        ( card X0) <= ( len f0) by A10, NAT_1: 43, XBOOLE_1: 7;

        then

         A35: (f . k20) = (f0 . k20) by A34, AFINSQ_1: 53;

        k20 < ( len f) by A6, A34, AFINSQ_1: 86;

        then k20 < x20 by A6, A31, XXREAL_0: 2;

        then nv10 < nv2 by A33, A29, A35, A30, Def4;

        hence contradiction by A1, A26, A25;

      end;

       A36:

      now

        per cases by A18;

          case Z0 c= X0;

          hence Z0 = X0 by A16, CARD_2: 102;

        end;

          case X0 c= Z0;

          hence Z0 = X0 by A16, CARD_2: 102;

        end;

      end;

      ( card X0) <= ( len f0) by A5, NAT_1: 43, XBOOLE_1: 7;

      hence thesis by A12, A7, A36, A3, AFINSQ_1: 53;

    end;

    theorem :: AFINSQ_2:28

    for X,Y be finite natural-membered set st X <N< Y & i in ( card X) holds (( Sgm0 (X \/ Y)) . i) in X

    proof

      let X,Y be finite natural-membered set;

      assume that

       A1: X <N< Y and

       A2: i in ( card X);

      set f = (( Sgm0 (X \/ Y)) | ( card X));

      set f0 = ( Sgm0 (X \/ Y));

      set Z = { v where v be Element of (X \/ Y) : ex k2 be Nat st v = (f . k2) & k2 in ( card X) };

      

       A3: ( rng f0) = (X \/ Y) by Def4;

      ( len ( Sgm0 (X \/ Y))) = ( card (X \/ Y)) by Th20;

      then

       A4: ( card X) <= ( len ( Sgm0 (X \/ Y))) by NAT_1: 43, XBOOLE_1: 7;

      then

       A5: ( len f) = ( card X) by AFINSQ_1: 54;

      

       A6: Z c= ( rng f)

      proof

        let y be object;

        assume y in Z;

        then ex v0 be Element of (X \/ Y) st y = v0 & ex k2 be Nat st v0 = (f . k2) & k2 in ( card X);

        hence thesis by A5, FUNCT_1:def 3;

      end;

      then

      reconsider Z0 = Z as finite set;

      ( rng f) c= Z

      proof

        let y be object;

        assume

         A7: y in ( rng f);

        then

        consider x be object such that

         A8: x in ( dom f) and

         A9: y = (f . x) by FUNCT_1:def 3;

        reconsider y0 = y as Element of (X \/ Y) by A7, Def4;

        ex k2 be Nat st y0 = (f . k2) & k2 in ( card X) by A8, A9;

        hence thesis;

      end;

      then

       A10: ( rng f) = Z by A6;

      

       A11: (X \/ Y) <> {} by A2, CARD_1: 27, XBOOLE_1: 15;

       A12:

      now

        assume that

         A13: not Z c= X and

         A14: not X c= Z;

        consider v1 be object such that

         A15: v1 in Z and

         A16: not v1 in X by A13;

        consider v10 be Element of (X \/ Y) such that

         A17: v1 = v10 and

         A18: ex k2 be Nat st v10 = (f . k2) & k2 in ( card X) by A15;

        

         A19: v10 in Y by A11, A16, A17, XBOOLE_0:def 3;

        reconsider nv10 = v10 as Nat;

        consider v2 be object such that

         A20: v2 in X and

         A21: not v2 in Z by A14;

        X c= (X \/ Y) by XBOOLE_1: 7;

        then

        consider x2 be object such that

         A22: x2 in ( dom f0) and

         A23: v2 = (f0 . x2) by A3, A20, FUNCT_1:def 3;

        reconsider x20 = x2 as Nat by A22;

        now

          assume x20 < ( card X);

          then

           A24: x20 in ( Segm ( card X)) by NAT_1: 44;

          ( card X) <= ( card (X \/ Y)) by NAT_1: 43, XBOOLE_1: 7;

          then ( card X) <= ( len f0) by Th20;

          then (f . x20) = (f0 . x20) by A24, AFINSQ_1: 53;

          hence contradiction by A5, A10, A21, A23, A24, FUNCT_1:def 3;

        end;

        then

         A25: ( len f) <= x20 by A4, AFINSQ_1: 54;

        consider k20 be Nat such that

         A26: v10 = (f . k20) and

         A27: k20 in ( card X) by A18;

        

         A28: (f . k20) = (f0 . k20) by A4, A27, AFINSQ_1: 53;

        reconsider nv2 = v2 as Nat by A23;

        k20 < ( len f) by A5, A27, AFINSQ_1: 86;

        then

         A29: k20 < x20 by A25, XXREAL_0: 2;

        x20 < ( len f0) by A22, AFINSQ_1: 86;

        then nv10 < nv2 by A26, A23, A29, A28, Def4;

        hence contradiction by A1, A20, A19;

      end;

      f is one-to-one by FUNCT_1: 52;

      then

       A30: (( dom f),(f .: ( dom f))) are_equipotent by CARD_1: 33;

      (f .: ( dom f)) = ( rng f) by RELAT_1: 113;

      then

       A31: ( card Z) = ( card ( len f)) by A10, A30, CARD_1: 5;

      then

       A32: ( card Z) = ( card X) by A4, AFINSQ_1: 54;

       A33:

      now

        per cases by A12;

          case Z0 c= X;

          hence Z0 = X by A4, A31, CARD_2: 102, AFINSQ_1: 54;

        end;

          case X c= Z0;

          hence Z0 = X by A32, CARD_2: 102;

        end;

      end;

      (f . i) = (f0 . i) by A2, A4, AFINSQ_1: 53;

      hence thesis by A2, A5, A10, A33, FUNCT_1:def 3;

    end;

    theorem :: AFINSQ_2:29

    

     Th29: for X,Y be finite natural-membered set st X <N< Y & i < ( len ( Sgm0 X)) holds (( Sgm0 X) . i) = (( Sgm0 (X \/ Y)) . i)

    proof

      let X,Y be finite natural-membered set;

      assume that

       A1: X <N< Y and

       A2: i < ( len ( Sgm0 X));

      reconsider h = (( Sgm0 (X \/ Y)) | ( len ( Sgm0 X))) as XFinSequence of NAT ;

      

       A3: ( len ( Sgm0 X)) = ( card X) by Th20;

      then

       A4: (h . i) = (( Sgm0 (X \/ Y)) . i) by A1, A2, Th27;

      ( Segm ( card X)) c= ( Segm ( card (X \/ Y))) by CARD_1: 11, XBOOLE_1: 7;

      then

       A5: ( card X) <= ( card (X \/ Y)) by NAT_1: 39;

      then ( card X) <= ( len ( Sgm0 (X \/ Y))) by Th20;

      then

       A6: ( len ( Sgm0 X)) <= ( len ( Sgm0 (X \/ Y))) by Th20;

      

       A7: ( len ( Sgm0 (X \/ Y))) = ( card (X \/ Y)) by Th20;

      then

       A8: ( len h) = ( len ( Sgm0 X)) by A5, A3, AFINSQ_1: 54;

      

       A9: ( len h) = ( card X) by A5, A3, A7, AFINSQ_1: 54;

      

       A10: for l,m,k1,k2 be Nat st l < m & m < ( len h) & k1 = (h . l) & k2 = (h . m) holds k1 < k2

      proof

        let l,m,k1,k2 be Nat;

        assume that

         A11: l < m and

         A12: m < ( len h) and

         A13: k1 = (h . l) and

         A14: k2 = (h . m);

        

         A15: m < ( len ( Sgm0 (X \/ Y))) by A8, A6, A12, XXREAL_0: 2;

        l < ( card X) by A9, A11, A12, XXREAL_0: 2;

        then

         A16: (h . l) = (( Sgm0 (X \/ Y)) . l) by A1, A3, Th27;

        (h . m) = (( Sgm0 (X \/ Y)) . m) by A1, A3, A8, A12, Th27;

        hence thesis by A11, A13, A14, A16, A15, Def4;

      end;

      ( rng h) = X by A1, A2, A3, Th27;

      hence thesis by A10, A4, Def4;

    end;

    theorem :: AFINSQ_2:30

    

     Th30: for X0,Y0 be finite natural-membered set st X0 <N< Y0 & i < ( card Y0) holds ( rng (( Sgm0 (X0 \/ Y0)) /^ ( card X0))) = Y0 & ((( Sgm0 (X0 \/ Y0)) /^ ( card X0)) . i) = (( Sgm0 (X0 \/ Y0)) . (i + ( card X0)))

    proof

      let X0,Y0 be finite natural-membered set;

      assume that

       A1: X0 <N< Y0 and

       A2: i < ( card Y0);

      consider n be Nat such that

       A3: Y0 c= ( Segm n) by Th2;

      (X0 /\ Y0) = (X0 /\ (Y0 /\ NAT )) by A3, XBOOLE_1: 1, XBOOLE_1: 28

      .= ((X0 /\ Y0) /\ NAT ) by XBOOLE_1: 16

      .= {} by A1, Th23;

      then

       A4: X0 misses Y0;

      set f = (( Sgm0 (X0 \/ Y0)) /^ ( card X0));

      set f0 = ( Sgm0 (X0 \/ Y0));

      set Z = { v where v be Element of (X0 \/ Y0) : ex k2 be Nat st v = (f . k2) & k2 in ( card Y0) };

      

       A5: (( dom f),(f .: ( dom f))) are_equipotent by CARD_1: 33;

      

       A6: ( rng f0) = (X0 \/ Y0) by Def4;

      

       A7: ( len ( Sgm0 (X0 \/ Y0))) = ( card (X0 \/ Y0)) by Th20;

      then

       A8: ( card X0) <= ( len ( Sgm0 (X0 \/ Y0))) by NAT_1: 43, XBOOLE_1: 7;

      

       A9: ( len f) = (( len f0) -' ( card X0)) by Def2

      .= (( len f0) - ( card X0)) by A8, XREAL_1: 233;

      

       A10: ((X0 \/ Y0) \ X0) = ((X0 \ X0) \/ (Y0 \ X0)) by XBOOLE_1: 42

      .= ( {} \/ (Y0 \ X0)) by XBOOLE_1: 37

      .= Y0 by A4, XBOOLE_1: 83;

      then

       A11: ( len f) = ( card Y0) by A7, A9, CARD_2: 44, XBOOLE_1: 7;

      

       A12: Z c= ( rng f)

      proof

        let y be object;

        assume y in Z;

        then ex v0 be Element of (X0 \/ Y0) st y = v0 & ex k2 be Nat st v0 = (f . k2) & k2 in ( card Y0);

        hence thesis by A11, FUNCT_1:def 3;

      end;

      then

      reconsider Z0 = Z as finite set;

      

       A13: (f .: ( dom f)) = ( rng f) by RELAT_1: 113;

      

       A14: ( rng f) c= ( rng ( Sgm0 (X0 \/ Y0))) by Th9;

      

       A15: ( rng f) c= Z

      proof

        let y be object;

        assume

         A16: y in ( rng f);

        then

        consider x be object such that

         A17: x in ( dom f) and

         A18: y = (f . x) by FUNCT_1:def 3;

        reconsider y0 = y as Element of (X0 \/ Y0) by A14, A16, Def4;

        ex k2 be Nat st y0 = (f . k2) & k2 in ( card Y0) by A11, A17, A18;

        hence thesis;

      end;

      then ( rng f) = Z by A12;

      then ( card Z) = ( card ( len f)) by A5, A13, CARD_1: 5;

      then

       A19: ( card Z) = ( card Y0) by A7, A9, A10, CARD_2: 44, XBOOLE_1: 7;

      ( len f0) = ( card (X0 \/ Y0)) by Th20;

      then

       A20: ( len f0) = (( card X0) + ( card Y0)) by A4, CARD_2: 40;

      

       A21: (X0 \/ Y0) <> {} by A2, CARD_1: 27, XBOOLE_1: 15;

       A22:

      now

        assume that

         A23: not Z c= Y0 and

         A24: not Y0 c= Z;

        consider v2 be object such that

         A25: v2 in Y0 and

         A26: not v2 in Z by A24;

        Y0 c= (X0 \/ Y0) by XBOOLE_1: 7;

        then

        consider x2 be object such that

         A27: x2 in ( dom f0) and

         A28: v2 = (f0 . x2) by A6, A25, FUNCT_1:def 3;

        consider v1 be object such that

         A29: v1 in Z and

         A30: not v1 in Y0 by A23;

        consider v10 be Element of (X0 \/ Y0) such that

         A31: v1 = v10 and

         A32: ex k2 be Nat st v10 = (f . k2) & k2 in ( Segm ( card Y0)) by A29;

        

         A33: v10 in X0 by A21, A30, A31, XBOOLE_0:def 3;

        reconsider nv10 = v10 as Nat;

        reconsider nv2 = v2 as Nat by A28;

        consider k20 be Nat such that

         A34: v10 = (f . k20) and

         A35: k20 in ( Segm ( card Y0)) by A32;

        

         A36: (k20 + ( card X0)) < ( len f0) by A20, XREAL_1: 6, A35, NAT_1: 44;

        then

         A37: (f . k20) = (f0 . (k20 + ( card X0))) by Th8;

        reconsider x20 = x2 as Nat by A27;

        set nx20 = (x20 -' ( card X0));

        

         A38: v2 in (X0 \/ Y0) by A6, A27, A28, FUNCT_1:def 3;

         A39:

        now

          assume

           A40: x20 >= ( card X0);

          then

           A41: (x20 -' ( card X0)) = (x20 - ( card X0)) by XREAL_1: 233;

          x20 < (( card X0) + ( card Y0)) by A20, A27, AFINSQ_1: 86;

          then (x20 - ( card X0)) < ((( card X0) + ( card Y0)) - ( card X0)) by XREAL_1: 9;

          then

           A42: nx20 < ( card Y0) by A40, XREAL_1: 233;

          then

           A43: nx20 in ( Segm ( card Y0)) by NAT_1: 44;

          (nx20 + ( card X0)) < ( len f0) by A20, A42, XREAL_1: 6;

          then (f . nx20) = (f0 . x20) by A41, Th8;

          hence contradiction by A26, A28, A38, A43;

        end;

        ( card X0) <= (( card X0) + k20) by NAT_1: 12;

        then (k20 + ( card X0)) > x20 by A39, XXREAL_0: 2;

        then nv10 > nv2 by A34, A28, A36, A37, Def4;

        hence contradiction by A1, A25, A33;

      end;

       A44:

      now

        per cases by A22;

          case Z0 c= Y0;

          hence Z0 = Y0 by A19, CARD_2: 102;

        end;

          case Y0 c= Z0;

          hence Z0 = Y0 by A19, CARD_2: 102;

        end;

      end;

      (i + ( card X0)) < ( len f0) by A2, A9, A11, XREAL_1: 20;

      hence thesis by A15, A12, A44, Th8;

    end;

    theorem :: AFINSQ_2:31

    

     Th31: for X,Y be finite natural-membered set st X <N< Y & i < ( len ( Sgm0 Y)) holds (( Sgm0 Y) . i) = (( Sgm0 (X \/ Y)) . (i + ( len ( Sgm0 X))))

    proof

      let X,Y be finite natural-membered set;

      assume that

       A1: X <N< Y and

       A2: i < ( len ( Sgm0 Y));

      consider m be Nat such that

       A3: Y c= ( Segm m) by Th2;

      reconsider h = (( Sgm0 (X \/ Y)) /^ ( len ( Sgm0 X))) as XFinSequence of NAT ;

      

       A4: ( len ( Sgm0 X)) = ( card X) by Th20;

      

       A5: ( len ( Sgm0 Y)) = ( card Y) by Th20;

      then

       A6: (h . i) = (( Sgm0 (X \/ Y)) . (i + ( card X))) by A1, A2, A4, Th30;

      

       A7: ( len ( Sgm0 (X \/ Y))) = ( card (X \/ Y)) by Th20;

      (X /\ Y) = (X /\ (Y /\ NAT )) by A3, XBOOLE_1: 1, XBOOLE_1: 28

      .= ((X /\ Y) /\ NAT ) by XBOOLE_1: 16

      .= {} by A1, Th23;

      then X misses Y;

      then

       A8: (( card Y) + ( card X)) = ( card (X \/ Y)) by CARD_2: 40;

      ( len h) = (( len ( Sgm0 (X \/ Y))) -' ( len ( Sgm0 X))) by Def2

      .= ((( card X) + ( card Y)) -' ( card X)) by A8, A7, Th20

      .= ( card Y) by NAT_D: 34

      .= ( len ( Sgm0 Y)) by Th20;

      then

       A9: ( len h) = ( card Y) by Th20;

      

       A10: for l,m,k1,k2 be Nat st l < m & m < ( len h) & k1 = (h . l) & k2 = (h . m) holds k1 < k2

      proof

        let l,m,k1,k2 be Nat;

        assume that

         A11: l < m and

         A12: m < ( len h) and

         A13: k1 = (h . l) and

         A14: k2 = (h . m);

        

         A15: (m + ( card X)) < ( len ( Sgm0 (X \/ Y))) by A8, A7, A9, A12, XREAL_1: 6;

        set m3 = (m + ( card X));

        set l3 = (l + ( card X));

        

         A16: l3 < m3 by A11, XREAL_1: 6;

        l < ( card Y) by A9, A11, A12, XXREAL_0: 2;

        then

         A17: (h . l) = (( Sgm0 (X \/ Y)) . (l + ( card X))) by A1, A4, Th30;

        (h . m) = (( Sgm0 (X \/ Y)) . (m + ( card X))) by A1, A4, A9, A12, Th30;

        hence thesis by A13, A14, A17, A15, A16, Def4;

      end;

      ( rng h) = Y by A1, A2, A4, A5, Th30;

      hence thesis by A4, A10, A6, Def4;

    end;

    theorem :: AFINSQ_2:32

    

     Th32: for X,Y be finite natural-membered set st Y <> {} & X <N< Y holds (( Sgm0 Y) . 0 ) = (( Sgm0 (X \/ Y)) . ( len ( Sgm0 X)))

    proof

      let X,Y be finite natural-membered set;

      assume that

       A1: Y <> {} and

       A2: X <N< Y;

      ( card Y) <> 0 by A1;

      then 0 < ( len ( Sgm0 Y)) by Th20;

      then (( Sgm0 Y) . 0 ) = (( Sgm0 (X \/ Y)) . ( 0 qua Element of NAT + ( len ( Sgm0 X)))) by A2, Th31;

      hence thesis;

    end;

    theorem :: AFINSQ_2:33

    

     Th33: for l,m,n,k be Nat, X be finite natural-membered set st k < l & m < ( len ( Sgm0 X)) & (( Sgm0 X) . m) = k & (( Sgm0 X) . n) = l holds m < n

    proof

      let l,m,n,k be Nat, X be finite natural-membered set;

      assume that

       A1: k < l and

       A2: m < ( len ( Sgm0 X)) and

       A3: (( Sgm0 X) . m) = k and

       A4: (( Sgm0 X) . n) = l and

       A5: not m < n;

      n < m by A1, A3, A4, A5, XXREAL_0: 1;

      hence thesis by A1, A2, A3, A4, Def4;

    end;

    theorem :: AFINSQ_2:34

    

     Th34: for X,Y be finite natural-membered set st X <> {} & X <N< Y holds (( Sgm0 X) . 0 ) = (( Sgm0 (X \/ Y)) . 0 )

    proof

      let X,Y be finite natural-membered set;

      assume that

       A1: X <> {} and

       A2: X <N< Y;

      ( card X) <> 0 by A1;

      then 0 < ( len ( Sgm0 X)) by Th20;

      hence thesis by A2, Th29;

    end;

    theorem :: AFINSQ_2:35

    

     Th35: for X,Y be finite natural-membered set holds X <N< Y iff ( Sgm0 (X \/ Y)) = (( Sgm0 X) ^ ( Sgm0 Y))

    proof

      let X,Y be finite natural-membered set;

      set p = ( Sgm0 X);

      set q = ( Sgm0 Y);

      set r = ( Sgm0 (X \/ Y));

      thus X <N< Y implies ( Sgm0 (X \/ Y)) = (( Sgm0 X) ^ ( Sgm0 Y))

      proof

        defpred P[ Nat] means $1 in ( dom p) implies (r . $1) = (p . $1);

        reconsider X1 = X, Y1 = Y as finite set;

        assume

         A1: X <N< Y;

        (X /\ Y) = {}

        proof

          set x = the Element of (X /\ Y);

          

           A2: X = ( rng p) by Def4;

          assume

           A3: not thesis;

          then x in X by XBOOLE_0:def 4;

          then

          reconsider m = x as Element of NAT by A2;

          

           A4: m in Y by A3, XBOOLE_0:def 4;

          m in X by A3, XBOOLE_0:def 4;

          hence thesis by A1, A4;

        end;

        then

         A5: X misses Y;

        

         A6: ( len r) = ( card (X1 \/ Y1)) by Th20

        .= (( card X1) + ( card Y1)) by A5, CARD_2: 40

        .= (( len p) + ( card Y1)) by Th20

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

         A7:

        now

          let k;

          assume

           A8: P[k];

          thus P[(k + 1)]

          proof

            set m = (r . (k + 1));

            set n = (p . (k + 1));

            assume

             A9: (k + 1) in ( dom p);

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

            then

             A10: n in X by Def4;

            ( len p) <= ( len r) by A6, NAT_1: 12;

            then

             A11: ( Segm ( len p)) c= ( Segm ( len r)) by NAT_1: 39;

            then m in ( rng r) by A9, FUNCT_1:def 3;

            then

             A12: m in (X \/ Y) by Def4;

            assume

             A13: m <> n;

            now

              per cases ;

                suppose

                 A14: k in ( dom p);

                set m1 = (r . k);

                set n1 = (p . k);

                now

                  per cases by A13, XXREAL_0: 1;

                    suppose

                     A15: m < n;

                    then not m in Y by A1, A10;

                    then m in X by A12, XBOOLE_0:def 3;

                    then m in ( rng p) by Def4;

                    then

                    consider x be object such that

                     A16: x in ( dom p) and

                     A17: (p . x) = m by FUNCT_1:def 3;

                    reconsider x as Element of NAT by A16;

                    x < ( len p) by A16, AFINSQ_1: 86;

                    then

                     A18: x < (k + 1) by A15, A17, Th33;

                    

                     A19: k < (k + 1) by XREAL_1: 29;

                    (k + 1) < ( len r) by A9, A11, AFINSQ_1: 86;

                    then

                     A20: n1 < m by A8, A14, A19, Def4;

                    k < ( len p) by A14, AFINSQ_1: 86;

                    then k < x by A17, A20, Th33;

                    hence contradiction by A18, NAT_1: 13;

                  end;

                    suppose

                     A21: n < m;

                    n in (X \/ Y) by A10, XBOOLE_0:def 3;

                    then n in ( rng r) by Def4;

                    then

                    consider x be object such that

                     A22: x in ( dom r) and

                     A23: (r . x) = n by FUNCT_1:def 3;

                    reconsider x as Element of NAT by A22;

                    x < ( len r) by A22, AFINSQ_1: 86;

                    then

                     A24: x < (k + 1) by A21, A23, Th33;

                    

                     A25: k < (k + 1) by XREAL_1: 29;

                    (k + 1) < ( len p) by A9, AFINSQ_1: 86;

                    then

                     A26: m1 < n by A8, A14, A25, Def4;

                    k < ( len r) by A11, A14, AFINSQ_1: 86;

                    then k < x by A23, A26, Th33;

                    hence contradiction by A24, NAT_1: 13;

                  end;

                end;

                hence contradiction;

              end;

                suppose

                 A27: not k in ( dom p);

                

                 A28: k < (k + 1) by XREAL_1: 29;

                ( len p) <= k by A27, AFINSQ_1: 86;

                then ( len p) < (k + 1) by A28, XXREAL_0: 2;

                hence contradiction by A9, AFINSQ_1: 86;

              end;

            end;

            hence contradiction;

          end;

        end;

         0 < ( len p) implies X1 <> {} by Th20, CARD_1: 27;

        then

         A29: P[ 0 ] by A1, Th34;

        

         A30: for k holds P[k] from NAT_1:sch 2( A29, A7);

        defpred P[ Nat] means $1 in ( dom q) implies (r . (( len p) + $1)) = (q . $1);

         A31:

        now

          let k;

          assume

           A32: P[k];

          thus P[(k + 1)]

          proof

            set n = (q . (k + 1));

            set a = (( len p) + (k + 1));

            set m = (r . a);

            assume

             A33: (k + 1) in ( dom q);

            then (q . (k + 1)) in ( rng q) by FUNCT_1:def 3;

            then

             A34: n in Y by Def4;

            (k + 1) < ( len q) by A33, AFINSQ_1: 86;

            then

             A35: a < ( len r) by A6, XREAL_1: 6;

            then

             A36: a in ( dom r) by AFINSQ_1: 86;

            then (r . a) in ( rng r) by FUNCT_1:def 3;

            then

             A37: m in (X \/ Y) by Def4;

             A38:

            now

              

               A39: ( len p) <= ( len r) by A6, NAT_1: 12;

              assume m in X;

              then m in ( rng p) by Def4;

              then

              consider x be object such that

               A40: x in ( dom p) and

               A41: (p . x) = m by FUNCT_1:def 3;

              reconsider x as Element of NAT by A40;

              x < ( len p) by A40, AFINSQ_1: 86;

              then x < ( len r) by A39, XXREAL_0: 2;

              then

               A42: x in ( dom r) by AFINSQ_1: 86;

              (r . x) = (r . a) by A30, A40, A41;

              then x = a by A36, A42, FUNCT_1:def 4;

              then (( len p) + (k + 1)) <= (( len p) + 0 qua Element of NAT ) by A40, AFINSQ_1: 86;

              hence contradiction by XREAL_1: 29;

            end;

            assume

             A43: (r . (( len p) + (k + 1))) <> (q . (k + 1));

            now

              per cases ;

                suppose

                 A44: k in ( dom q);

                set m1 = (r . (( len p) + k));

                set n1 = (q . k);

                

                 A45: k < ( len q) by A44, AFINSQ_1: 86;

                now

                  per cases by A43, XXREAL_0: 1;

                    suppose

                     A46: m < n;

                    m in Y by A37, A38, XBOOLE_0:def 3;

                    then m in ( rng q) by Def4;

                    then

                    consider x be object such that

                     A47: x in ( dom q) and

                     A48: (q . x) = m by FUNCT_1:def 3;

                    reconsider x as Element of NAT by A47;

                    x < ( len q) by A47, AFINSQ_1: 86;

                    then

                     A49: x < (k + 1) by A46, A48, Th33;

                    (( len p) + k) < ((( len p) + k) + 1) by XREAL_1: 29;

                    then

                     A50: n1 < m by A32, A35, A44, Def4;

                    k < ( len q) by A44, AFINSQ_1: 86;

                    then k < x by A48, A50, Th33;

                    hence contradiction by A49, NAT_1: 13;

                  end;

                    suppose

                     A51: n < m;

                    n in (X \/ Y) by A34, XBOOLE_0:def 3;

                    then n in ( rng r) by Def4;

                    then

                    consider x be object such that

                     A52: x in ( dom r) and

                     A53: (r . x) = n by FUNCT_1:def 3;

                    reconsider x as Element of NAT by A52;

                    x < ( len r) by A52, AFINSQ_1: 86;

                    then

                     A54: x < ((( len p) + k) + 1) by A51, A53, Th33;

                    

                     A55: k < (k + 1) by XREAL_1: 29;

                    (k + 1) < ( len q) by A33, AFINSQ_1: 86;

                    then

                     A56: m1 < n by A32, A44, A55, Def4;

                    (( len p) + k) < ( len r) by A6, A45, XREAL_1: 6;

                    then (( len p) + k) < x by A53, A56, Th33;

                    hence contradiction by A54, NAT_1: 13;

                  end;

                end;

                hence contradiction;

              end;

                suppose

                 A57: not k in ( dom q);

                

                 A58: k < (k + 1) by XREAL_1: 29;

                ( len q) <= k by A57, AFINSQ_1: 86;

                hence contradiction by A33, AFINSQ_1: 86, A58, XXREAL_0: 2;

              end;

            end;

            hence contradiction;

          end;

        end;

        ( len q) > 0 implies Y <> {} by Th20, CARD_1: 27;

        then

         A59: P[ 0 ] by A1, Th32;

        for k holds P[k] from NAT_1:sch 2( A59, A31);

        hence thesis by A6, A30, AFINSQ_1:def 3;

      end;

      assume

       A60: ( Sgm0 (X \/ Y)) = (( Sgm0 X) ^ ( Sgm0 Y));

      let m,n be Nat;

      assume that

       A61: m in X and

       A62: n in Y;

      n in ( rng q) by A62, Def4;

      then

      consider y be object such that

       A63: y in ( dom q) and

       A64: (q . y) = n by FUNCT_1:def 3;

      reconsider y as Element of NAT by A63;

      

       A65: n = (r . (( len p) + y)) by A60, A63, A64, AFINSQ_1:def 3;

      y < ( len q) by A63, AFINSQ_1: 86;

      then (( len p) + y) < (( len p) + ( len q)) by XREAL_1: 6;

      then

       A66: (( len p) + y) < ( len r) by A60, AFINSQ_1: 17;

      

       A67: ( len p) <= (( len p) + y) by NAT_1: 12;

      m in ( rng ( Sgm0 X)) by A61, Def4;

      then

      consider x be object such that

       A68: x in ( dom p) and

       A69: (p . x) = m by FUNCT_1:def 3;

      reconsider x as Element of NAT by A68;

      x < ( len p) by A68, AFINSQ_1: 86;

      then

       A70: x < (( len p) + y) by A67, XXREAL_0: 2;

      m = (r . x) by A60, A68, A69, AFINSQ_1:def 3;

      hence thesis by A65, A70, A66, Def4;

    end;

    definition

      let f be XFinSequence;

      let B be set;

      :: AFINSQ_2:def7

      func SubXFinS (f,B) -> XFinSequence equals (f * ( Sgm0 (B /\ ( Segm ( len f)))));

      coherence

      proof

        (B /\ ( Segm ( len f))) c= ( dom f) by XBOOLE_1: 17;

        then ( rng ( Sgm0 (B /\ ( Segm ( len f))))) c= ( dom f) by Def4;

        hence thesis by AFINSQ_1: 10;

      end;

    end

    theorem :: AFINSQ_2:36

    

     Th36: for B be set holds ( len ( SubXFinS (p,B))) = ( card (B /\ ( Segm ( len p)))) & for i st i < ( len ( SubXFinS (p,B))) holds (( SubXFinS (p,B)) . i) = (p . (( Sgm0 (B /\ ( Segm ( len p)))) . i))

    proof

      let B be set;

      (B /\ ( Segm ( len p))) c= ( dom p) by XBOOLE_1: 17;

      then ( rng ( Sgm0 (B /\ ( Segm ( len p))))) c= ( dom p) by Def4;

      

      then ( dom ( SubXFinS (p,B))) = ( len ( Sgm0 (B /\ ( Segm ( len p))))) by RELAT_1: 27

      .= ( card (B /\ ( Segm ( len p)))) by Th20;

      hence ( len ( SubXFinS (p,B))) = ( card (B /\ ( Segm ( len p))));

      let i;

      assume i < ( len ( SubXFinS (p,B)));

      hence thesis by FUNCT_1: 12, AFINSQ_1: 86;

    end;

    registration

      let D be set;

      let f be XFinSequence of D, B be set;

      cluster ( SubXFinS (f,B)) -> D -valued;

      coherence ;

    end

    registration

      let p;

      cluster ( SubXFinS (p, {} )) -> empty;

      coherence

      proof

        ( len ( SubXFinS (p, {} ))) = ( card {} ) by Th36;

        hence thesis;

      end;

    end

    registration

      let B be set;

      cluster ( SubXFinS ( {} ,B)) -> empty;

      coherence ;

    end

    reserve D for non empty set,

F,G for XFinSequence of D,

b for BinOp of D,

d,d1,d2 for Element of D;

    scheme :: AFINSQ_2:sch2

    Sch5 { D() -> set , P[ set] } :

for F be XFinSequence of D() holds P[F]

      provided

       A1: P[( <%> D())]

       and

       A2: for F be XFinSequence of D(), d be Element of D() st P[F] holds P[(F ^ <%d%>)];

      defpred R[ set] means for F be XFinSequence of D() st ( len F) = $1 holds P[F];

      

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

      proof

        let n such that

         A4: for F be XFinSequence of D() st ( len F) = n holds P[F];

        let F be XFinSequence of D();

        assume

         A5: ( len F) = (n + 1);

        then F <> {} ;

        then

        consider G be XFinSequence, d be object such that

         A6: F = (G ^ <%d%>) by AFINSQ_1: 40;

        reconsider G, dd = <%d%> as XFinSequence of D() by A6, AFINSQ_1: 31;

        

         A7: ( rng dd) c= D() & ( rng dd) = {d} & d in {d} by AFINSQ_1: 33, TARSKI:def 1;

        ( len dd) = 1 by AFINSQ_1: 34;

        then ( len F) = (( len G) + 1) by A6, AFINSQ_1: 17;

        hence thesis by A2, A4, A5, A6, A7;

      end;

      let F be XFinSequence of D();

      

       A8: ( len F) = ( len F);

      ( card X) = {} implies X = {} ;

      then

       A9: R[ 0 ] by A1;

      for n holds R[n] from NAT_1:sch 2( A9, A3);

      hence thesis by A8;

    end;

    definition

      let D;

      let F be XFinSequence;

      assume

       A1: F is D -valued;

      let b;

      assume

       A2: b is having_a_unity or ( len F) >= 1;

      :: AFINSQ_2:def8

      func b "**" F -> Element of D means

      : Def8: it = ( the_unity_wrt b) if b is having_a_unity & ( len F) = 0

      otherwise ex f be sequence of D st (f . 0 ) = (F . 0 ) & (for n st (n + 1) < ( len F) holds (f . (n + 1)) = (b . ((f . n),(F . (n + 1))))) & it = (f . (( len F) - 1));

      existence

      proof

        now

          per cases ;

            suppose ( len F) = 0 ;

            hence thesis by A2;

          end;

            suppose

             A3: ( len F) <> 0 ;

            defpred P[ Nat] means for F st ( len F) = $1 & ( len F) <> 0 holds ex d be Element of D, f be sequence of D st (f . 0 ) = (F . 0 ) & (for n st (n + 1) < ( len F) holds (f . (n + 1)) = (b . ((f . n),(F . (n + 1))))) & d = (f . (( len F) - 1));

            

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

            proof

              let k such that

               A5: P[k];

              let F such that

               A6: ( len F) = (k + 1) and ( len F) <> 0 ;

              set G = (F | k);

              

               A7: k < (k + 1) by NAT_1: 13;

              then

               A8: ( len G) = k by A6, AFINSQ_1: 11;

              now

                per cases ;

                  suppose

                   A9: ( len G) = 0 ;

                  then 0 in ( dom F) by A6, A8, CARD_1: 49, TARSKI:def 1;

                  then

                   A10: (F . 0 ) in ( rng F) by FUNCT_1:def 3;

                  reconsider f = ( NAT --> (F . 0 )) as sequence of D by A10, FUNCOP_1: 45;

                  take d = (f . 0 ), f;

                  thus (f . 0 ) = (F . 0 ) by FUNCOP_1: 7;

                  thus for n st (n + 1) < ( len F) holds (f . (n + 1)) = (b . ((f . n),(F . (n + 1)))) by A6, A8, A9, NAT_1: 14;

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

                  hence d = (f . (( len F) - 1)) by A6, A9, AFINSQ_1: 11;

                end;

                  suppose

                   A11: ( len G) <> 0 ;

                  k < ( len F) by A6, NAT_1: 13;

                  then k in ( dom F) by AFINSQ_1: 86;

                  then

                   A12: (F . k) in ( rng F) by FUNCT_1:def 3;

                  reconsider d1 = (F . k) as Element of D by A12;

                  

                   A13: 0 in ( len G) by A11, AFINSQ_1: 86;

                  consider d be Element of D, f be sequence of D such that

                   A14: (f . 0 ) = (G . 0 ) and

                   A15: for n st (n + 1) < ( len G) holds (f . (n + 1)) = (b . ((f . n),(G . (n + 1)))) and

                   A16: d = (f . (( len G) - 1)) by A5, A6, A7, A11, AFINSQ_1: 11;

                  deffunc F( Element of NAT ) = (f . $1);

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

                  consider h be sequence of D such that

                   A17: (h . K) = (b . (d,d1)) and

                   A18: for n be Element of NAT st n <> K holds (h . n) = F(n) from FUNCT_2:sch 6;

                  take a = (h . k), h;

                  (h . 0 ) = (f . 0 ) by A8, A11, A18;

                  hence (h . 0 ) = (F . 0 ) by A14, A13, FUNCT_1: 47;

                  thus for n st (n + 1) < ( len F) holds (h . (n + 1)) = (b . ((h . n),(F . (n + 1))))

                  proof

                    let n;

                    assume (n + 1) < ( len F);

                    then

                     A19: (n + 1) <= ( len G) by A6, A8, NAT_1: 13;

                    now

                      per cases by A19, XXREAL_0: 1;

                        suppose

                         A20: (n + 1) = ( len G);

                        then

                         A21: n < k by A8, NAT_1: 13;

                        (n + 1) = k & n in NAT by A6, A7, A20, AFINSQ_1: 11, ORDINAL1:def 12;

                        hence thesis by A16, A17, A18, A20, A21;

                      end;

                        suppose

                         A22: (n + 1) < ( len G);

                        then

                         A23: (G . (n + 1)) = (F . (n + 1)) by FUNCT_1: 47, AFINSQ_1: 86;

                        n <= (n + 1) & n in NAT by NAT_1: 11, ORDINAL1:def 12;

                        then

                         A24: (f . n) = (h . n) by A8, A18, A22;

                        (f . (n + 1)) = (h . (n + 1)) by A8, A18, A22;

                        hence thesis by A15, A22, A23, A24;

                      end;

                    end;

                    hence thesis;

                  end;

                  thus a = (h . (( len F) - 1)) by A6;

                end;

              end;

              hence thesis;

            end;

            

             A25: P[ 0 ];

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

            hence thesis by A1, A3;

          end;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let d1,d2 be Element of D;

        thus b is having_a_unity & ( len F) = 0 & d1 = ( the_unity_wrt b) & d2 = ( the_unity_wrt b) implies d1 = d2;

        

         A26: ((( len F) - 1) + 1) = ( len F);

        assume not b is having_a_unity or ( len F) <> 0 ;

        then 0 < ( len F) by A2;

        then

         A27: (( len F) - 1) is Element of NAT by NAT_1: 20;

        given f1 be sequence of D such that

         A28: (f1 . 0 ) = (F . 0 ) and

         A29: for n st (n + 1) < ( len F) holds (f1 . (n + 1)) = (b . ((f1 . n),(F . (n + 1)))) and

         A30: d1 = (f1 . (( len F) - 1));

        given f2 be sequence of D such that

         A31: (f2 . 0 ) = (F . 0 ) and

         A32: for n st (n + 1) < ( len F) holds (f2 . (n + 1)) = (b . ((f2 . n),(F . (n + 1)))) and

         A33: d2 = (f2 . (( len F) - 1));

        defpred P[ Nat] means ($1 + 1) <= ( len F) implies (f1 . $1) = (f2 . $1);

        

         A34: P[n] implies P[(n + 1)]

        proof

          assume

           A35: P[n];

          assume ((n + 1) + 1) <= ( len F);

          then

           A36: (n + 1) < ( len F) by NAT_1: 13;

          then (f2 . (n + 1)) = (b . ((f2 . n),(F . (n + 1)))) by A32;

          hence thesis by A29, A35, A36;

        end;

        

         A37: P[ 0 ] by A28, A31;

        for n holds P[n] from NAT_1:sch 2( A37, A34);

        hence thesis by A30, A33, A26, A27;

      end;

      consistency ;

    end

    theorem :: AFINSQ_2:37

    

     Th37: (b "**" <%d%>) = d

    proof

      ( len <%d%>) = 1 by AFINSQ_1: 33;

      then ex f be sequence of D st (f . 0 ) = ( <%d%> . 0 ) & (for n st (n + 1) < ( len <%d%>) holds (f . (n + 1)) = (b . ((f . n),( <%d%> . (n + 1))))) & (b "**" <%d%>) = (f . (1 - 1)) by Def8;

      hence thesis;

    end;

    reconsider zz = 0 as Nat;

    theorem :: AFINSQ_2:38

    

     Th38: (b "**" <%d1, d2%>) = (b . (d1,d2))

    proof

      ( len <%d1, d2%>) = 2 by AFINSQ_1: 38;

      then

      consider f be sequence of D such that

       A1: (f . 0 ) = ( <%d1, d2%> . 0 ) and

       A2: for n st (n + 1) < 2 holds (f . (n + 1)) = (b . ((f . n),( <%d1, d2%> . (n + 1)))) and

       A3: (b "**" <%d1, d2%>) = (f . (2 - 1)) by Def8;

      (f . (zz + 1)) = (b . ((f . zz),( <%d1, d2%> . (zz + 1)))) by A2;

      hence thesis by A1, A3;

    end;

    theorem :: AFINSQ_2:39

    

     Th39: (b "**" <%d, d1, d2%>) = (b . ((b . (d,d1)),d2))

    proof

      set F = <%d, d1, d2%>;

      ( len F) = 3 by AFINSQ_1: 39;

      then

      consider f be sequence of D such that

       A1: (f . 0 ) = (F . 0 ) and

       A2: for n st (n + 1) < 3 holds (f . (n + 1)) = (b . ((f . n),(F . (n + 1)))) and

       A3: (b "**" F) = (f . (3 - 1)) by Def8;

      

       A4: (f . (1 + 1)) = (b . ((f . 1),(F . (1 + 1)))) by A2;

      (f . (zz + 1)) = (b . ((f . zz),(F . (zz + 1)))) by A2;

      hence thesis by A1, A3, A4;

    end;

    theorem :: AFINSQ_2:40

    

     Th40: b is having_a_unity or ( len F) > 0 implies (b "**" (F ^ <%d%>)) = (b . ((b "**" F),d))

    proof

      assume

       A1: b is having_a_unity or ( len F) > 0 ;

      now

        per cases ;

          suppose

           A2: ( len F) < (zz + 1);

          then

           A3: F = {} by NAT_1: 13;

          

           A4: (b "**" (F ^ <%d%>)) = d by Th37, A3;

          ( len F) = 0 by A2, NAT_1: 13;

          then (b "**" F) = ( the_unity_wrt b) by A1, Def8;

          hence thesis by A1, A2, A4, NAT_1: 13, SETWISEO: 15;

        end;

          suppose

           A5: ( len F) >= 1;

          set G = (F ^ <%d%>);

          reconsider lenF1 = (( len F) - 1) as Element of NAT by A5, NAT_1: 21;

          

           A6: (G . ( len F)) = d by AFINSQ_1: 36;

          

           A7: ( len G) = (( len F) + ( len <%d%>)) by AFINSQ_1: 17

          .= (( len F) + 1) by AFINSQ_1: 33;

          then 1 <= ( len G) by NAT_1: 12;

          then

          consider f1 be sequence of D such that

           A8: (f1 . 0 ) = (G . 0 ) and

           A9: for n st (n + 1) < ( len G) holds (f1 . (n + 1)) = (b . ((f1 . n),(G . (n + 1)))) and

           A10: (b "**" G) = (f1 . (( len G) - 1)) by Def8;

          consider f be sequence of D such that

           A11: (f . 0 ) = (F . 0 ) and

           A12: for n st (n + 1) < ( len F) holds (f . (n + 1)) = (b . ((f . n),(F . (n + 1)))) and

           A13: (b "**" F) = (f . (( len F) - 1)) by A5, Def8;

          defpred P[ Nat] means ($1 + 1) < ( len G) implies (f . $1) = (f1 . $1);

          

           A14: P[n] implies P[(n + 1)]

          proof

            assume

             A15: P[n];

            set n1 = (n + 1);

            assume

             A16: (n1 + 1) < ( len G);

            then

             A17: (f1 . n1) = (b . ((f1 . n),(G . (n + 1)))) by A9, NAT_1: 13;

            

             A18: ((n1 + 1) + ( - 1)) < ((( len F) + 1) + ( - 1)) by A7, A16, XREAL_1: 8;

            then

             A19: n1 in ( len F) by AFINSQ_1: 86;

            (f . n1) = (b . ((f . n),(F . n1))) by A12, A18;

            hence thesis by A15, A16, A17, A19, AFINSQ_1:def 3, NAT_1: 13;

          end;

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

          then

           A20: P[ 0 ] by A11, A8, AFINSQ_1:def 3;

          

           A21: for n holds P[n] from NAT_1:sch 2( A20, A14);

          

           A22: (lenF1 + 1) < ( len G) by A7, NAT_1: 13;

          then (b "**" G) = (b . ((f1 . lenF1),(G . (lenF1 + 1)))) by A7, A9, A10;

          hence thesis by A13, A21, A22, A6;

        end;

      end;

      hence thesis;

    end;

    ::$Canceled

    theorem :: AFINSQ_2:42

    

     Th41: b is associative & (b is having_a_unity or ( len F) >= 1 & ( len G) >= 1) implies (b "**" (F ^ G)) = (b . ((b "**" F),(b "**" G)))

    proof

      defpred P[ XFinSequence of D] means for F, b st b is associative & (b is having_a_unity or ( len F) >= 1 & ( len $1) >= 1) holds (b "**" (F ^ $1)) = (b . ((b "**" F),(b "**" $1)));

      

       A1: for G, d st P[G] holds P[(G ^ <%d%>)]

      proof

        let G, d such that

         A2: P[G];

        let F, b such that

         A3: b is associative and

         A4: b is having_a_unity or ( len F) >= 1 & ( len (G ^ <%d%>)) >= 1;

        now

          per cases ;

            suppose

             A5: ( len G) <> 0 ;

            then b is having_a_unity or ( len F) >= 1 & ( len (F ^ G)) = (( len F) + ( len G)) & (( len F) + ( len G)) > (( len F) + zz) by A4, AFINSQ_1: 17, XREAL_1: 8;

            then (b . ((b "**" (F ^ G)),d)) = (b "**" ((F ^ G) ^ <%d%>)) by Th40;

            then

             A6: (b "**" (F ^ (G ^ <%d%>))) = (b . ((b "**" (F ^ G)),d)) by AFINSQ_1: 27;

            ( len G) >= 1 by A5, NAT_1: 14;

            

            then (b "**" (F ^ (G ^ <%d%>))) = (b . ((b . ((b "**" F),(b "**" G))),d)) by A2, A3, A4, A6

            .= (b . ((b "**" F),(b . ((b "**" G),d)))) by A3

            .= (b . ((b "**" F),(b "**" (G ^ <%d%>)))) by A5, Th40;

            hence thesis;

          end;

            suppose ( len G) = 0 ;

            then

             A7: G = {} ;

            

            hence (b "**" (F ^ (G ^ <%d%>))) = (b "**" (F ^ ( {} ^ <%d%>)))

            .= (b "**" (F ^ <%d%>))

            .= (b . ((b "**" F),d)) by A4, Th40

            .= (b . ((b "**" F),(b "**" ( {} ^ <%d%>)))) by Th37

            .= (b . ((b "**" F),(b "**" (G ^ <%d%>)))) by A7;

          end;

        end;

        hence thesis;

      end;

      

       A8: P[( <%> D)]

      proof

        let F, b;

        assume that b is associative and

         A9: b is having_a_unity or ( len F) >= 1 & ( len ( <%> D)) >= 1;

        

        thus (b "**" (F ^ ( <%> D))) = (b "**" (F ^ {} ))

        .= (b . ((b "**" F),( the_unity_wrt b))) by A9, SETWISEO: 15

        .= (b . ((b "**" F),(b "**" ( <%> D)))) by A9, Def8, CARD_1: 27;

      end;

      for G holds P[G] from Sch5( A8, A1);

      hence thesis;

    end;

    theorem :: AFINSQ_2:43

    

     Th42: n in ( dom F) & (b is having_a_unity or n <> 0 ) implies (b . ((b "**" (F | n)),(F . n))) = (b "**" (F | (n + 1)))

    proof

      assume that

       A1: n in ( dom F) and

       A2: b is having_a_unity or n <> 0 ;

      ( len F) > n by A1, AFINSQ_1: 86;

      then

       A3: ( len (F | n)) = n by AFINSQ_1: 54;

      defpred P[ Nat] means $1 in ( dom F) & (b is having_a_unity or ( len (F | $1)) >= 1) implies (b . ((b "**" (F | $1)),(F . $1))) = (b "**" (F | ($1 + 1)));

      

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

      proof

        let k such that P[k];

        set k1 = (k + 1);

        set Fk1 = (F | k1);

        set Fk2 = (F | (k1 + 1));

        assume that

         A5: k1 in ( dom F) and

         A6: b is having_a_unity or ( len Fk1) >= 1;

         0 < ( len F) by A5;

        then

         A7: 0 in ( dom F) by AFINSQ_1: 86;

         0 in ( Segm k1) by NAT_1: 44;

        then 0 in (( dom F) /\ k1) by A7, XBOOLE_0:def 4;

        then 0 in ( dom Fk1) by RELAT_1: 61;

        then

         A8: (Fk1 . 0 ) = (F . 0 ) by FUNCT_1: 47;

        

         A9: k < k1 by NAT_1: 13;

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

        then k1 in ( Segm (k1 + 1)) by NAT_1: 44;

        then

         A10: k1 in (( dom F) /\ (k1 + 1)) by A5, XBOOLE_0:def 4;

        

         A12: k1 < ( len F) by A5, AFINSQ_1: 86;

        then

         A13: ( len Fk1) = k1 by AFINSQ_1: 54;

        then

        consider f1 be sequence of D such that

         A14: (f1 . 0 ) = (Fk1 . 0 ) and

         A15: for n st (n + 1) < ( len Fk1) holds (f1 . (n + 1)) = (b . ((f1 . n),(Fk1 . (n + 1)))) and

         A16: (b "**" Fk1) = (f1 . (k1 - 1)) by A6, Def8;

        (k1 + 1) <= ( dom F) by A12, NAT_1: 13;

        then

         A17: ( len Fk2) = (k1 + 1) by AFINSQ_1: 54;

        then b is having_a_unity or ( len Fk2) >= 1 by A6, A13, NAT_1: 13;

        then

        consider f2 be sequence of D such that

         A18: (f2 . 0 ) = (Fk2 . 0 ) and

         A19: for n st (n + 1) < ( len Fk2) holds (f2 . (n + 1)) = (b . ((f2 . n),(Fk2 . (n + 1)))) and

         A20: (b "**" Fk2) = (f2 . ((k1 + 1) - 1)) by A17, Def8;

        defpred R[ Nat] means $1 < k1 implies (f1 . $1) = (f2 . $1);

        

         A21: for m st R[m] holds R[(m + 1)]

        proof

          let m such that

           A22: R[m];

          set m1 = (m + 1);

          assume

           A23: m1 < k1;

          k1 < ( len F) by A5, AFINSQ_1: 86;

          then m1 < ( len F) by A23, XXREAL_0: 2;

          then

           A24: m1 in ( dom F) by AFINSQ_1: 86;

          m1 < (k1 + 1) by A23, NAT_1: 13;

          then m1 in ( Segm (k1 + 1)) by NAT_1: 44;

          then m1 in (( dom F) /\ ( Segm (k1 + 1))) by A24, XBOOLE_0:def 4;

          then m1 in ( dom Fk2) by RELAT_1: 61;

          then

           A25: (Fk2 . m1) = (F . m1) by FUNCT_1: 47;

          m1 in ( Segm k1) by A23, NAT_1: 44;

          then m1 in (( dom F) /\ ( Segm k1)) by A24, XBOOLE_0:def 4;

          then m1 in ( dom Fk1) by RELAT_1: 61;

          then

           A26: (Fk1 . m1) = (F . m1) by FUNCT_1: 47;

          m1 < ( len Fk2) by A17, A23, NAT_1: 13;

          then (f2 . m1) = (b . ((f1 . m),(Fk1 . m1))) by A19, A22, A23, A26, A25, NAT_1: 13;

          hence thesis by A13, A15, A23;

        end;

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

        then 0 in (( dom F) /\ (k1 + 1)) by A7, XBOOLE_0:def 4;

        then 0 in ( dom Fk2) by RELAT_1: 61;

        then

         A27: R[ 0 ] by A14, A18, A8, FUNCT_1: 47;

        for m holds R[m] from NAT_1:sch 2( A27, A21);

        then

         A28: (( dom F) /\ (k1 + 1)) = ( dom Fk2) & (f1 . k) = (f2 . k) by A9, RELAT_1: 61;

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

        then (f2 . k1) = (b . ((f2 . k),(Fk2 . k1))) by A17, A19;

        hence thesis by A16, A20, A10, A28, FUNCT_1: 47;

      end;

      

       A29: P[ 0 ]

      proof

        assume that

         A30: 0 in ( dom F) and

         A31: b is having_a_unity or ( len (F | 0 qua Ordinal)) >= 1;

        

         A32: (F . 0 ) in ( rng F) by A30, FUNCT_1:def 3;

        ( len F) > 0 by A30;

        then

         A33: ( len (F | 1)) = 1 by AFINSQ_1: 54, NAT_1: 14;

        then

         A34: (F | 1) = <%((F | 1) . 0 )%> by AFINSQ_1: 34;

         0 in ( Segm 1) by NAT_1: 44;

        then

         A35: (F . 0 ) = ((F | 1) . 0 ) by A33, FUNCT_1: 47;

        ( len (F | 0 qua Ordinal)) = 0 ;

        then (b "**" (F | 0 qua Ordinal)) = ( the_unity_wrt b) by A31, Def8;

        then (b . ((b "**" (F | 0 qua Ordinal)),(F . 0 ))) = (F . 0 ) by A31, A32, SETWISEO: 15;

        hence thesis by A32, A34, A35, Th37;

      end;

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

      hence thesis by A1, A2, A3, NAT_1: 14;

    end;

    theorem :: AFINSQ_2:44

    

     Th43: b is having_a_unity or ( len F) >= 1 implies (b "**" F) = (b "**" ( XFS2FS F))

    proof

      assume

       A1: b is having_a_unity or ( len F) >= 1;

      per cases by A1;

        suppose

         A2: ( len F) >= 1;

        set FS = ( XFS2FS F);

        ( len F) = ( len FS) by AFINSQ_1:def 9;

        then

        consider f be sequence of D such that

         A3: (f . 1) = (FS . 1) and

         A4: for n be Nat st 0 <> n & n < ( len F) holds (f . (n + 1)) = (b . ((f . n),(FS . (n + 1)))) and

         A5: (b "**" FS) = (f . ( len F)) by A2, FINSOP_1:def 1;

        consider xf be sequence of D such that

         A6: (xf . 0 ) = (F . 0 ) and

         A7: for n st (n + 1) < ( len F) holds (xf . (n + 1)) = (b . ((xf . n),(F . (n + 1)))) and

         A8: (b "**" F) = (xf . (( len F) - 1)) by A2, Def8;

        defpred P[ Nat] means $1 < ( len F) implies (xf . $1) = (f . ($1 + 1));

        

         A9: for n st P[n] holds P[(n + 1)]

        proof

          let n such that

           A10: P[n];

          set n1 = (n + 1);

          set n2 = (n1 + 1);

          assume

           A11: n1 < ( len F);

          then (zz + 1) <= n2 & n2 <= ( len F) by NAT_1: 13;

          then

           A12: (F . (n2 -' 1)) = (FS . n2) by AFINSQ_1:def 9;

          (xf . n1) = (b . ((xf . n),(F . n1))) & (f . (n1 + 1)) = (b . ((f . n1),(FS . (n1 + 1)))) by A7, A4, A11;

          hence thesis by A10, A11, A12, NAT_1: 13, NAT_D: 34;

        end;

        reconsider L1 = (( len F) - 1) as Element of NAT by A2, NAT_1: 21;

        

         A13: L1 < (L1 + 1) by NAT_1: 13;

        

         A14: P[ 0 ]

        proof

          assume 0 < ( len F);

          then (zz + 1) <= ( len F) by NAT_1: 13;

          then (F . (1 -' 1)) = (FS . 1) by AFINSQ_1:def 9;

          hence thesis by A6, A3, XREAL_1: 232;

        end;

        for n holds P[n] from NAT_1:sch 2( A14, A9);

        hence thesis by A8, A5, A13;

      end;

        suppose

         A15: b is having_a_unity & ( len F) < 1;

        then ( len F) <= (zz + 1);

        then

         A16: ( len F) = 0 by A15, NAT_1: 8;

        then ( len F) = ( len ( XFS2FS F)) & (b "**" F) = ( the_unity_wrt b) by A15, Def8, AFINSQ_1:def 9;

        hence thesis by A15, A16, FINSOP_1:def 1;

      end;

    end;

    theorem :: AFINSQ_2:45

    

     Th44: for P be Permutation of ( dom F) st b is commutative associative & (b is having_a_unity or ( len F) >= 1) & G = (F * P) holds (b "**" F) = (b "**" G)

    proof

      let P be Permutation of ( dom F) such that

       A1: b is commutative associative and

       A2: b is having_a_unity or ( len F) >= 1 and

       A3: G = (F * P);

      set xF = ( XFS2FS F);

      

       A4: b is having_a_unity or ( len xF) >= 1 by A2, AFINSQ_1:def 9;

      set xG = ( XFS2FS G);

      defpred p[ object, object] means for n st $1 = n holds $2 = ((P . (n - 1)) + 1);

      ( dom F) = ( len F);

      then

      reconsider d = ( dom F) as Element of NAT ;

      

       A6: for x be object st x in ( Seg d) holds ex y be object st y in ( Seg d) & p[x, y]

      proof

        let x be object such that

         A7: x in ( Seg d);

        reconsider x9 = x as Element of NAT by A7;

        (1 + zz) <= x9 by A7, FINSEQ_1: 1;

        then

        reconsider x91 = (x9 - 1) as Element of NAT by NAT_1: 21;

        

         A8: (x91 + 1) <= d by A7, FINSEQ_1: 1;

        then x91 < d by NAT_1: 13;

        then

         A9: x91 in ( Segm d) by NAT_1: 44;

        take ((P . x91) + 1);

        ( dom F) = ( dom P) by A8, FUNCT_2:def 1;

        then (P . x91) in ( rng P) by A9, FUNCT_1:def 3;

        then (P . x91) < d by AFINSQ_1: 86;

        then (zz + 1) <= ((P . x91) + 1) & ((P . x91) + 1) <= d by NAT_1: 13;

        hence thesis by FINSEQ_1: 1;

      end;

      consider P9 be Function of ( Seg d), ( Seg d) such that

       A10: for x be object st x in ( Seg d) holds p[x, (P9 . x)] from FUNCT_2:sch 1( A6);

      now

        let x1,x2 be object such that

         A11: x1 in ( dom P9) and

         A12: x2 in ( dom P9) and

         A13: (P9 . x1) = (P9 . x2);

        ( dom P9) = ( Seg d) by FUNCT_2: 52;

        then

        reconsider X1 = x1, X2 = x2 as Element of NAT by A11, A12;

        (1 + zz) <= X1 & (1 + zz) <= X2 by A11, A12, FINSEQ_1: 1;

        then

        reconsider X19 = (X1 - 1), X29 = (X2 - 1) as Element of NAT by NAT_1: 21;

        

         A14: X19 < (X19 + 1) & X1 <= d by A11, FINSEQ_1: 1, NAT_1: 13;

        then

         A15: ( dom P) = ( dom F) by FUNCT_2:def 1;

        X29 < (X29 + 1) & X2 <= d by A12, FINSEQ_1: 1, NAT_1: 13;

        then X29 < d by XXREAL_0: 2;

        then

         A16: X29 in ( dom P) by A15, AFINSQ_1: 86;

        X19 < d by A14, XXREAL_0: 2;

        then

         A17: X19 in ( dom P) by A15, AFINSQ_1: 86;

        (P9 . X1) = ((P . X19) + 1) by A10, A11;

        then (((P . X19) + 1) - 1) = (((P . X29) + 1) - 1) by A10, A12, A13;

        then ((X1 - 1) + 1) = ((X2 - 1) + 1) by A17, A16, FUNCT_1:def 4;

        hence x1 = x2;

      end;

      then

       A18: P9 is one-to-one;

      ( card ( Seg d)) = ( card ( Seg d));

      then

       A19: P9 is one-to-one onto by A18, Lm1;

      ( len xF) = ( len F) by AFINSQ_1:def 9;

      then ( dom xF) = ( Seg ( len F)) by FINSEQ_1:def 3;

      then

      reconsider P9 as Permutation of ( dom xF) by A19;

      

       A20: ( dom P9) = ( Seg d) & ( dom xG) = ( Seg ( len xG)) by FINSEQ_1:def 3, FUNCT_2: 52;

      ( rng P9) c= ( dom xF);

      then

       A21: ( dom (xF * P9)) = ( dom P9) by RELAT_1: 27;

      ( rng P) c= ( dom F);

      then ( dom (F * P)) = ( dom P) by RELAT_1: 27;

      then

       A22: ( dom G) = ( dom F) by A3, FUNCT_2: 52;

      

       A24: for x9 be object st x9 in ( dom xG) holds (xG . x9) = ((xF * P9) . x9)

      proof

        let x9 be object such that

         A25: x9 in ( dom xG);

        reconsider x = x9 as Element of NAT by A25;

        

         A26: ( dom xG) = ( Seg ( len xG)) by FINSEQ_1:def 3;

        then

         A27: 1 <= x by A25, FINSEQ_1: 1;

        then

         A28: (x -' 1) = (x - 1) by XREAL_1: 233;

         0 < x by A25, A26, FINSEQ_1: 1;

        then

        reconsider x1 = (x - 1) as Element of NAT by NAT_1: 20;

        

         A29: ( dom xF) = ( Seg ( len xF)) by FINSEQ_1:def 3;

        

         A30: ( len xG) = ( len G) by AFINSQ_1:def 9;

        then

         A31: ((P . (x - 1)) + 1) = (P9 . x) & x in ( dom P9) by A10, A22, A25, A26, FUNCT_2: 52;

        then

         A32: ((P . (x - 1)) + 1) in ( rng P9) by FUNCT_1:def 3;

        

         A33: x <= ( len F) by A22, A25, A26, A30, FINSEQ_1: 1;

        then

         A34: (xG . x) = ((F * P) . (x -' 1)) by A3, A22, A27, AFINSQ_1:def 9;

        ( len xF) = ( len F) by AFINSQ_1:def 9;

        then

         A35: ((P . (x - 1)) + 1) <= ( len F) by A32, A29, FINSEQ_1: 1;

        x1 < (x1 + 1) & (x -' 1) = x1 by A27, NAT_1: 13, XREAL_1: 233;

        then (x -' 1) < ( len G) by A22, A33, XXREAL_0: 2;

        then (x -' 1) in ( dom G) by AFINSQ_1: 86;

        then

         A36: (((P . (x -' 1)) + 1) -' 1) = (P . (x -' 1)) & ((F * P) . (x -' 1)) = (F . (P . (x -' 1))) by A3, FUNCT_1: 12, NAT_D: 34;

        1 <= ((P . (x - 1)) + 1) by A32, A29, FINSEQ_1: 1;

        then ((F * P) . (x -' 1)) = (xF . ((P . (x - 1)) + 1)) by A35, A28, A36, AFINSQ_1:def 9;

        hence thesis by A31, A34, FUNCT_1: 13;

      end;

      ( len xG) = ( len F) by A22, AFINSQ_1:def 9;

      then xG = (xF * P9) by A24, A21, A20;

      then

       A37: (b "**" xG) = (b "**" xF) by A1, A4, FINSOP_1: 7;

      (b "**" xG) = (b "**" G) by A2, A22, Th43;

      hence thesis by A2, A37, Th43;

    end;

    theorem :: AFINSQ_2:46

    for bFG be XFinSequence of D st b is commutative associative & (b is having_a_unity or ( len F) >= 1) & ( len F) = ( len G) & ( len F) = ( len bFG) & (for n st n in ( dom bFG) holds (bFG . n) = (b . ((F . n),(G . n)))) holds (b "**" (F ^ G)) = (b "**" bFG)

    proof

      let bFG be XFinSequence of D such that

       A1: b is commutative associative and

       A2: b is having_a_unity or ( len F) >= 1 and

       A3: ( len F) = ( len G) and

       A4: ( len F) = ( len bFG) and

       A5: for n st n in ( dom bFG) holds (bFG . n) = (b . ((F . n),(G . n)));

      set xG = ( XFS2FS G);

      set xF = ( XFS2FS F);

      

       A6: (b "**" F) = (b "**" xF) & (b "**" G) = (b "**" xG) by A2, A3, Th43;

      set xb = ( XFS2FS bFG);

      

       A7: ( len xb) = ( len bFG) by AFINSQ_1:def 9;

      

       A8: for k be Nat st k in ( dom xb) holds (xb . k) = (b . ((xF . k),(xG . k)))

      proof

        let k be Nat such that

         A9: k in ( dom xb);

        k in ( Seg ( len xb)) by A9, FINSEQ_1:def 3;

        then k >= 1 by FINSEQ_1: 1;

        then

        reconsider k1 = (k - 1) as Element of NAT by NAT_1: 21;

        

         A10: k in ( Seg ( len xb)) by A9, FINSEQ_1:def 3;

        then

         A11: 1 <= k by FINSEQ_1: 1;

        then

         A12: k1 = (k -' 1) by XREAL_1: 233;

        k in ( Seg ( len xb)) by A9, FINSEQ_1:def 3;

        then k1 < (k1 + 1) & k <= ( len xb) by FINSEQ_1: 1, NAT_1: 13;

        then k1 < ( len xb) by XXREAL_0: 2;

        then k1 in ( dom bFG) by A7, AFINSQ_1: 86;

        then

         A13: (bFG . k1) = (b . ((F . k1),(G . k1))) by A5;

        

         A14: k <= ( len bFG) by A7, A10, FINSEQ_1: 1;

        then (bFG . (k -' 1)) = (xb . k) & (F . (k -' 1)) = (xF . k) by A4, A11, AFINSQ_1:def 9;

        hence thesis by A3, A4, A11, A14, A13, A12, AFINSQ_1:def 9;

      end;

      ( len xF) = ( len F) & ( len G) = ( len xG) by AFINSQ_1:def 9;

      then (b "**" xb) = (b . ((b "**" xF),(b "**" xG))) by A1, A2, A3, A4, A7, A8, FINSOP_1: 9;

      then (b "**" bFG) = (b . ((b "**" F),(b "**" G))) by A2, A4, A6, Th43;

      hence thesis by A1, A2, A3, Th41;

    end;

    theorem :: AFINSQ_2:47

    

     Th46: for D1,D2 be non empty set holds for b1 be BinOp of D1, b2 be BinOp of D2 st ( len F) >= 1 & D c= (D1 /\ D2) & for x, y st x in D & y in D holds (b1 . (x,y)) = (b2 . (x,y)) & (b1 . (x,y)) in D holds (b1 "**" F) = (b2 "**" F)

    proof

      let D1,D2 be non empty set;

      let b1 be BinOp of D1, b2 be BinOp of D2 such that

       A1: ( len F) >= 1 and

       A2: D c= (D1 /\ D2) and

       A3: for x, y st x in D & y in D holds (b1 . (x,y)) = (b2 . (x,y)) & (b1 . (x,y)) in D;

      (D1 /\ D2) c= D1 & (D1 /\ D2) c= D2 by XBOOLE_1: 17;

      then

       A4: D c= D1 & D c= D2 by A2;

      ( rng F) c= D1 & ( rng F) c= D2 by A4;

      then

       A5: F is D1 -valued & F is D2 -valued by RELAT_1:def 19;

      then

      consider F1 be sequence of D1 such that

       A6: (F1 . 0 ) = (F . 0 ) and

       A7: for n st (n + 1) < ( len F) holds (F1 . (n + 1)) = (b1 . ((F1 . n),(F . (n + 1)))) and

       A8: (b1 "**" F) = (F1 . (( len F) - 1)) by A1, Def8;

      consider F2 be sequence of D2 such that

       A9: (F2 . 0 ) = (F . 0 ) and

       A10: for n st (n + 1) < ( len F) holds (F2 . (n + 1)) = (b2 . ((F2 . n),(F . (n + 1)))) and

       A11: (b2 "**" F) = (F2 . (( len F) - 1)) by A1, Def8, A5;

      defpred P[ Nat] means $1 < ( len F) implies (F1 . $1) = (F2 . $1) & (F1 . $1) in D;

       0 in ( dom F) by A1, AFINSQ_1: 86;

      then (F . 0 ) in ( rng F) by FUNCT_1:def 3;

      then

       A12: P[ 0 ] by A6, A9;

      

       A13: P[n] implies P[(n + 1)]

      proof

        assume

         A14: P[n];

        assume

         A15: (n + 1) < ( len F);

        then (n + 1) in ( dom F) & n < ( len F) by NAT_1: 13, AFINSQ_1: 86;

        then

         A16: (F . (n + 1)) in ( rng F) & n in ( dom F) by FUNCT_1:def 3, AFINSQ_1: 86;

        

         A17: (F1 . (n + 1)) = (b1 . ((F1 . n),(F . (n + 1)))) by A7, A15;

        

        then (F1 . (n + 1)) = (b2 . ((F2 . n),(F . (n + 1)))) by A3, A16, A14, AFINSQ_1: 86

        .= (F2 . (n + 1)) by A10, A15;

        hence thesis by A16, A14, A17, A3, AFINSQ_1: 86;

      end;

      reconsider l1 = (( len F) - 1) as Element of NAT by A1, NAT_1: 21;

      

       A18: l1 < (l1 + 1) by NAT_1: 13;

       P[n] from NAT_1:sch 2( A12, A13);

      hence thesis by A8, A11, A18;

    end;

    reserve F for XFinSequence,

rF,rF1,rF2 for real-valued XFinSequence,

r for Real,

cF,cF1,cF2 for complex-valued XFinSequence,

c,c1,c2 for Complex;

    

     Lm2: cF is COMPLEX -valued

    proof

      ( rng cF) c= COMPLEX by VALUED_0:def 1;

      hence thesis by RELAT_1:def 19;

    end;

    

     Lm3: rF is REAL -valued

    proof

      ( rng rF) c= REAL by VALUED_0:def 3;

      hence thesis by RELAT_1:def 19;

    end;

    definition

      let F;

      :: AFINSQ_2:def9

      func Sum F -> Element of COMPLEX equals ( addcomplex "**" F);

      coherence ;

    end

    registration

      let f be empty complex-valued XFinSequence;

      cluster ( Sum f) -> zero;

      coherence

      proof

        f is COMPLEX -valued & ( len f) = 0 by Lm2;

        hence thesis by Def8, BINOP_2: 1;

      end;

    end

    theorem :: AFINSQ_2:48

    

     Th47: F is real-valued implies ( Sum F) = ( addreal "**" F)

    proof

      assume

       A1: F is real-valued;

      then ( rng F) c= REAL by VALUED_0:def 3;

      then

       A2: F is REAL -valued by RELAT_1:def 19;

      ( rng F) c= COMPLEX by A1, MEMBERED: 1;

      then

       A3: F is COMPLEX -valued by RELAT_1:def 19;

      per cases by NAT_1: 14;

        suppose

         A4: ( len F) = 0 ;

        

        hence ( addreal "**" F) = 0 by Def8, A2, BINOP_2: 2

        .= ( Sum F) by Def8, A3, A4, BINOP_2: 1;

      end;

        suppose

         A5: ( len F) >= 1;

        

         A6: REAL = ( REAL /\ COMPLEX ) by MEMBERED: 1, XBOOLE_1: 28;

        now

          let x, y;

          assume x in REAL & y in REAL ;

          then

          reconsider X = x, Y = y as Element of REAL ;

          ( addreal . (x,y)) = (X + Y) by BINOP_2:def 9;

          hence ( addreal . (x,y)) = ( addcomplex . (x,y)) & ( addreal . (x,y)) in REAL by BINOP_2:def 3, XREAL_0:def 1;

        end;

        hence thesis by Th46, A5, A6, A2;

      end;

    end;

    theorem :: AFINSQ_2:49

    

     Th48: F is RAT -valued implies ( Sum F) = ( addrat "**" F)

    proof

      assume

       A1: F is RAT -valued;

      ( rng F) c= COMPLEX by A1, MEMBERED: 1;

      then

       A2: F is COMPLEX -valued by RELAT_1:def 19;

      per cases by NAT_1: 14;

        suppose

         A3: ( len F) = 0 ;

        

        hence ( addrat "**" F) = 0 by Def8, A1, BINOP_2: 3

        .= ( Sum F) by Def8, A2, A3, BINOP_2: 1;

      end;

        suppose

         A4: ( len F) >= 1;

        

         A5: RAT = ( RAT /\ COMPLEX ) by MEMBERED: 1, XBOOLE_1: 28;

        now

          let x, y;

          assume x in RAT & y in RAT ;

          then

          reconsider X = x, Y = y as Element of RAT ;

          ( addrat . (x,y)) = (X + Y) by BINOP_2:def 15;

          hence ( addrat . (x,y)) = ( addcomplex . (x,y)) & ( addrat . (x,y)) in RAT by BINOP_2:def 3, RAT_1:def 2;

        end;

        hence thesis by Th46, A4, A5, A1;

      end;

    end;

    theorem :: AFINSQ_2:50

    

     Th49: F is INT -valued implies ( Sum F) = ( addint "**" F)

    proof

      assume

       A1: F is INT -valued;

      ( rng F) c= COMPLEX by A1, MEMBERED: 1;

      then

       A2: F is COMPLEX -valued by RELAT_1:def 19;

      per cases by NAT_1: 14;

        suppose

         A3: ( len F) = 0 ;

        

        hence ( addint "**" F) = 0 by Def8, A1, BINOP_2: 4

        .= ( Sum F) by Def8, A2, A3, BINOP_2: 1;

      end;

        suppose

         A4: ( len F) >= 1;

        

         A5: INT = ( INT /\ COMPLEX ) by MEMBERED: 1, XBOOLE_1: 28;

        now

          let x, y;

          assume x in INT & y in INT ;

          then

          reconsider X = x, Y = y as Element of INT ;

          ( addint . (x,y)) = (X + Y) by BINOP_2:def 20;

          hence ( addint . (x,y)) = ( addcomplex . (x,y)) & ( addint . (x,y)) in INT by BINOP_2:def 3, INT_1:def 2;

        end;

        hence thesis by Th46, A4, A5, A1;

      end;

    end;

    theorem :: AFINSQ_2:51

    

     Th50: F is natural-valued implies ( Sum F) = ( addnat "**" F)

    proof

      assume

       A1: F is natural-valued;

      then ( rng F) c= NAT by VALUED_0:def 6;

      then

       A2: F is NAT -valued by RELAT_1:def 19;

      ( rng F) c= COMPLEX by A1, MEMBERED: 1;

      then

       A3: F is COMPLEX -valued by RELAT_1:def 19;

      per cases by NAT_1: 14;

        suppose

         A4: ( len F) = 0 ;

        

        hence ( addnat "**" F) = 0 by Def8, A2, BINOP_2: 5

        .= ( Sum F) by Def8, A3, A4, BINOP_2: 1;

      end;

        suppose

         A5: ( len F) >= 1;

        

         A6: NAT = ( NAT /\ COMPLEX ) by MEMBERED: 1, XBOOLE_1: 28;

        now

          let x, y;

          assume x in NAT & y in NAT ;

          then

          reconsider X = x, Y = y as Element of NAT ;

          ( addnat . (x,y)) = (X + Y) by BINOP_2:def 23;

          hence ( addnat . (x,y)) = ( addcomplex . (x,y)) & ( addnat . (x,y)) in NAT by BINOP_2:def 3;

        end;

        hence thesis by Th46, A5, A6, A2;

      end;

    end;

    registration

      let F be real-valued XFinSequence;

      cluster ( Sum F) -> real;

      coherence

      proof

        ( Sum F) = ( addreal "**" F) by Th47;

        hence thesis;

      end;

    end

    registration

      let F be RAT -valued XFinSequence;

      cluster ( Sum F) -> rational;

      coherence

      proof

        ( Sum F) = ( addrat "**" F) by Th48;

        hence thesis;

      end;

    end

    registration

      let F be INT -valued XFinSequence;

      cluster ( Sum F) -> integer;

      coherence

      proof

        ( Sum F) = ( addint "**" F) by Th49;

        hence thesis;

      end;

    end

    registration

      let F be natural-valued XFinSequence;

      cluster ( Sum F) -> natural;

      coherence

      proof

        ( Sum F) = ( addnat "**" F) by Th50;

        hence thesis;

      end;

    end

    registration

      cluster natural-valued -> nonnegative-yielding for Relation;

      coherence

      proof

        let R be Relation;

        assume R is natural-valued;

        then for r be Real st r in ( rng R) holds r >= 0 ;

        hence thesis by PARTFUN3:def 4;

      end;

    end

    theorem :: AFINSQ_2:52

    cF = {} implies ( Sum cF) = 0 ;

    theorem :: AFINSQ_2:53

    ( Sum <%c%>) = c

    proof

      c in COMPLEX by XCMPLX_0:def 2;

      hence thesis by Th37;

    end;

    theorem :: AFINSQ_2:54

    ( Sum <%c1, c2%>) = (c1 + c2)

    proof

      c1 in COMPLEX & c2 in COMPLEX by XCMPLX_0:def 2;

      

      then ( addcomplex "**" <%c1, c2%>) = ( addcomplex . (c1,c2)) by Th38

      .= (c1 + c2) by BINOP_2:def 3;

      hence thesis;

    end;

    theorem :: AFINSQ_2:55

    

     Th54: ( Sum (cF1 ^ cF2)) = (( Sum cF1) + ( Sum cF2))

    proof

      

       A1: cF1 is COMPLEX -valued & cF2 is COMPLEX -valued by Lm2;

      

      thus ( Sum (cF1 ^ cF2)) = ( addcomplex . (( Sum cF1),( Sum cF2))) by Th41, A1

      .= (( Sum cF1) + ( Sum cF2)) by BINOP_2:def 3;

    end;

    theorem :: AFINSQ_2:56

    for S be Real_Sequence st rF = (S | (n + 1)) holds ( Sum rF) = (( Partial_Sums S) . n)

    proof

      let S be Real_Sequence;

      

       A1: rF is REAL -valued by Lm3;

      (n + 1) c= NAT ;

      then

       A2: (n + 1) c= ( dom S) by FUNCT_2:def 1;

      assume

       A3: rF = (S | (n + 1));

      then ( dom rF) = (( dom S) /\ (n + 1)) by RELAT_1: 61;

      then

       A4: ( dom rF) = (n + 1) by A2, XBOOLE_1: 28;

      then

      consider f be sequence of REAL such that

       A5: (f . 0 ) = (rF . 0 ) and

       A6: for m be Nat st (m + 1) < ( len rF) holds (f . (m + 1)) = ( addreal . ((f . m),(rF . (m + 1)))) and

       A7: ( addreal "**" rF) = (f . (( len rF) - 1)) by Def8, A1;

      defpred P[ Nat] means $1 in ( dom rF) implies (f . $1) = (( Partial_Sums S) . $1);

       A8:

      now

        let k;

        assume

         A9: P[k];

        thus P[(k + 1)]

        proof

          assume

           A10: (k + 1) in ( dom rF);

          then

           A11: (k + 1) < ( len rF) by AFINSQ_1: 86;

          then

           A12: k < ( len rF) by NAT_1: 13;

          

          thus (f . (k + 1)) = ( addreal . ((f . k),(rF . (k + 1)))) by A6, A11

          .= ((f . k) + (rF . (k + 1))) by BINOP_2:def 9

          .= ((f . k) + (S . (k + 1))) by A3, A10, FUNCT_1: 47

          .= (( Partial_Sums S) . (k + 1)) by A9, A12, AFINSQ_1: 86, SERIES_1:def 1;

        end;

      end;

      (( Partial_Sums S) . 0 ) = (S . 0 ) by SERIES_1:def 1;

      then

       A13: P[ 0 ] by A3, A5, FUNCT_1: 47;

      

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

      for m holds P[m] from NAT_1:sch 2( A13, A8);

      

      hence (( Partial_Sums S) . n) = (f . n) by A4, A14

      .= ( Sum rF) by Th47, A7, A4;

    end;

    theorem :: AFINSQ_2:57

    

     Th56: ( len rF1) = ( len rF2) & (for i st i in ( dom rF1) holds (rF1 . i) <= (rF2 . i)) implies ( Sum rF1) <= ( Sum rF2)

    proof

      set d = rF1, e = rF2;

      assume that

       A1: ( len d) = ( len e) and

       A2: for i st i in ( dom d) holds (d . i) <= (e . i);

      reconsider d, e as XFinSequence of REAL by Lm3;

      

       A3: ( Sum d) = ( addreal "**" d) & ( Sum e) = ( addreal "**" e) by Th47;

      per cases by NAT_1: 14;

        suppose

         A4: ( len d) >= 1;

        consider f be sequence of REAL such that

         A5: (f . 0 ) = (d . 0 ) and

         A6: for n st (n + 1) < ( len d) holds (f . (n + 1)) = ( addreal . ((f . n),(d . (n + 1)))) and

         A7: ( Sum d) = (f . (( len d) - 1)) by A4, Def8, A3;

        consider g be sequence of REAL such that

         A8: (g . 0 ) = (e . 0 ) and

         A9: for n st (n + 1) < ( len e) holds (g . (n + 1)) = ( addreal . ((g . n),(e . (n + 1)))) and

         A10: ( Sum e) = (g . (( len e) - 1)) by A4, A1, Def8, A3;

        defpred P[ Nat] means $1 in ( dom d) implies (f . $1) <= (g . $1);

         A11:

        now

          let i;

          assume

           A12: P[i];

          thus P[(i + 1)]

          proof

            assume

             A13: (i + 1) in ( dom d);

            then

             A14: (i + 1) < ( len d) by AFINSQ_1: 86;

            then

             A15: i < ( len d) by NAT_1: 13;

            

             A16: (d . (i + 1)) <= (e . (i + 1)) by A2, A13;

            

             A17: (f . (i + 1)) = ( addreal . ((f . i),(d . (i + 1)))) by A6, A14

            .= ((f . i) + (d . (i + 1))) by BINOP_2:def 9;

            (g . (i + 1)) = ( addreal . ((g . i),(e . (i + 1)))) by A1, A9, A14

            .= ((g . i) + (e . (i + 1))) by BINOP_2:def 9;

            hence thesis by A12, A15, A17, A16, AFINSQ_1: 86, XREAL_1: 7;

          end;

        end;

        reconsider ld = (( len d) - 1) as Element of NAT by A4, NAT_1: 21;

        (( len d) - 1) < (( len d) - 0 ) by XREAL_1: 10;

        then

         A18: ld in ( len d) by AFINSQ_1: 86;

        

         A19: P[ 0 ] by A2, A5, A8;

        for i holds P[i] from NAT_1:sch 2( A19, A11);

        hence thesis by A1, A7, A10, A18;

      end;

        suppose ( len d) = 0 ;

        then ( Sum d) = ( the_unity_wrt addreal ) & ( Sum e) = ( the_unity_wrt addreal ) by Def8, A3, A1;

        hence thesis;

      end;

    end;

    theorem :: AFINSQ_2:58

    

     Th57: ( Sum (n --> c)) = (n * c)

    proof

      set Fn = (n --> c);

      reconsider Fn as XFinSequence of COMPLEX by Lm2;

      

       A1: ( dom Fn) = n by FUNCOP_1: 13;

      now

        per cases ;

          suppose ( dom Fn) = 0 ;

          hence thesis by A1;

        end;

          suppose

           A2: ( dom Fn) > 0 ;

          then

          consider f be sequence of COMPLEX such that

           A3: (f . 0 ) = (Fn . 0 ) and

           A4: for k st (k + 1) < ( len Fn) holds (f . (k + 1)) = ( addcomplex . ((f . k),(Fn . (k + 1)))) and

           A5: ( Sum Fn) = (f . (( len Fn) - 1)) by Def8;

          defpred P[ Nat] means $1 < ( len Fn) implies (f . $1) = (($1 + 1) * c);

          

           A6: for m st P[m] holds P[(m + 1)]

          proof

            let m such that

             A7: P[m];

            assume

             A8: (m + 1) < ( len Fn);

            then (f . (m + 1)) = ( addcomplex . ((f . m),(Fn . (m + 1)))) by A4;

            then

             A9: (f . (m + 1)) = ((f . m) + (Fn . (m + 1))) by BINOP_2:def 3;

            (Fn . (m + 1)) = c by A1, FUNCOP_1: 7, A8, AFINSQ_1: 86;

            hence thesis by A7, A8, A9, NAT_1: 13;

          end;

          reconsider lenFn1 = (( len Fn) - 1) as Element of NAT by A2, NAT_1: 20;

          

           A10: lenFn1 < (lenFn1 + 1) by NAT_1: 13;

          

           A11: P[ 0 ] by A3, A1, FUNCOP_1: 7, AFINSQ_1: 86;

          for m holds P[m] from NAT_1:sch 2( A11, A6);

          hence thesis by A5, A10, A1;

        end;

      end;

      hence thesis;

    end;

    theorem :: AFINSQ_2:59

    (for n st n in ( dom rF) holds (rF . n) <= r) implies ( Sum rF) <= (( len rF) * r)

    proof

      set L = (( len rF) --> r);

      assume

       A1: n in ( dom rF) implies (rF . n) <= r;

      

       A2: ( len L) = ( len rF) by FUNCOP_1: 13;

      now

        let n;

        assume n in ( dom rF);

        then (rF . n) <= r & (L . n) = r by A1, FUNCOP_1: 7;

        hence (rF . n) <= (L . n);

      end;

      then ( Sum rF) <= ( Sum L) by Th56, A2;

      hence thesis by Th57;

    end;

    theorem :: AFINSQ_2:60

    (for n st n in ( dom rF) holds (rF . n) >= r) implies ( Sum rF) >= (( len rF) * r)

    proof

      set L = (( len rF) --> r);

      assume

       A1: n in ( dom rF) implies (rF . n) >= r;

      

       A2: ( len L) = ( len rF) by FUNCOP_1: 13;

      now

        let n;

        assume n in ( dom rF);

        then (rF . n) >= r & (L . n) = r by A1, FUNCOP_1: 7;

        hence (rF . n) >= (L . n);

      end;

      then ( Sum rF) >= ( Sum L) by Th56, A2;

      hence thesis by Th57;

    end;

    theorem :: AFINSQ_2:61

    

     Th60: rF is nonnegative-yielding & ( len rF) > 0 & (ex x st x in ( dom rF) & (rF . x) = r) implies ( Sum rF) >= r

    proof

      assume that

       A1: rF is nonnegative-yielding and

       A2: ( len rF) > 0 and

       A3: ex x st x in ( dom rF) & (rF . x) = r;

      consider x such that

       A4: x in ( dom rF) and

       A5: (rF . x) = r by A3;

      reconsider lenrF1 = (( len rF) - 1) as Element of NAT by A2, NAT_1: 20;

      

       A6: ( dom rF) = (lenrF1 + 1);

      reconsider x as Element of NAT by A4;

      

       A7: lenrF1 < (lenrF1 + 1) by NAT_1: 13;

      

       A8: x < ( len rF) by A4, AFINSQ_1: 86;

      then

       A9: x <= lenrF1 by A6, NAT_1: 13;

      rF is REAL -valued by Lm3;

      then

      consider f be sequence of REAL such that

       A10: (f . 0 ) = (rF . 0 ) and

       A11: for n st (n + 1) < ( len rF) holds (f . (n + 1)) = ( addreal . ((f . n),(rF . (n + 1)))) and

       A12: ( addreal "**" rF) = (f . (( len rF) - 1)) by Def8, A2;

      defpred P[ Nat] means $1 < x implies (f . $1) >= 0 ;

       0 in ( len rF) by A2, AFINSQ_1: 86;

      then (rF . 0 ) in ( rng rF) by FUNCT_1:def 3;

      then

       A13: P[ 0 ] by A1, A10, PARTFUN3:def 4;

      

       A14: P[n] implies P[(n + 1)]

      proof

        assume

         A15: P[n];

        assume

         A16: (n + 1) < x;

        then n < x & (n + 1) < ( len rF) by A8, NAT_1: 13, XXREAL_0: 2;

        then

         A17: (f . (n + 1)) = ( addreal . ((f . n),(rF . (n + 1)))) & (f . n) >= 0 & (n + 1) in ( dom rF) by A11, A15, AFINSQ_1: 86;

        then (rF . (n + 1)) in ( rng rF) by FUNCT_1:def 3;

        then (rF . (n + 1)) >= 0 by A1, PARTFUN3:def 4;

        then ((f . n) + (rF . (n + 1))) >= (zz + zz) by A16, A15, NAT_1: 13;

        hence thesis by A17, BINOP_2:def 9;

      end;

      

       A18: P[n] from NAT_1:sch 2( A13, A14);

      defpred P[ Nat] means x <= $1 & $1 < ( len rF) implies (f . $1) >= r;

      now

        per cases ;

          suppose

           A19: x = 0 ;

          assume that x <= x and x < ( len rF);

          thus (f . x) >= r by A5, A10, A19;

        end;

          suppose x > 0 ;

          then

          reconsider x1 = (x - 1) as Element of NAT by NAT_1: 20;

          assume that x <= x and

           A20: x < ( len rF);

          

           A21: x1 < (x1 + 1) by NAT_1: 13;

          (x1 + 1) < ( len rF) by A20;

          then (f . x) = ( addreal . ((f . x1),(rF . x))) by A11;

          then (f . x) = ((f . x1) + (rF . x)) & (f . x1) >= 0 by A21, A18, BINOP_2:def 9;

          then (f . x) >= (r + 0 qua Real) by A5, XREAL_1: 7;

          hence (f . x) >= r;

        end;

      end;

      then

       A22: P[x];

      

       A23: for m be Nat st m >= x & P[m] holds P[(m + 1)]

      proof

        let m be Nat such that

         A24: m >= x and

         A25: P[m];

        reconsider m1 = m as Element of NAT by ORDINAL1:def 12;

        assume that x <= (m + 1) and

         A26: (m + 1) < ( len rF);

        (m + 1) in ( dom rF) by A26, AFINSQ_1: 86;

        then

         A27: (rF . (m + 1)) in ( rng rF) by FUNCT_1:def 3;

        (f . (m1 + 1)) = ( addreal . ((f . m1),(rF . (m1 + 1)))) by A11, A26;

        then (f . (m1 + 1)) = ((f . m1) + (rF . (m1 + 1))) & (rF . (m1 + 1)) >= 0 by A27, A1, BINOP_2:def 9, PARTFUN3:def 4;

        then (f . (m + 1)) >= (r + 0 qua Real) by A24, A25, A26, NAT_1: 13, XREAL_1: 7;

        hence thesis;

      end;

      for m be Nat st m >= x holds P[m] from NAT_1:sch 8( A22, A23);

      then ( addreal "**" rF) >= r by A12, A9, A7;

      hence thesis by Th47;

    end;

    theorem :: AFINSQ_2:62

    

     Th61: rF is nonnegative-yielding implies (( Sum rF) = 0 iff (( len rF) = 0 or rF = (( len rF) --> 0 )))

    proof

      assume

       A1: rF is nonnegative-yielding;

      hereby

        assume

         A2: ( Sum rF) = 0 ;

        assume

         A3: ( len rF) <> 0 ;

        set L = (( len rF) --> 0 );

        assume rF <> (( len rF) --> 0 );

        then

        consider k such that

         A4: k in ( dom L) & (L . k) <> (rF . k) by AFINSQ_1: 8, FUNCOP_1: 13;

        (rF . k) in ( rng rF) by A4, FUNCT_1:def 3;

        then (L . k) = 0 & (rF . k) >= 0 by A4, A1, FUNCOP_1: 7, PARTFUN3:def 4;

        hence contradiction by A2, Th60, A1, A4, A3;

      end;

      

       A5: rF is COMPLEX -valued by Lm2;

      assume ( len rF) = 0 or rF = (( len rF) --> 0 );

      then ( Sum rF) = 0 or ( Sum rF) = (( len rF) * 0 ) by A5, Th57, Def8, BINOP_2: 1;

      hence thesis;

    end;

    theorem :: AFINSQ_2:63

    

     Th62: (c (#) (cF | n)) = ((c (#) cF) | n)

    proof

      set ccF = (c (#) cF);

      set cFn = (cF | n);

      

       A1: ( len ccF) = ( len cF) & ( len (c (#) cFn)) = ( len cFn) by VALUED_1:def 5;

      per cases ;

        suppose

         A2: n <= ( len cF);

        then

         A3: ( len cFn) = n & ( len (ccF | n)) = n by A1, AFINSQ_1: 54;

        now

          let i;

          assume i < ( len (c (#) cFn));

          then

           A4: i in ( dom (c (#) cFn)) by AFINSQ_1: 86;

          

          thus ((c (#) cFn) . i) = (c * (cFn . i)) by VALUED_1: 6

          .= (c * (cF . i)) by A4, A2, AFINSQ_1: 53

          .= (ccF . i) by VALUED_1: 6

          .= ((ccF | n) . i) by A4, A1, A2, AFINSQ_1: 53;

        end;

        hence thesis by A1, A3, AFINSQ_1: 9;

      end;

        suppose n > ( len cF);

        then (cF | n) = cF & (ccF | n) = ccF by A1, AFINSQ_1: 52;

        hence thesis;

      end;

    end;

    theorem :: AFINSQ_2:64

    (c * ( Sum cF)) = ( Sum (c (#) cF))

    proof

      defpred P[ Nat] means for cF st ( len cF) = $1 holds (c * ( Sum cF)) = ( Sum (c (#) cF));

      

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

      proof

        let k such that

         A2: P[k];

        

         A3: k < (k + 1) by NAT_1: 13;

        let cF such that

         A4: ( len cF) = (k + 1);

        set cF1 = (c (#) cF);

        

         A5: ( dom cF) = ( dom cF1) by VALUED_1:def 5;

        reconsider cF, cF1 as XFinSequence of COMPLEX by Lm2;

        

         A6: (cF | (k + 1)) = cF by A4;

        

         A7: ( len (cF | k)) = k by A3, AFINSQ_1: 11, A4;

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

        then

         A8: k in ( dom cF) by A4, AFINSQ_1: 86;

        then ( addcomplex . (( addcomplex "**" (cF | k)),(cF . k))) = ( addcomplex "**" (cF | (k + 1))) by Th42;

        then

         A9: ( Sum cF) = (( Sum (cF | k)) + (cF . k)) by A6, BINOP_2:def 3;

        

         A10: (c * ( Sum (cF | k))) = ( Sum (c (#) (cF | k))) by A2, A7

        .= ( Sum (cF1 | k)) by Th62;

        

         A11: (c * (cF . k)) = (cF1 . k) by VALUED_1: 6;

        

         A12: (cF1 | (k + 1)) = cF1 by A4, A5;

        ( addcomplex . (( addcomplex "**" (cF1 | k)),(cF1 . k))) = ( addcomplex "**" (cF1 | (k + 1))) by A5, A8, Th42;

        then ( Sum cF1) = (( Sum (cF1 | k)) + (cF1 . k)) by A12, BINOP_2:def 3;

        hence thesis by A9, A11, A10;

      end;

      

       A13: P[ 0 ]

      proof

        let cF such that

         A14: ( len cF) = 0 ;

        set cF1 = (c (#) cF);

        reconsider cF, cF1 as XFinSequence of COMPLEX by Lm2;

        

         A15: ( addcomplex "**" cF) = 0 by Def8, BINOP_2: 1, A14;

        ( len cF1) = 0 by A14, VALUED_1:def 5;

        hence thesis by A15, Def8, BINOP_2: 1;

      end;

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

      then P[( len cF)];

      hence thesis;

    end;

    theorem :: AFINSQ_2:65

    

     Th64: n in ( dom cF) implies (( Sum (cF | n)) + (cF . n)) = ( Sum (cF | (n + 1)))

    proof

      assume

       A1: n in ( dom cF);

      reconsider cF as XFinSequence of COMPLEX by Lm2;

      ( addcomplex . (( addcomplex "**" (cF | n)),(cF . n))) = ( addcomplex "**" (cF | (n + 1))) by Th42, A1;

      hence thesis by BINOP_2:def 3;

    end;

    theorem :: AFINSQ_2:66

    

     Th65: for f be Function st (f . y) = x & y in ( dom f) holds ( {y} \/ ((f | (( dom f) \ {y})) " {x})) = (f " {x})

    proof

      let f be Function;

      assume that

       A1: (f . y) = x and

       A2: y in ( dom f);

      set d = (( dom f) \ {y});

      

       A3: ((f | d) " {x}) c= (f " {x})

      proof

        let x1 be object such that

         A4: x1 in ((f | d) " {x});

        

         A5: ((f | d) . x1) in {x} by A4, FUNCT_1:def 7;

        

         A6: x1 in ( dom (f | d)) by A4, FUNCT_1:def 7;

        then ( dom (f | d)) = (( dom f) /\ d) & (f . x1) = ((f | d) . x1) by FUNCT_1: 47, RELAT_1: 61;

        hence thesis by A6, A5, FUNCT_1:def 7;

      end;

      

       A7: (f " {x}) c= ( {y} \/ ((f | d) " {x}))

      proof

        let x1 be object such that

         A8: x1 in (f " {x});

        x1 in ( dom f) & not x1 in {y} or x1 = y by A8, FUNCT_1:def 7, TARSKI:def 1;

        then x1 in ( dom f) & x1 in d & ( dom (f | d)) = (( dom f) /\ d) or x1 = y by RELAT_1: 61, XBOOLE_0:def 5;

        then x1 in ( dom (f | d)) or x1 = y by XBOOLE_0:def 4;

        then x1 in ( dom (f | d)) & (f . x1) = ((f | d) . x1) & (f . x1) in {x} or x1 in {y} by A8, FUNCT_1: 47, FUNCT_1:def 7, TARSKI:def 1;

        then x1 in ((f | d) " {x}) or x1 in {y} by FUNCT_1:def 7;

        hence thesis by XBOOLE_0:def 3;

      end;

       {y} c= (f " {x})

      proof

        let z be object;

        assume z in {y};

        then

         A9: z = y by TARSKI:def 1;

        (f . y) in {x} by A1, TARSKI:def 1;

        hence thesis by A2, A9, FUNCT_1:def 7;

      end;

      hence thesis by A7, A3, XBOOLE_1: 8;

    end;

    theorem :: AFINSQ_2:67

    

     Th66: for x,y be object holds for f be Function st (f . y) <> x holds ((f | (( dom f) \ {y})) " {x}) = (f " {x})

    proof

      let x,y be object;

      let f be Function;

      set d = (( dom f) \ {y});

      assume

       A1: (f . y) <> x;

      

       A2: (f " {x}) c= ((f | d) " {x})

      proof

        

         A3: ( dom (f | d)) = (( dom f) /\ d) by RELAT_1: 61;

        let x1 be object such that

         A4: x1 in (f " {x});

        

         A5: (f . x1) in {x} by A4, FUNCT_1:def 7;

        (f . x1) in {x} by A4, FUNCT_1:def 7;

        then (f . x1) = x by TARSKI:def 1;

        then

         A6: not x1 in {y} by A1, TARSKI:def 1;

        x1 in ( dom f) by A4, FUNCT_1:def 7;

        then x1 in d by A6, XBOOLE_0:def 5;

        then

         A7: x1 in ( dom (f | d)) by A3, XBOOLE_0:def 4;

        then (f . x1) = ((f | d) . x1) by FUNCT_1: 47;

        hence thesis by A7, A5, FUNCT_1:def 7;

      end;

      ((f | d) " {x}) c= (f " {x})

      proof

        let x1 be object such that

         A8: x1 in ((f | d) " {x});

        

         A9: ((f | d) . x1) in {x} by A8, FUNCT_1:def 7;

        

         A10: x1 in ( dom (f | d)) by A8, FUNCT_1:def 7;

        then ( dom (f | d)) = (( dom f) /\ d) & (f . x1) = ((f | d) . x1) by FUNCT_1: 47, RELAT_1: 61;

        hence thesis by A10, A9, FUNCT_1:def 7;

      end;

      hence thesis by A2;

    end;

    theorem :: AFINSQ_2:68

    ( rng cF) c= { 0 , c} implies ( Sum cF) = (c * ( card (cF " {c})))

    proof

      defpred P[ Nat] means for cF, c st ( len cF) = $1 & ( rng cF) c= { 0 , c} holds ( Sum cF) = (c * ( card (cF " {c})));

      assume

       A1: ( rng cF) c= { 0 , c};

      

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

      proof

        let k such that

         A3: P[k];

        let F be complex-valued XFinSequence, c be Complex such that

         A4: ( len F) = (k + 1) and

         A5: ( rng F) c= { 0 , c};

        per cases ;

          suppose

           A6: c <> 0 ;

          ( not k in k) & (( Segm k) \/ {k}) = ( Segm (k + 1)) by AFINSQ_1: 2;

          then

           A7: (( dom F) \ {k}) = k by A4, ZFMISC_1: 117;

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

          then k in ( dom F) by A4, AFINSQ_1: 86;

          then

           A8: (F . k) in ( rng F) by FUNCT_1:def 3;

          per cases by A5, A8, TARSKI:def 2;

            suppose

             A9: (F . k) = 0 ;

            

             A10: (F | (k + 1)) = F by A4;

            

             A11: k < (k + 1) by NAT_1: 13;

            then

             A12: (( Sum (F | k)) + 0 qua Real) = ( Sum F) by A9, A10, Th64, A4, AFINSQ_1: 86;

            

             A13: ( len (F | k)) = k by A4, A11, AFINSQ_1: 54;

            ( rng (F | k)) c= ( rng F) & ((F | k) " {c}) = (F " {c}) by A6, A7, A9, Th66;

            hence thesis by A3, A5, A13, A12, XBOOLE_1: 1;

          end;

            suppose

             A14: (F . k) = c;

            set Fk = ((F | k) " {c});

             not k in k;

            then not k in ( dom (F | k));

            then

             A15: not k in Fk by FUNCT_1:def 7;

            

             A16: k < (k + 1) by NAT_1: 13;

            then

             A17: k in ( dom F) by A4, AFINSQ_1: 86;

            ( rng (F | k)) c= ( rng F) & ( len (F | k)) = k by A4, A16, AFINSQ_1: 54;

            then

             A18: ( Sum (F | k)) = (c * ( card ((F | k) " {c}))) by A3, A5, XBOOLE_1: 1;

            (F | (k + 1)) = F by A4;

            then

             A19: (( Sum (F | k)) + c) = ( Sum F) by A14, A17, Th64;

            ( {k} \/ Fk) = (F " {c}) by A7, A14, A17, Th65;

            then (( card Fk) + 1) = ( card (F " {c})) by A15, CARD_2: 41;

            hence thesis by A18, A19;

          end;

        end;

          suppose

           A20: c = 0 ;

          for x be object st x in ( dom F) holds (F . x) = 0

          proof

            let x be object;

            assume x in ( dom F);

            then (F . x) in ( rng F) by FUNCT_1:def 3;

            hence thesis by A5, A20, TARSKI:def 2;

          end;

          then F = (( dom F) --> 0 ) by FUNCOP_1: 11;

          then ( Sum F) = (( len F) * 0 ) by Th61;

          hence thesis by A20;

        end;

      end;

      

       A21: P[ 0 ]

      proof

        let F be complex-valued XFinSequence, c be Complex such that

         A22: ( len F) = 0 and ( rng F) c= { 0 , c};

        (F " {c}) c= 0 & F = {} by A22, RELAT_1: 132;

        then ( card (F " {c})) = 0 & ( Sum F) = 0 ;

        hence thesis;

      end;

      for k holds P[k] from NAT_1:sch 2( A21, A2);

      then P[( len cF)];

      hence thesis by A1;

    end;

    theorem :: AFINSQ_2:69

    ( Sum cF) = ( Sum ( Rev cF))

    proof

      cF is COMPLEX -valued by Lm2;

      then

      reconsider Fr2 = cF, Fr1 = ( Rev cF) as XFinSequence of COMPLEX ;

      

       A1: ( len Fr1) = ( len Fr2) by Def1;

      defpred P[ object, object] means for i st i = $1 holds $2 = (( len Fr1) - (1 + i));

      

       A2: ( card ( len Fr1)) = ( card ( len Fr1));

      

       A3: for x be object st x in ( len Fr1) holds ex y be object st y in ( len Fr1) & P[x, y]

      proof

        let x be object such that

         A4: x in ( len Fr1);

        reconsider k = x as Element of NAT by Th1, A4;

        (k + 1) <= ( len Fr1) by NAT_1: 13, A4, AFINSQ_1: 86;

        then

         A5: (( len Fr1) -' (1 + k)) = (( len Fr1) - (1 + k)) by XREAL_1: 233;

        take (( len Fr1) -' (1 + k));

        (( len Fr1) + zz) < (( len Fr1) + (1 + k)) by XREAL_1: 8;

        then (( len Fr1) - (1 + k)) < ((( len Fr1) + (1 + k)) - (1 + k)) by XREAL_1: 9;

        hence thesis by A5, AFINSQ_1: 86;

      end;

      consider P be Function of ( len Fr1), ( len Fr1) such that

       A6: for x be object st x in ( len Fr1) holds P[x, (P . x)] from FUNCT_2:sch 1( A3);

      for x1,x2 be object st x1 in ( len Fr1) & x2 in ( len Fr1) & (P . x1) = (P . x2) holds x1 = x2

      proof

        let x1,x2 be object such that

         A7: x1 in ( len Fr1) and

         A8: x2 in ( len Fr1) and

         A9: (P . x1) = (P . x2);

        reconsider i = x1, j = x2 as Element of NAT by A7, A8, Th1;

        

         A10: (P . x2) = (( len Fr1) - (1 + j)) by A6, A8;

        (P . x1) = (( len Fr1) - (1 + i)) by A6, A7;

        hence thesis by A9, A10;

      end;

      then

       A11: P is one-to-one by FUNCT_2: 56;

      then P is onto by A2, Lm1;

      then

      reconsider P as Permutation of ( dom Fr1) by A11;

       A12:

      now

        let x be object such that

         A13: x in ( dom Fr1);

        reconsider k = x as Element of NAT by A13;

        (P . k) = (( len Fr1) - (1 + k)) by A6, A13;

        hence (Fr1 . x) = (Fr2 . (P . x)) by A1, Def1, A13;

      end;

       A14:

      now

        let x be object such that

         A15: x in ( dom Fr1);

        x in ( dom P) by A15, FUNCT_2: 52;

        then (P . x) in ( rng P) by FUNCT_1: 3;

        hence x in ( dom P) & (P . x) in ( dom Fr2) by A1, A15, FUNCT_2: 52;

      end;

      for x be object st x in ( dom P) & (P . x) in ( dom Fr2) holds x in ( dom Fr1);

      then Fr1 = (Fr2 * P) by A14, A12, FUNCT_1: 10;

      hence thesis by A1, Th44;

    end;

    theorem :: AFINSQ_2:70

    

     Th69: for f be Function, p,q,fp,fq be XFinSequence st ( rng p) c= ( dom f) & ( rng q) c= ( dom f) & fp = (f * p) & fq = (f * q) holds (fp ^ fq) = (f * (p ^ q))

    proof

      let f be Function, p,q,fp,fq be XFinSequence such that

       A1: ( rng p) c= ( dom f) & ( rng q) c= ( dom f) & fp = (f * p) & fq = (f * q);

      set pq = (p ^ q);

      

       A2: ( rng pq) = (( rng p) \/ ( rng q)) by AFINSQ_1: 26;

      then

       A3: ( dom (f * pq)) = ( dom pq) by A1, RELAT_1: 27, XBOOLE_1: 8;

      reconsider fpq = (f * pq) as XFinSequence by A2, A1, AFINSQ_1: 10, XBOOLE_1: 8;

      

       A4: ( dom fp) = ( dom p) & ( dom fq) = ( dom q) by A1, RELAT_1: 27;

      

       A5: ( dom pq) = (( len p) + ( len q)) & ( dom (fp ^ fq)) = (( len fp) + ( len fq)) by AFINSQ_1:def 3;

      

       A6: ( len fpq) = ( len (fp ^ fq)) by A2, A1, A4, A5, RELAT_1: 27, XBOOLE_1: 8;

      k < ( len fpq) implies ((fp ^ fq) . k) = (fpq . k)

      proof

        assume

         A7: k < ( len fpq);

        then

         A8: k in ( dom fpq) by AFINSQ_1: 86;

        per cases ;

          suppose k < ( len p);

          then k in ( dom p) by AFINSQ_1: 86;

          then (pq . k) = (p . k) & (fp . k) = (f . (p . k)) & ((fp ^ fq) . k) = (fp . k) by A1, A4, AFINSQ_1:def 3, FUNCT_1: 13;

          hence thesis by A8, FUNCT_1: 12;

        end;

          suppose

           A9: k >= ( len p);

          then

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

          (( len p) + kp) < (( len p) + ( len q)) by A5, A2, A1, A7, RELAT_1: 27, XBOOLE_1: 8;

          then kp < ( len q) by XREAL_1: 7;

          then (pq . k) = (q . kp) & ((fp ^ fq) . k) = (fq . kp) & (fq . kp) = (f . (q . kp)) by A7, A1, A3, A4, A5, A9, AFINSQ_1: 18, FUNCT_1: 13, AFINSQ_1: 86;

          hence thesis by A8, FUNCT_1: 12;

        end;

      end;

      hence thesis by A6, AFINSQ_1: 9;

    end;

    theorem :: AFINSQ_2:71

    for B1,B2 be finite natural-membered set st B1 <N< B2 holds ( Sum ( SubXFinS (cF,(B1 \/ B2)))) = (( Sum ( SubXFinS (cF,B1))) + ( Sum ( SubXFinS (cF,B2))))

    proof

      let B1,B2 be finite natural-membered set such that

       A1: B1 <N< B2;

      set B12 = (B1 \/ B2);

      set B12L = (B12 /\ ( len cF));

      set B1L = (B1 /\ ( len cF));

      set B2L = (B2 /\ ( len cF));

      (B1L \/ B2L) = B12L by XBOOLE_1: 23;

      then

       A3: ( Sgm0 B12L) = (( Sgm0 B1L) ^ ( Sgm0 B2L)) by Th35, A1, Th25;

      ( rng ( Sgm0 B1L)) = B1L & ( rng ( Sgm0 B2L)) = B2L by Def4;

      then ( rng ( Sgm0 B1L)) c= ( dom cF) & ( rng ( Sgm0 B2L)) c= ( dom cF) by XBOOLE_1: 17;

      then (( SubXFinS (cF,B1)) ^ ( SubXFinS (cF,B2))) = ( SubXFinS (cF,B12)) by A3, Th69;

      hence thesis by Th54;

    end;

    theorem :: AFINSQ_2:72

    

     Th71: b is having_a_unity implies (b "**" ( <%> D)) = ( the_unity_wrt b)

    proof

      

       A1: ( len ( <%> D)) = 0 ;

      assume b is having_a_unity;

      hence thesis by A1, Def8;

    end;

    definition

      let D be set, F be XFinSequence of (D ^omega );

      :: AFINSQ_2:def10

      func FlattenSeq F -> Element of (D ^omega ) means

      : Def10: ex g be BinOp of (D ^omega ) st (for p,q be Element of (D ^omega ) holds (g . (p,q)) = (p ^ q)) & it = (g "**" F);

      existence

      proof

        deffunc F( Element of (D ^omega ), Element of (D ^omega )) = ($1 ^ $2);

        consider g be BinOp of (D ^omega ) such that

         A1: for a,b be Element of (D ^omega ) holds (g . (a,b)) = F(a,b) from BINOP_1:sch 4;

        take (g "**" F), g;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let it1,it2 be Element of (D ^omega );

        given g1 be BinOp of (D ^omega ) such that

         A2: for p,q be Element of (D ^omega ) holds (g1 . (p,q)) = (p ^ q) and

         A3: it1 = (g1 "**" F);

        given g2 be BinOp of (D ^omega ) such that

         A4: for p,q be Element of (D ^omega ) holds (g2 . (p,q)) = (p ^ q) and

         A5: it2 = (g2 "**" F);

        now

          let a,b be Element of (D ^omega );

          

          thus (g1 . (a,b)) = (a ^ b) by A2

          .= (g2 . (a,b)) by A4;

        end;

        hence thesis by A3, A5, BINOP_1: 2;

      end;

    end

    theorem :: AFINSQ_2:73

    for D be set, d be Element of (D ^omega ) holds ( FlattenSeq <%d%>) = d

    proof

      let D be set, d be Element of (D ^omega );

      ex g be BinOp of (D ^omega ) st (for p,q be Element of (D ^omega ) holds (g . (p,q)) = (p ^ q)) & ( FlattenSeq <%d%>) = (g "**" <%d%>) by Def10;

      hence thesis by Th37;

    end;

    theorem :: AFINSQ_2:74

    for D be set holds ( FlattenSeq ( <%> (D ^omega ))) = ( <%> D)

    proof

      let D be set;

      consider g be BinOp of (D ^omega ) such that

       A1: for d1,d2 be Element of (D ^omega ) holds (g . (d1,d2)) = (d1 ^ d2) and

       A2: ( FlattenSeq ( <%> (D ^omega ))) = (g "**" ( <%> (D ^omega ))) by Def10;

      

       A3: {} is Element of (D ^omega ) by AFINSQ_1: 43;

      reconsider p = {} as Element of (D ^omega ) by AFINSQ_1: 43;

      now

        let a be Element of (D ^omega );

        

        thus (g . ( {} ,a)) = ( {} ^ a) by A1, A3

        .= a;

        

        thus (g . (a, {} )) = (a ^ {} ) by A1, A3

        .= a;

      end;

      then

       A4: p is_a_unity_wrt g by BINOP_1: 3;

      then (g "**" ( <%> (D ^omega ))) = ( the_unity_wrt g) by Th71, SETWISEO:def 2;

      hence thesis by A2, A4, BINOP_1:def 8;

    end;

    theorem :: AFINSQ_2:75

    

     Th74: for D be set, F,G be XFinSequence of (D ^omega ) holds ( FlattenSeq (F ^ G)) = (( FlattenSeq F) ^ ( FlattenSeq G))

    proof

      let D be set, F,G be XFinSequence of (D ^omega );

      consider g be BinOp of (D ^omega ) such that

       A1: for d1,d2 be Element of (D ^omega ) holds (g . (d1,d2)) = (d1 ^ d2) and

       A2: ( FlattenSeq (F ^ G)) = (g "**" (F ^ G)) by Def10;

      now

        let a,b,c be Element of (D ^omega );

        

        thus (g . (a,(g . (b,c)))) = (a ^ (g . (b,c))) by A1

        .= (a ^ (b ^ c)) by A1

        .= ((a ^ b) ^ c) by AFINSQ_1: 27

        .= ((g . (a,b)) ^ c) by A1

        .= (g . ((g . (a,b)),c)) by A1;

      end;

      then

       A3: g is associative;

      

       A4: {} is Element of (D ^omega ) by AFINSQ_1: 43;

      reconsider p = {} as Element of (D ^omega ) by AFINSQ_1: 43;

      now

        let a be Element of (D ^omega );

        

        thus (g . ( {} ,a)) = ( {} ^ a) by A1, A4

        .= a;

        

        thus (g . (a, {} )) = (a ^ {} ) by A1, A4

        .= a;

      end;

      then p is_a_unity_wrt g by BINOP_1: 3;

      then g is having_a_unity or ( len F) >= 1 & ( len G) >= 1 by SETWISEO:def 2;

      

      hence ( FlattenSeq (F ^ G)) = (g . ((g "**" F),(g "**" G))) by A2, A3, Th41

      .= ((g "**" F) ^ (g "**" G)) by A1

      .= (( FlattenSeq F) ^ (g "**" G)) by A1, Def10

      .= (( FlattenSeq F) ^ ( FlattenSeq G)) by A1, Def10;

    end;

    theorem :: AFINSQ_2:76

    for D be set, p,q be Element of (D ^omega ) holds ( FlattenSeq <%p, q%>) = (p ^ q)

    proof

      let D be set, p,q be Element of (D ^omega );

      consider g be BinOp of (D ^omega ) such that

       A1: for d1,d2 be Element of (D ^omega ) holds (g . (d1,d2)) = (d1 ^ d2) and

       A2: ( FlattenSeq <%p, q%>) = (g "**" <%p, q%>) by Def10;

      

      thus ( FlattenSeq <%p, q%>) = (g . (p,q)) by A2, Th38

      .= (p ^ q) by A1;

    end;

    theorem :: AFINSQ_2:77

    for D be set, p,q,r be Element of (D ^omega ) holds ( FlattenSeq <%p, q, r%>) = ((p ^ q) ^ r)

    proof

      let D be set, p,q,r be Element of (D ^omega );

      consider g be BinOp of (D ^omega ) such that

       A1: for d1,d2 be Element of (D ^omega ) holds (g . (d1,d2)) = (d1 ^ d2) and

       A2: ( FlattenSeq <%p, q, r%>) = (g "**" <%p, q, r%>) by Def10;

      

      thus ( FlattenSeq <%p, q, r%>) = (g . ((g . (p,q)),r)) by A2, Th39

      .= ((g . (p,q)) ^ r) by A1

      .= ((p ^ q) ^ r) by A1;

    end;

    theorem :: AFINSQ_2:78

    

     Th77: p c= q implies (p ^ (q /^ ( len p))) = q

    proof

      assume

       A1: p c= q;

      

       A2: (( len p) + ( len (q /^ ( len p)))) = (( len p) + (( len q) -' ( len p))) by Def2

      .= ((( len q) + ( len p)) -' ( len p)) by A1, NAT_1: 43, NAT_D: 38

      .= ( dom q) by NAT_D: 34;

      

       A3: for k st k in ( dom p) holds (q . k) = (p . k) by A1, GRFUNC_1: 2;

      for k st k in ( dom (q /^ ( len p))) holds (q . (( len p) + k)) = ((q /^ ( len p)) . k) by Def2;

      hence (p ^ (q /^ ( len p))) = q by A2, A3, AFINSQ_1:def 3;

    end;

    reserve r,s for XFinSequence;

    theorem :: AFINSQ_2:79

    

     Th78: p c= q implies ex r st (p ^ r) = q

    proof

      assume

       A1: p c= q;

      take r = (q /^ ( len p));

      thus (p ^ r) = q by A1, Th77;

    end;

    theorem :: AFINSQ_2:80

    

     Th79: for p,q be XFinSequence of D st p c= q holds ex r be XFinSequence of D st (p ^ r) = q

    proof

      let p,q be XFinSequence of D;

      assume p c= q;

      then

      consider r such that

       A1: (p ^ r) = q by Th78;

      reconsider r as XFinSequence of D by A1, AFINSQ_1: 31;

      take r;

      thus thesis by A1;

    end;

    theorem :: AFINSQ_2:81

    q c= r implies (p ^ q) c= (p ^ r)

    proof

      assume q c= r;

      then

      consider s such that

       A1: (q ^ s) = r by Th78;

      (p ^ q) c= ((p ^ q) ^ s) by AFINSQ_1: 74;

      hence thesis by A1, AFINSQ_1: 27;

    end;

    theorem :: AFINSQ_2:82

    for D be set, F,G be XFinSequence of (D ^omega ) holds F c= G implies ( FlattenSeq F) c= ( FlattenSeq G)

    proof

      let D be set, F,G be XFinSequence of (D ^omega );

      assume F c= G;

      then

      consider F9 be XFinSequence of (D ^omega ) such that

       A1: (F ^ F9) = G by Th79;

      (( FlattenSeq F) ^ ( FlattenSeq F9)) = ( FlattenSeq G) by A1, Th74;

      hence thesis by AFINSQ_1: 74;

    end;

    registration

      let p;

      let q be non empty XFinSequence;

      cluster (p ^ q) -> non empty;

      coherence by AFINSQ_1: 30;

      cluster (q ^ p) -> non empty;

      coherence by AFINSQ_1: 30;

    end

    theorem :: AFINSQ_2:83

    ( CutLastLoc (p ^ <%x%>)) = p

    proof

      set q = ( CutLastLoc (p ^ <%x%>));

      

       A1: (( len (p ^ <%x%>)) -' 1) = ((( len p) + 1) -' 1) by AFINSQ_1: 75

      .= ( len p) by NAT_D: 34;

      

       A2: ( dom (p ^ <%x%>)) = ( len (p ^ <%x%>))

      .= ( Segm (( len p) + 1)) by AFINSQ_1: 75

      .= (( Segm ( len p)) \/ {( len p)}) by AFINSQ_1: 2;

      

       A3: not ( len p) in ( dom p);

      ( LastLoc (p ^ <%x%>)) = (( len (p ^ <%x%>)) -' 1) by AFINSQ_1: 70;

      

      hence

       A4: ( dom q) = (( dom (p ^ <%x%>)) \ {( len p)}) by A1, VALUED_1: 36

      .= ( dom p) by A2, A3, ZFMISC_1: 117;

      let y be object;

      assume

       A5: y in ( dom q);

      

       A6: p c= (p ^ <%x%>) by AFINSQ_1: 74;

      

      thus (q . y) = ((p ^ <%x%>) . y) by A5, GRFUNC_1: 2

      .= (p . y) by A5, A4, A6, GRFUNC_1: 2;

    end;

    theorem :: AFINSQ_2:84

    

     Th17: for D be set, p be XFinSequence of D, n be Nat holds ( XFS2FS (p | n)) = (( XFS2FS p) | n) & ( XFS2FS (p /^ n)) = (( XFS2FS p) /^ n)

    proof

      let D be set, p be XFinSequence of D, n be Nat;

      thus ( XFS2FS (p | n)) = (( XFS2FS p) | n)

      proof

         A1:

        now

          let x be object;

          hereby

            assume

             A2: x in ( dom ( XFS2FS (p | n)));

            then

            reconsider m1 = x as Nat;

            

             A3: 1 <= m1 & m1 <= ( len ( XFS2FS (p | n))) by A2, FINSEQ_3: 25;

            then

            reconsider m = (m1 - 1) as Nat by INT_1: 74;

            (m + 1) in ( dom ( XFS2FS (p | n))) by A2;

            then m in ( dom (p | n)) by AFINSQ_1: 95;

            then

             A4: m in ( dom p) & m in n by RELAT_1: 57;

            then

             A5: (m + 1) in ( dom ( XFS2FS p)) by AFINSQ_1: 95;

            m in ( Segm n) by A4;

            then m < n by NAT_1: 44;

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

            then x in ( dom (( XFS2FS p) | ( Seg n))) by A3, A5, FINSEQ_1: 1, RELAT_1: 57;

            hence x in ( dom (( XFS2FS p) | n)) by FINSEQ_1:def 15;

          end;

          assume x in ( dom (( XFS2FS p) | n));

          then x in ( dom (( XFS2FS p) | ( Seg n))) by FINSEQ_1:def 15;

          then

           A6: x in ( dom ( XFS2FS p)) & x in ( Seg n) by RELAT_1: 57;

          then

          reconsider m1 = x as Nat;

          

           A7: 1 <= m1 & m1 <= n by A6, FINSEQ_1: 1;

          then

          reconsider m = (m1 - 1) as Nat by INT_1: 74;

          (m + 1) in ( dom ( XFS2FS p)) by A6;

          then

           A8: m in ( dom p) by AFINSQ_1: 95;

          (m + 1) <= n by A7;

          then m < n by NAT_1: 13;

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

          then m in ( dom (p | n)) by A8, RELAT_1: 57;

          then (m + 1) in ( dom ( XFS2FS (p | n))) by AFINSQ_1: 95;

          hence x in ( dom ( XFS2FS (p | n)));

        end;

        for k be Nat st k in ( dom ( XFS2FS (p | n))) holds (( XFS2FS (p | n)) . k) = ((( XFS2FS p) | n) . k)

        proof

          let k be Nat;

          assume

           A9: k in ( dom ( XFS2FS (p | n)));

          then

           A10: 1 <= k & k <= ( len ( XFS2FS (p | n))) by FINSEQ_3: 25;

          then

          reconsider m = (k - 1) as Nat by INT_1: 74;

          (m + 1) in ( dom ( XFS2FS (p | n))) by A9;

          then

           A11: m in ( dom (p | n)) by AFINSQ_1: 95;

          then m in ( Segm ( len (p | n)));

          then m < ( len (p | n)) by NAT_1: 44;

          then

           A12: (m + 1) <= ( len (p | n)) by NAT_1: 13;

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

          then ( len (p | n)) <= ( len p) by NAT_1: 39;

          then

           A13: k <= ( len p) by A12, XXREAL_0: 2;

          m in ( Segm n) by A11;

          then m < n by NAT_1: 44;

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

          then

           A14: k in ( Seg n) by A10, FINSEQ_1: 1;

          

          thus (( XFS2FS (p | n)) . k) = ((p | n) . ((m + 1) -' 1)) by A10, A12, AFINSQ_1:def 9

          .= ((p | n) . m) by NAT_D: 34

          .= (p . m) by A11, FUNCT_1: 47

          .= (p . ((m + 1) -' 1)) by NAT_D: 34

          .= (( XFS2FS p) . k) by A10, A13, AFINSQ_1:def 9

          .= ((( XFS2FS p) | ( Seg n)) . k) by A14, FUNCT_1: 49

          .= ((( XFS2FS p) | n) . k) by FINSEQ_1:def 15;

        end;

        hence ( XFS2FS (p | n)) = (( XFS2FS p) | n) by A1, TARSKI: 2;

      end;

      per cases ;

        suppose

         A15: ( len p) <= n;

        then (p /^ n) = {} by Th6;

        then

         A16: ( XFS2FS (p /^ n)) = {} ;

        ( len (( XFS2FS p) /^ n)) = 0

        proof

          per cases by A15, XXREAL_0: 1;

            suppose ( len p) < n;

            then

             A17: (( len p) - n) < (n - n) by XREAL_1: 14;

            

            thus ( len (( XFS2FS p) /^ n)) = (( len ( XFS2FS p)) -' n) by RFINSEQ: 29

            .= (( len p) -' n) by AFINSQ_1:def 9

            .= 0 by A17, XREAL_0:def 2;

          end;

            suppose

             A18: ( len p) = n;

            

            thus ( len (( XFS2FS p) /^ n)) = (( len ( XFS2FS p)) -' n) by RFINSEQ: 29

            .= (( 0 + ( len p)) -' n) by AFINSQ_1:def 9

            .= 0 by A18, NAT_D: 34;

          end;

        end;

        hence thesis by A16;

      end;

        suppose

         A19: n < ( len p);

        then

         A20: n <= ( len ( XFS2FS p)) by AFINSQ_1:def 9;

        

         A21: ( len ( XFS2FS (p /^ n))) = ( len (p /^ n)) by AFINSQ_1:def 9

        .= (( len p) -' n) by Def2

        .= (( len ( XFS2FS p)) -' n) by AFINSQ_1:def 9

        .= ( len (( XFS2FS p) /^ n)) by RFINSEQ: 29;

        now

          let k be Nat;

          assume

           A22: 1 <= k & k <= ( len ( XFS2FS (p /^ n)));

          then

           A23: 1 <= k & k <= ( len (p /^ n)) by AFINSQ_1:def 9;

          then

          reconsider m = (k - 1) as Nat by INT_1: 74;

          (m + 1) <= ( len (p /^ n)) by A23;

          then m < ( len (p /^ n)) by NAT_1: 13;

          then m in ( Segm ( len (p /^ n))) by NAT_1: 44;

          then

           A24: m in ( dom (p /^ n));

          

           A25: k in ( dom (( XFS2FS p) /^ n)) by A21, A22, FINSEQ_3: 25;

          

           A26: (1 + 0 ) <= (k + n) by A23, XREAL_1: 7;

          k <= (( len p) - n) by A19, A23, Th7;

          then

           A27: (k + n) <= ((( len p) - n) + n) by XREAL_1: 6;

          

          thus (( XFS2FS (p /^ n)) . k) = ((p /^ n) . ((m + 1) -' 1)) by A23, AFINSQ_1:def 9

          .= ((p /^ n) . m) by NAT_D: 34

          .= (p . (m + n)) by A24, Def2

          .= (p . (((n + m) + 1) -' 1)) by NAT_D: 34

          .= (( XFS2FS p) . (k + n)) by A26, A27, AFINSQ_1:def 9

          .= ((( XFS2FS p) /^ n) . k) by A20, A25, RFINSEQ:def 1;

        end;

        hence thesis by A21;

      end;

    end;

    theorem :: AFINSQ_2:85

    

     Th5: for D be set holds for d be FinSequence of D holds ( XFS2FS ( FS2XFS d)) = d

    proof

      let D be set;

      let d be FinSequence of D;

      set Xd = ( FS2XFS d);

      

       A1: ( len d) = ( len Xd) by AFINSQ_1:def 8;

      

       A2: ( len Xd) = ( len ( XFS2FS Xd)) by AFINSQ_1:def 9;

      now

        let i such that

         A3: 1 <= i and

         A4: i <= ( len d);

        reconsider i1 = (i - 1) as Nat by A3, NAT_1: 21;

        

         A5: (i1 + 1) = i;

        

         A6: (i -' 1) = i1 by XREAL_0:def 2;

        

        thus (d . i) = (Xd . i1) by A4, A5, NAT_1: 13, AFINSQ_1:def 8

        .= (( XFS2FS Xd) . i) by A3, A4, A6, A1, AFINSQ_1:def 9;

      end;

      hence thesis by A1, A2;

    end;

    registration

      let D be set, f be FinSequence of D;

      reduce ( XFS2FS ( FS2XFS f)) to f;

      reducibility by Th5;

    end

    theorem :: AFINSQ_2:86

    for D be set, p be FinSequence of D, n be Nat holds (( FS2XFS p) | n) = ( FS2XFS (p | n)) & (( FS2XFS p) /^ n) = ( FS2XFS (p /^ n))

    proof

      let D be set, p be FinSequence of D, n be Nat;

      

      thus (( FS2XFS p) | n) = ( FS2XFS ( XFS2FS (( FS2XFS p) | n)))

      .= ( FS2XFS (( XFS2FS ( FS2XFS p)) | n)) by Th17

      .= ( FS2XFS (p | n));

      

      thus (( FS2XFS p) /^ n) = ( FS2XFS ( XFS2FS (( FS2XFS p) /^ n)))

      .= ( FS2XFS (( XFS2FS ( FS2XFS p)) /^ n)) by Th17

      .= ( FS2XFS (p /^ n));

    end;

    theorem :: AFINSQ_2:87

    for D be set, p be one-to-one XFinSequence of D, n be Nat holds ( rng (p | n)) misses ( rng (p /^ n))

    proof

      let D be set, p be one-to-one XFinSequence of D, n be Nat;

      ( rng (( XFS2FS p) | n)) misses ( rng (( XFS2FS p) /^ n)) by FINSEQ_5: 34;

      then ( rng (( XFS2FS p) | n)) misses ( rng ( XFS2FS (p /^ n))) by Th17;

      then ( rng ( XFS2FS (p | n))) misses ( rng ( XFS2FS (p /^ n))) by Th17;

      then ( rng ( XFS2FS (p | n))) misses ( rng (p /^ n)) by AFINSQ_1: 97;

      hence ( rng (p | n)) misses ( rng (p /^ n)) by AFINSQ_1: 97;

    end;

    registration

      cluster finite for Ordinal-Sequence;

      existence

      proof

        reconsider f = ( 0 --> omega ) as Ordinal-Sequence;

        take f;

        thus thesis;

      end;

    end

    registration

      let A be finite Ordinal-Sequence, n be Nat;

      cluster (A /^ n) -> Ordinal-yielding;

      coherence

      proof

        consider a be Ordinal such that

         A1: ( rng A) c= a by ORDINAL2:def 4;

        ( rng (A /^ n)) c= ( rng A) by Th9;

        hence thesis by A1, XBOOLE_1: 1, ORDINAL2:def 4;

      end;

    end