finsop_1.miz



    begin

    reserve x,y,y1,y2 for set,

D for non empty set,

d,d1,d2,d3 for Element of D,

F,G,H,H1,H2 for FinSequence of D,

f,f1,f2 for sequence of D,

g for BinOp of D,

k,n,i,l for Nat,

P for Permutation of ( dom F);

    definition

      let D, F, g;

      assume

       A1: g is having_a_unity or ( len F) >= 1;

      :: FINSOP_1:def1

      func g "**" F -> Element of D means

      : Def1: it = ( the_unity_wrt g) if g is having_a_unity & ( len F) = 0

      otherwise ex f st (f . 1) = (F . 1) & (for n be Nat st 0 <> n & n < ( len F) holds (f . (n + 1)) = (g . ((f . n),(F . (n + 1))))) & it = (f . ( len F));

      existence

      proof

        now

          per cases ;

            suppose ( len F) = 0 ;

            hence thesis by A1;

          end;

            suppose

             A2: ( len F) <> 0 ;

            defpred P[ Nat] means for F st ( len F) = $1 & ( len F) <> 0 holds ex d, f st (f . 1) = (F . 1) & (for n be Nat st 0 <> n & n < ( len F) holds (f . (n + 1)) = (g . ((f . n),(F . (n + 1))))) & d = (f . ( len F));

            

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

            proof

              let k;

              assume

               A4: P[k];

              let F;

              assume that

               A5: ( len F) = (k + 1) and ( len F) <> 0 ;

              reconsider G = (F | ( Seg k)) as FinSequence of D by FINSEQ_1: 18;

              

               A6: ( len G) = k by A5, FINSEQ_3: 53;

              now

                per cases ;

                  suppose

                   A7: ( len G) = 0 ;

                  set f = ( NAT --> (F . 1));

                  

                   A8: ( rng f) c= D

                  proof

                    let x be object;

                    assume x in ( rng f);

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

                    then

                     A9: x = (F . 1) by FUNCOP_1: 7;

                    1 in ( dom F) by A5, A6, A7, FINSEQ_3: 25;

                    then

                     A10: x in ( rng F) by A9, FUNCT_1:def 3;

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

                    hence thesis by A10;

                  end;

                  ( dom f) = NAT by FUNCOP_1: 13;

                  then

                  reconsider f as sequence of D by A8, RELSET_1: 4;

                  take d = (f . 1), f;

                  thus (f . 1) = (F . 1) by FUNCOP_1: 7;

                  thus for n be Nat st 0 <> n & n < ( len F) holds (f . (n + 1)) = (g . ((f . n),(F . (n + 1)))) by A5, A6, A7, NAT_1: 14;

                  thus d = (f . ( len F)) by A5, A6, A7;

                end;

                  suppose

                   A11: ( len G) <> 0 ;

                  reconsider j = ( len F) as Element of NAT ;

                  1 <= ( len F) by A5, NAT_1: 12;

                  then ( len F) in ( dom F) by FINSEQ_3: 25;

                  then

                   A12: (F . ( len F)) in ( rng F) by FUNCT_1:def 3;

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

                  then

                  reconsider t = (F . ( len F)) as Element of D by A12;

                  ( len G) >= 1 by A11, NAT_1: 14;

                  then

                   A13: 1 in ( dom G) by FINSEQ_3: 25;

                  consider d, f such that

                   A14: (f . 1) = (G . 1) and

                   A15: for n be Nat st 0 <> n & n < ( len G) holds (f . (n + 1)) = (g . ((f . n),(G . (n + 1)))) and

                   A16: d = (f . ( len G)) by A4, A5, A11, FINSEQ_3: 53;

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

                  consider h be sequence of D such that

                   A17: (h . j) = (g . (d,t)) and

                   A18: for n be Element of NAT st n <> j holds (h . n) = F(n) from FUNCT_2:sch 6;

                  take a = (h . j), h;

                  1 <> j by A5, A11, FINSEQ_3: 53;

                  

                  hence (h . 1) = (G . 1) by A14, A18

                  .= (F . 1) by A13, FUNCT_1: 47;

                  thus for n be Nat st 0 <> n & n < ( len F) holds (h . (n + 1)) = (g . ((h . n),(F . (n + 1))))

                  proof

                    let n be Nat;

                    assume that

                     A19: n <> 0 and

                     A20: n < ( len F);

                    now

                      per cases ;

                        suppose

                         A21: (n + 1) = ( len F);

                        ( len G) <> ( len F) by A5, A6;

                        hence thesis by A5, A6, A16, A17, A18, A21;

                      end;

                        suppose

                         A22: (n + 1) <> ( len F);

                        (n + 1) <= ( len F) by A20, NAT_1: 13;

                        then

                         A23: (n + 1) < ( len F) by A22, XXREAL_0: 1;

                        then

                         A24: n < ( len G) by A5, A6, XREAL_1: 6;

                        1 <= (n + 1) & (n + 1) <= ( len G) by A5, A6, A23, NAT_1: 12, NAT_1: 13;

                        then

                         A25: (n + 1) in ( dom G) by FINSEQ_3: 25;

                        (h . (n + 1)) = (f . (n + 1)) by A18, A22

                        .= (g . ((f . n),(G . (n + 1)))) by A15, A19, A24

                        .= (g . ((f . n),(F . (n + 1)))) by A25, FUNCT_1: 47

                        .= (g . ((h . ( In (n, NAT ))),(F . (n + 1)))) by A18, A20;

                        hence thesis;

                      end;

                    end;

                    hence thesis;

                  end;

                  thus a = (h . ( len F));

                end;

              end;

              hence thesis;

            end;

            

             A26: P[ 0 ];

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

            hence thesis by A2;

          end;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let d1, d2;

        thus g is having_a_unity & ( len F) = 0 & d1 = ( the_unity_wrt g) & d2 = ( the_unity_wrt g) implies d1 = d2;

        assume

         A27: not g is having_a_unity or ( len F) <> 0 ;

        given f1 such that

         A28: (f1 . 1) = (F . 1) and

         A29: for n be Nat st 0 <> n & n < ( len F) holds (f1 . (n + 1)) = (g . ((f1 . n),(F . (n + 1)))) and

         A30: d1 = (f1 . ( len F));

        given f2 such that

         A31: (f2 . 1) = (F . 1) and

         A32: for n be Nat st 0 <> n & n < ( len F) holds (f2 . (n + 1)) = (g . ((f2 . n),(F . (n + 1)))) and

         A33: d2 = (f2 . ( len F));

        defpred P[ Nat] means $1 <> 0 & $1 <= ( len F) implies (f1 . $1) = (f2 . $1);

        

         A34: for n st P[n] holds P[(n + 1)]

        proof

          let n;

          assume

           A35: n <> 0 & n <= ( len F) implies (f1 . n) = (f2 . n);

          assume that (n + 1) <> 0 and

           A36: (n + 1) <= ( len F);

          now

            per cases ;

              suppose n = 0 ;

              hence thesis by A28, A31;

            end;

              suppose

               A37: n <> 0 ;

              

               A38: n < ( len F) by A36, NAT_1: 13;

              then (f1 . (n + 1)) = (g . ((f1 . n),(F . (n + 1)))) by A29, A37;

              hence thesis by A32, A35, A37, A38;

            end;

          end;

          hence thesis;

        end;

        

         A39: P[ 0 ];

        for n holds P[n] from NAT_1:sch 2( A39, A34);

        hence thesis by A1, A27, A30, A33;

      end;

      consistency ;

    end

    theorem :: FINSOP_1:1

    ( len F) >= 1 implies ex f st (f . 1) = (F . 1) & (for n be Nat st 0 <> n & n < ( len F) holds (f . (n + 1)) = (g . ((f . n),(F . (n + 1))))) & (g "**" F) = (f . ( len F)) by Def1;

    theorem :: FINSOP_1:2

    ( len F) >= 1 & (ex f st (f . 1) = (F . 1) & (for n be Nat st 0 <> n & n < ( len F) holds (f . (n + 1)) = (g . ((f . n),(F . (n + 1))))) & d = (f . ( len F))) implies d = (g "**" F) by Def1;

    definition

      let A be non empty set, F be sequence of A, p be FinSequence of A;

      :: original: +*

      redefine

      func F +* p -> sequence of A ;

      coherence

      proof

        

         A1: ( dom F) = NAT by FUNCT_2:def 1;

        ( dom (F +* p)) = (( dom F) \/ ( dom p)) by FUNCT_4:def 1

        .= NAT by A1, XBOOLE_1: 12;

        hence thesis by FUNCT_2:def 1;

      end;

    end

    notation

      let f be FinSequence;

      synonym findom f for dom f;

    end

    definition

      let f be FinSequence;

      :: original: findom

      redefine

      func findom f -> Element of ( Fin NAT ) ;

      coherence

      proof

        ( dom f) = ( Seg ( len f)) by FINSEQ_1:def 3;

        hence thesis by FINSUB_1:def 5;

      end;

    end

    

     Lm1: ( len F) >= 1 & g is associative & g is commutative implies (g "**" F) = (g $$ (( findom F),(( NAT --> ( the_unity_wrt g)) +* F)))

    proof

      assume that

       A1: ( len F) >= 1 and

       A2: g is associative & g is commutative;

      set A = ( findom F);

      set h = (( NAT --> ( the_unity_wrt g)) +* F);

      

       A3: ( dom F) = ( Seg ( len F)) by FINSEQ_1:def 3;

      then

      consider G be Function of ( Fin NAT ), D such that

       A4: (g $$ (A,h)) = (G . A) and for d st d is_a_unity_wrt g holds (G . {} ) = d and

       A5: for n be Element of NAT holds (G . {n}) = (h . n) and

       A6: for B be Element of ( Fin NAT ) st B c= A & B <> {} holds for n be Element of NAT st n in (A \ B) holds (G . (B \/ {n})) = (g . ((G . B),(h . n))) by A1, A2, SETWISEO:def 3;

      consider f such that

       A7: (f . 1) = (F . 1) and

       A8: for n be Nat st 0 <> n & n < ( len F) holds (f . (n + 1)) = (g . ((f . n),(F . (n + 1)))) and

       A9: (g "**" F) = (f . ( len F)) by A1, Def1;

      defpred P[ Nat] means $1 <> 0 & $1 <= ( len F) implies (f . $1) = (G . ( Seg $1));

      

       A10: for n st P[n] holds P[(n + 1)]

      proof

        let n;

        assume

         A11: n <> 0 & n <= ( len F) implies (f . n) = (G . ( Seg n));

        assume that (n + 1) <> 0 and

         A12: (n + 1) <= ( len F);

        now

          per cases ;

            suppose

             A13: n = 0 ;

            1 in ( dom F) by A1, A3, FINSEQ_1: 1;

            then (h . 1) = (F . 1) by FUNCT_4: 13;

            hence thesis by A7, A5, A13, FINSEQ_1: 2;

          end;

            suppose

             A14: n <> 0 ;

            reconsider B = ( Seg n) as Element of ( Fin NAT ) by FINSUB_1:def 5;

            (n + 1) >= 1 by NAT_1: 12;

            then

             A15: (n + 1) in ( dom F) by A12, FINSEQ_3: 25;

            

             A16: n < ( len F) by A12, NAT_1: 13;

            then

             A17: (f . (n + 1)) = (g . ((f . n),(F . (n + 1)))) by A8, A14;

             not (n + 1) in ( Seg n) by FINSEQ_3: 10;

            then

             A18: (n + 1) in (A \ ( Seg n)) by A15, XBOOLE_0:def 5;

            

             A19: ( Seg n) c= A by A3, A16, FINSEQ_1: 5;

            (G . ( Seg (n + 1))) = (G . (( Seg n) \/ {(n + 1)})) by FINSEQ_1: 9

            .= (g . ((G . B),(h . (n + 1)))) by A6, A14, A19, A18;

            hence thesis by A11, A12, A14, A17, A15, FUNCT_4: 13, NAT_1: 13;

          end;

        end;

        hence thesis;

      end;

      

       A20: P[ 0 ];

      for n holds P[n] from NAT_1:sch 2( A20, A10);

      hence thesis by A1, A9, A3, A4;

    end;

    

     Lm2: ( len F) = 0 & g is having_a_unity & g is associative & g is commutative implies (g "**" F) = (g $$ (( findom F),(( NAT --> ( the_unity_wrt g)) +* F)))

    proof

      assume that

       A1: ( len F) = 0 and

       A2: g is having_a_unity and

       A3: g is associative & g is commutative;

      F = {} by A1;

      then

       A4: ( dom F) = ( {}. NAT );

      

      thus (g "**" F) = ( the_unity_wrt g) by A1, A2, Def1

      .= (g $$ (( findom F),(( NAT --> ( the_unity_wrt g)) +* F))) by A2, A3, A4, SETWISEO: 31;

    end;

    theorem :: FINSOP_1:3

    (g is having_a_unity or ( len F) >= 1) & g is associative & g is commutative implies (g "**" F) = (g $$ (( findom F),(( NAT --> ( the_unity_wrt g)) +* F)))

    proof

      ( len F) = 0 or ( len F) >= 1 by NAT_1: 14;

      hence thesis by Lm1, Lm2;

    end;

    

     Lm3: g is having_a_unity implies (g "**" ( <*> D)) = ( the_unity_wrt g)

    proof

      

       A1: ( len ( <*> D)) = 0 ;

      assume g is having_a_unity;

      hence thesis by A1, Def1;

    end;

    

     Lm4: (g "**" <*d*>) = d

    proof

      

       A1: ( len <*d*>) = 1 by FINSEQ_1: 39;

      then ex f st (f . 1) = ( <*d*> . 1) & (for n be Nat st 0 <> n & n < ( len <*d*>) holds (f . (n + 1)) = (g . ((f . n),( <*d*> . (n + 1))))) & (g "**" <*d*>) = (f . ( len <*d*>)) by Def1;

      hence thesis by A1, FINSEQ_1:def 8;

    end;

    

     Lm5: ( len F) >= 1 implies (g "**" (F ^ <*d*>)) = (g . ((g "**" F),d))

    proof

      set G = (F ^ <*d*>);

      

       A1: (G . (( len F) + 1)) = d by FINSEQ_1: 42;

      

       A2: ( len G) = (( len F) + ( len <*d*>)) by FINSEQ_1: 22

      .= (( len F) + 1) by FINSEQ_1: 39;

      then 1 <= ( len G) by NAT_1: 12;

      then

      consider f1 such that

       A3: (f1 . 1) = (G . 1) and

       A4: for n be Nat st 0 <> n & n < ( len G) holds (f1 . (n + 1)) = (g . ((f1 . n),(G . (n + 1)))) and

       A5: (g "**" G) = (f1 . ( len G)) by Def1;

      assume

       A6: ( len F) >= 1;

      then

      consider f such that

       A7: (f . 1) = (F . 1) and

       A8: for n be Nat st 0 <> n & n < ( len F) holds (f . (n + 1)) = (g . ((f . n),(F . (n + 1)))) and

       A9: (g "**" F) = (f . ( len F)) by Def1;

      defpred P[ Nat] means 0 <> $1 & $1 < ( len G) implies (f . $1) = (f1 . $1);

      

       A10: for n st P[n] holds P[(n + 1)]

      proof

        let n;

        assume

         A11: P[n];

        assume that 0 <> (n + 1) and

         A12: (n + 1) < ( len G);

        

         A13: (n + 1) >= 1 by NAT_1: 14;

        now

          per cases by A13, XXREAL_0: 1;

            suppose

             A14: (n + 1) = 1;

            1 in ( dom F) by A6, FINSEQ_3: 25;

            hence thesis by A7, A3, A14, FINSEQ_1:def 7;

          end;

            suppose

             A15: (n + 1) > 1;

            then n <> 0 ;

            then

             A16: (f1 . (n + 1)) = (g . ((f1 . n),(G . (n + 1)))) by A4, A12, NAT_1: 12;

            

             A17: (n + 1) <= ( len F) by A2, A12, NAT_1: 13;

            then

             A18: n < ( len F) by NAT_1: 13;

            1 <= (n + 1) by NAT_1: 12;

            then

             A19: (n + 1) in ( dom F) by A17, FINSEQ_3: 25;

            (n + 1) > ( 0 + 1) by A15;

            then (f . (n + 1)) = (g . ((f . n),(F . (n + 1)))) by A8, A18;

            hence thesis by A11, A12, A15, A16, A19, FINSEQ_1:def 7, NAT_1: 12;

          end;

        end;

        hence thesis;

      end;

      

       A20: P[ 0 ];

      

       A21: for n holds P[n] from NAT_1:sch 2( A20, A10);

      (g "**" G) = (g . ((f1 . ( len F)),(G . (( len F) + 1)))) by A6, A2, A4, A5, XREAL_1: 29;

      hence thesis by A6, A9, A2, A1, A21, XREAL_1: 29;

    end;

    

     Lm6: g is having_a_unity & ( len F) = 0 implies (g "**" (F ^ <*d*>)) = (g . ((g "**" F),d))

    proof

      assume that

       A1: g is having_a_unity and

       A2: ( len F) = 0 ;

      F = ( <*> D) by A2;

      

      hence (g "**" (F ^ <*d*>)) = (g "**" <*d*>) by FINSEQ_1: 34

      .= d by Lm4

      .= (g . (( the_unity_wrt g),d)) by A1, SETWISEO: 15

      .= (g . ((g "**" F),d)) by A1, A2, Def1;

    end;

    theorem :: FINSOP_1:4

    

     Th4: g is having_a_unity or ( len F) >= 1 implies (g "**" (F ^ <*d*>)) = (g . ((g "**" F),d))

    proof

      ( len F) >= 1 or ( len F) = 0 by NAT_1: 14;

      hence thesis by Lm5, Lm6;

    end;

    theorem :: FINSOP_1:5

    

     Th5: g is associative & (g is having_a_unity or ( len F) >= 1 & ( len G) >= 1) implies (g "**" (F ^ G)) = (g . ((g "**" F),(g "**" G)))

    proof

      defpred P[ FinSequence of D] means for F, g st g is associative & (g is having_a_unity or ( len F) >= 1 & ( len $1) >= 1) holds (g "**" (F ^ $1)) = (g . ((g "**" F),(g "**" $1)));

      

       A1: for G, d st P[G] holds P[(G ^ <*d*>)]

      proof

        let G, d;

        assume

         A2: P[G];

        let F, g;

        assume that

         A3: g is associative and

         A4: g is having_a_unity or ( len F) >= 1 & ( len (G ^ <*d*>)) >= 1;

         A5:

        now

          

           A6: ( len (F ^ G)) = (( len F) + ( len G)) by FINSEQ_1: 22;

          assume not g is having_a_unity;

          hence ( len (F ^ G)) >= 1 by A4, A6, NAT_1: 12;

        end;

        

         A7: (g "**" (F ^ (G ^ <*d*>))) = (g "**" ((F ^ G) ^ <*d*>)) by FINSEQ_1: 32

        .= (g . ((g "**" (F ^ G)),d)) by A5, Th4;

        now

          per cases ;

            suppose

             A8: ( len G) <> 0 ;

            then ( len G) >= 1 by NAT_1: 14;

            

            hence (g "**" (F ^ (G ^ <*d*>))) = (g . ((g . ((g "**" F),(g "**" G))),d)) by A2, A3, A4, A7

            .= (g . ((g "**" F),(g . ((g "**" G),d)))) by A3, BINOP_1:def 3

            .= (g . ((g "**" F),(g "**" (G ^ <*d*>)))) by A8, Th4, NAT_1: 14;

          end;

            suppose ( len G) = 0 ;

            then

             A9: G = {} ;

            

            hence (g "**" (F ^ (G ^ <*d*>))) = (g "**" (F ^ <*d*>)) by FINSEQ_1: 34

            .= (g . ((g "**" F),d)) by A4, Th4

            .= (g . ((g "**" F),(g "**" <*d*>))) by Lm4

            .= (g . ((g "**" F),(g "**" (G ^ <*d*>)))) by A9, FINSEQ_1: 34;

          end;

        end;

        hence thesis;

      end;

      

       A10: P[( <*> D)]

      proof

        let F, g;

        assume that g is associative and

         A11: g is having_a_unity or ( len F) >= 1 & ( len ( <*> D)) >= 1;

        

        thus (g "**" (F ^ ( <*> D))) = (g "**" F) by FINSEQ_1: 34

        .= (g . ((g "**" F),( the_unity_wrt g))) by A11, SETWISEO: 15

        .= (g . ((g "**" F),(g "**" ( <*> D)))) by A11, Lm3;

      end;

      for G holds P[G] from FINSEQ_2:sch 2( A10, A1);

      hence thesis;

    end;

    theorem :: FINSOP_1:6

    

     Th6: g is associative & (g is having_a_unity or ( len F) >= 1) implies (g "**" ( <*d*> ^ F)) = (g . (d,(g "**" F)))

    proof

      

       A1: ( len <*d*>) = 1 by FINSEQ_1: 39;

      assume g is associative & (g is having_a_unity or ( len F) >= 1);

      

      hence (g "**" ( <*d*> ^ F)) = (g . ((g "**" <*d*>),(g "**" F))) by A1, Th5

      .= (g . (d,(g "**" F))) by Lm4;

    end;

    

     Lm7: g is associative & g is commutative implies for f be Permutation of ( dom F) st ( len F) >= 1 & ( len F) = ( len G) & (for i st i in ( dom G) holds (G . i) = (F . (f . i))) holds (g "**" F) = (g "**" G)

    proof

      assume that

       A1: g is associative and

       A2: g is commutative;

      defpred P[ Nat] means for H1, H2 st ( len H1) >= 1 & ( len H1) = $1 & ( len H1) = ( len H2) holds for f be Permutation of ( dom H1) st (for i st i in ( dom H2) holds (H2 . i) = (H1 . (f . i))) holds (g "**" H1) = (g "**" H2);

       A3:

      now

        let k;

        assume

         A4: P[k];

        thus P[(k + 1)]

        proof

          let H1, H2;

          assume that ( len H1) >= 1 and

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

           A6: ( len H1) = ( len H2);

          reconsider p = (H2 | ( Seg k)) as FinSequence of D by FINSEQ_1: 18;

          let f be Permutation of ( dom H1);

          

           A7: ( dom H1) = ( Seg (k + 1)) by A5, FINSEQ_1:def 3;

          then

           A8: ( rng f) = ( Seg (k + 1)) by FUNCT_2:def 3;

           A9:

          now

            let n;

            assume n in ( dom f);

            then (f . n) in ( Seg (k + 1)) by A8, FUNCT_1:def 3;

            hence (f . n) is Element of NAT ;

          end;

          

           A10: ( rng H2) c= D by FINSEQ_1:def 4;

          

           A11: ( dom f) = ( Seg (k + 1)) by A7, FUNCT_2:def 1;

          

           A12: (k + 1) in ( Seg (k + 1)) by FINSEQ_1: 4;

          then

           A13: (f . (k + 1)) in ( Seg (k + 1)) by A11, A8, FUNCT_1:def 3;

          then

          reconsider n = (f . (k + 1)) as Element of NAT ;

          

           A14: ( dom H2) = ( Seg (k + 1)) by A5, A6, FINSEQ_1:def 3;

          then (H2 . (k + 1)) in ( rng H2) by A12, FUNCT_1:def 3;

          then

          reconsider d = (H2 . (k + 1)) as Element of D by A10;

          

           A15: n <= (k + 1) by A13, FINSEQ_1: 1;

          then

          consider m2 be Nat such that

           A16: (n + m2) = (k + 1) by NAT_1: 10;

          defpred P[ Nat, object] means $2 = (H1 . (n + $1));

          1 <= n by A13, FINSEQ_1: 1;

          then

          consider m1 be Nat such that

           A17: (1 + m1) = n by NAT_1: 10;

          reconsider m1, m2 as Element of NAT by ORDINAL1:def 12;

          

           A18: for j be Nat st j in ( Seg m2) holds ex x be object st P[j, x];

          consider q2 be FinSequence such that

           A19: ( dom q2) = ( Seg m2) and

           A20: for k be Nat st k in ( Seg m2) holds P[k, (q2 . k)] from FINSEQ_1:sch 1( A18);

          ( rng q2) c= D

          proof

            let x be object;

            assume x in ( rng q2);

            then

            consider y be object such that

             A21: y in ( findom q2) and

             A22: x = (q2 . y) by FUNCT_1:def 3;

            reconsider y as Element of NAT by A21, SETWISEO: 9;

            1 <= y by A19, A21, FINSEQ_1: 1;

            then

             A23: 1 <= (n + y) by NAT_1: 12;

            y <= m2 by A19, A21, FINSEQ_1: 1;

            then (n + y) <= ( len H1) by A5, A16, XREAL_1: 7;

            then (n + y) in ( Seg ( len H1)) by A23, FINSEQ_1: 1;

            then (n + y) in ( dom H1) by FINSEQ_1:def 3;

            then

             A24: (H1 . (n + y)) in ( rng H1) by FUNCT_1:def 3;

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

            then

            reconsider xx = (H1 . (n + y)) as Element of D by A24;

            xx in D;

            hence thesis by A19, A20, A21, A22;

          end;

          then

          reconsider q2 as FinSequence of D by FINSEQ_1:def 4;

          reconsider q1 = (H1 | ( Seg m1)) as FinSequence of D by FINSEQ_1: 18;

          defpred P[ Nat, object] means ((f . $1) in ( dom q1) implies $2 = (f . $1)) & ( not (f . $1) in ( dom q1) implies for l st l = (f . $1) holds $2 = (l - 1));

          

           A25: k <= (k + 1) by NAT_1: 12;

          then

           A26: ( Seg k) c= ( Seg (k + 1)) by FINSEQ_1: 5;

          

           A27: for i be Nat st i in ( Seg k) holds ex y be object st P[i, y]

          proof

            let i be Nat;

            assume

             A28: i in ( Seg k);

            now

              (f . i) in ( Seg (k + 1)) by A11, A8, A26, A28, FUNCT_1:def 3;

              then

              reconsider j = (f . i) as Element of NAT ;

              assume

               A29: not (f . i) in ( dom q1);

              take y = (j - 1);

              thus (f . i) in ( dom q1) implies y = (f . i) by A29;

              assume not (f . i) in ( dom q1);

              let t be Nat;

              assume t = (f . i);

              hence y = (t - 1);

            end;

            hence thesis;

          end;

          consider gg be FinSequence such that

           A30: ( dom gg) = ( Seg k) and

           A31: for i be Nat st i in ( Seg k) holds P[i, (gg . i)] from FINSEQ_1:sch 1( A27);

          

           A32: ( dom p) = ( Seg k) by A5, A6, A25, FINSEQ_1: 17;

          m1 <= n by A17, NAT_1: 11;

          then

           A33: m1 <= (k + 1) by A15, XXREAL_0: 2;

          then

           A34: ( dom q1) = ( Seg m1) by A5, FINSEQ_1: 17;

           A35:

          now

            let i, l;

            assume that

             A36: l = (f . i) and

             A37: not (f . i) in ( dom q1) and

             A38: i in ( dom gg);

            

             A39: l < 1 or m1 < l by A34, A36, A37, FINSEQ_1: 1;

             A40:

            now

              assume (m1 + 1) = l;

              then (k + 1) = i by A12, A11, A17, A26, A30, A36, A38, FUNCT_1:def 4;

              then (k + 1) <= (k + 0 ) by A30, A38, FINSEQ_1: 1;

              hence contradiction by XREAL_1: 6;

            end;

            (f . i) in ( rng f) by A11, A26, A30, A38, FUNCT_1:def 3;

            then (m1 + 1) <= l by A8, A36, A39, FINSEQ_1: 1, NAT_1: 13;

            then (m1 + 1) < l by A40, XXREAL_0: 1;

            then ((m1 + 1) + 1) <= l by NAT_1: 13;

            hence (m1 + 2) <= l;

          end;

          (1 + k) = (1 + (m1 + m2)) by A17, A16;

          then

           A41: m1 <= k by NAT_1: 11;

          

           A42: ( rng gg) c= ( dom p)

          proof

            let y be object;

            assume y in ( rng gg);

            then

            consider x be object such that

             A43: x in ( findom gg) and

             A44: (gg . x) = y by FUNCT_1:def 3;

            reconsider x as Element of NAT by A43, SETWISEO: 9;

            now

              per cases ;

                suppose

                 A45: (f . x) in ( dom q1);

                

                 A46: ( dom q1) c= ( dom p) by A41, A34, A32, FINSEQ_1: 5;

                (f . x) = (gg . x) by A30, A31, A43, A45;

                hence thesis by A44, A45, A46;

              end;

                suppose

                 A47: not (f . x) in ( dom q1);

                reconsider j = (f . x) as Element of NAT by A11, A26, A9, A30, A43;

                

                 A48: (f . x) in ( Seg (k + 1)) by A11, A8, A26, A30, A43, FUNCT_1:def 3;

                j < 1 or m1 < j by A34, A47, FINSEQ_1: 1;

                then

                reconsider l = (j - 1) as Element of NAT by A48, FINSEQ_1: 1, NAT_1: 20;

                j <= (k + 1) by A48, FINSEQ_1: 1;

                then

                 A49: l <= ((k + 1) - 1) by XREAL_1: 9;

                (m1 + 2) <= j by A35, A43, A47;

                then

                 A50: ((m1 + 2) - 1) <= l by XREAL_1: 9;

                1 <= (m1 + 1) by NAT_1: 12;

                then

                 A51: 1 <= l by A50, XXREAL_0: 2;

                (gg . x) = (j - 1) by A30, A31, A43, A47;

                hence thesis by A32, A44, A51, A49, FINSEQ_1: 1;

              end;

            end;

            hence thesis;

          end;

          

           A52: ( len q1) = m1 by A5, A33, FINSEQ_1: 17;

           A53:

          now

            let j be Nat;

            assume

             A54: j in ( dom q2);

            ( len (q1 ^ <*d*>)) = (m1 + ( len <*d*>)) by A52, FINSEQ_1: 22

            .= n by A17, FINSEQ_1: 39;

            hence (H1 . (( len (q1 ^ <*d*>)) + j)) = (q2 . j) by A19, A20, A54;

          end;

          set q = (q1 ^ q2);

          

           A55: ( len q2) = m2 by A19, FINSEQ_1:def 3;

          then

           A56: ( len q) = (m1 + m2) by A52, FINSEQ_1: 22;

          then

           A57: ( dom q) = ( Seg k) by A17, A16, FINSEQ_1:def 3;

          then

          reconsider gg as Function of ( dom q), ( dom q) by A32, A30, A42, FUNCT_2: 2;

          

           A58: ( len p) = k by A5, A6, A25, FINSEQ_1: 17;

          

           A59: ( rng gg) = ( dom q)

          proof

            thus ( rng gg) c= ( dom q) by A17, A16, A56, A32, A42, FINSEQ_1:def 3;

            let y be object;

            assume

             A60: y in ( dom q);

            then

            reconsider j = y as Element of NAT ;

            consider x be object such that

             A61: x in ( dom f) and

             A62: (f . x) = y by A8, A26, A57, A60, FUNCT_1:def 3;

            reconsider x as Element of NAT by A11, A61;

            now

              per cases ;

                suppose

                 A63: x in ( dom gg);

                now

                  per cases ;

                    suppose (f . x) in ( dom q1);

                    then (gg . x) = (f . x) by A30, A31, A63;

                    hence thesis by A62, A63, FUNCT_1:def 3;

                  end;

                    suppose

                     A64: not (f . x) in ( dom q1);

                    j <= k by A57, A60, FINSEQ_1: 1;

                    then 1 <= (j + 1) & (j + 1) <= (k + 1) by NAT_1: 12, XREAL_1: 7;

                    then (j + 1) in ( rng f) by A8, FINSEQ_1: 1;

                    then

                    consider x1 be object such that

                     A65: x1 in ( dom f) and

                     A66: (f . x1) = (j + 1) by FUNCT_1:def 3;

                     A67:

                    now

                      assume not x1 in ( dom gg);

                      then x1 in (( Seg (k + 1)) \ ( Seg k)) by A7, A30, A65, XBOOLE_0:def 5;

                      then x1 in {(k + 1)} by FINSEQ_3: 15;

                      then

                       A68: (j + 1) = (m1 + 1) by A17, A66, TARSKI:def 1;

                      1 <= j by A57, A60, FINSEQ_1: 1;

                      hence contradiction by A34, A62, A64, A68, FINSEQ_1: 1;

                    end;

                    j < 1 or m1 < j by A34, A62, A64, FINSEQ_1: 1;

                    then not (j + 1) <= m1 by A57, A60, FINSEQ_1: 1, NAT_1: 13;

                    then not (f . x1) in ( dom q1) by A34, A66, FINSEQ_1: 1;

                    

                    then (gg . x1) = ((j + 1) - 1) by A30, A31, A66, A67

                    .= y;

                    hence thesis by A67, FUNCT_1:def 3;

                  end;

                end;

                hence thesis;

              end;

                suppose

                 A69: not x in ( dom gg);

                j <= k by A57, A60, FINSEQ_1: 1;

                then 1 <= (j + 1) & (j + 1) <= (k + 1) by NAT_1: 12, XREAL_1: 7;

                then (j + 1) in ( rng f) by A8, FINSEQ_1: 1;

                then

                consider x1 be object such that

                 A70: x1 in ( dom f) and

                 A71: (f . x1) = (j + 1) by FUNCT_1:def 3;

                x in (( Seg (k + 1)) \ ( Seg k)) by A7, A30, A61, A69, XBOOLE_0:def 5;

                then x in {(k + 1)} by FINSEQ_3: 15;

                then

                 A72: x = (k + 1) by TARSKI:def 1;

                 A73:

                now

                  assume not x1 in ( dom gg);

                  then x1 in (( Seg (k + 1)) \ ( Seg k)) by A7, A30, A70, XBOOLE_0:def 5;

                  then x1 in {(k + 1)} by FINSEQ_3: 15;

                  then (j + 1) = (j + 0 ) by A62, A72, A71, TARSKI:def 1;

                  hence contradiction;

                end;

                m1 <= j by A17, A62, A72, XREAL_1: 29;

                then not (j + 1) <= m1 by NAT_1: 13;

                then not (f . x1) in ( dom q1) by A34, A71, FINSEQ_1: 1;

                

                then (gg . x1) = ((j + 1) - 1) by A30, A31, A71, A73

                .= y;

                hence thesis by A73, FUNCT_1:def 3;

              end;

            end;

            hence thesis;

          end;

          assume

           A74: for i st i in ( dom H2) holds (H2 . i) = (H1 . (f . i));

          then

           A75: (H2 . (k + 1)) = (H1 . (f . (k + 1))) by A14, FINSEQ_1: 4;

           A76:

          now

            let j be Nat;

            assume

             A77: j in ( dom (q1 ^ <*d*>));

             A78:

            now

              assume j in ( Seg m1);

              then

               A79: j in ( dom q1) by A5, A33, FINSEQ_1: 17;

              then (q1 . j) = (H1 . j) by FUNCT_1: 47;

              hence (H1 . j) = ((q1 ^ <*d*>) . j) by A79, FINSEQ_1:def 7;

            end;

             A80:

            now

              1 in ( Seg 1) & ( len <*d*>) = 1 by FINSEQ_1: 1, FINSEQ_1: 39;

              then 1 in ( dom <*d*>) by FINSEQ_1:def 3;

              then

               A81: ((q1 ^ <*d*>) . (( len q1) + 1)) = ( <*d*> . 1) by FINSEQ_1:def 7;

              assume j in {n};

              then j = n by TARSKI:def 1;

              hence ((q1 ^ <*d*>) . j) = (H1 . j) by A75, A17, A52, A81, FINSEQ_1: 40;

            end;

            ( len (q1 ^ <*d*>)) = (m1 + ( len <*d*>)) by A52, FINSEQ_1: 22

            .= (m1 + 1) by FINSEQ_1: 40;

            then j in ( Seg (m1 + 1)) by A77, FINSEQ_1:def 3;

            then j in (( Seg m1) \/ {n}) by A17, FINSEQ_1: 9;

            hence (H1 . j) = ((q1 ^ <*d*>) . j) by A78, A80, XBOOLE_0:def 3;

          end;

          gg is one-to-one

          proof

            let y1,y2 be object;

            assume that

             A82: y1 in ( dom gg) and

             A83: y2 in ( dom gg) and

             A84: (gg . y1) = (gg . y2);

            reconsider j1 = y1, j2 = y2 as Element of NAT by A30, A82, A83;

            

             A85: (f . y2) in ( Seg (k + 1)) by A11, A8, A26, A30, A83, FUNCT_1:def 3;

            

             A86: (f . y1) in ( Seg (k + 1)) by A11, A8, A26, A30, A82, FUNCT_1:def 3;

            then

            reconsider a = (f . y1), b = (f . y2) as Element of NAT by A85;

            now

              per cases ;

                suppose (f . y1) in ( dom q1) & (f . y2) in ( dom q1);

                then (gg . j1) = (f . y1) & (gg . j2) = (f . y2) by A30, A31, A82, A83;

                hence thesis by A11, A26, A30, A82, A83, A84, FUNCT_1:def 4;

              end;

                suppose

                 A87: (f . y1) in ( dom q1) & not (f . y2) in ( dom q1);

                then

                 A88: a <= m1 by A34, FINSEQ_1: 1;

                (gg . j1) = a & (gg . j2) = (b - 1) by A30, A31, A82, A83, A87;

                then

                 A89: ((b - 1) + 1) <= (m1 + 1) by A84, A88, XREAL_1: 6;

                1 <= b by A85, FINSEQ_1: 1;

                then

                 A90: b in ( Seg (m1 + 1)) by A89, FINSEQ_1: 1;

                 not b in ( Seg m1) by A5, A33, A87, FINSEQ_1: 17;

                then b in (( Seg (m1 + 1)) \ ( Seg m1)) by A90, XBOOLE_0:def 5;

                then b in {(m1 + 1)} by FINSEQ_3: 15;

                then b = (m1 + 1) by TARSKI:def 1;

                then y2 = (k + 1) by A12, A11, A17, A26, A30, A83, FUNCT_1:def 4;

                hence thesis by A30, A83, FINSEQ_3: 8;

              end;

                suppose

                 A91: not (f . y1) in ( dom q1) & (f . y2) in ( dom q1);

                then

                 A92: b <= m1 by A34, FINSEQ_1: 1;

                (gg . j1) = (a - 1) & (gg . j2) = b by A30, A31, A82, A83, A91;

                then

                 A93: ((a - 1) + 1) <= (m1 + 1) by A84, A92, XREAL_1: 6;

                1 <= a by A86, FINSEQ_1: 1;

                then

                 A94: a in ( Seg (m1 + 1)) by A93, FINSEQ_1: 1;

                 not a in ( Seg m1) by A5, A33, A91, FINSEQ_1: 17;

                then a in (( Seg (m1 + 1)) \ ( Seg m1)) by A94, XBOOLE_0:def 5;

                then a in {(m1 + 1)} by FINSEQ_3: 15;

                then a = (m1 + 1) by TARSKI:def 1;

                then y1 = (k + 1) by A12, A11, A17, A26, A30, A82, FUNCT_1:def 4;

                hence thesis by A30, A82, FINSEQ_3: 8;

              end;

                suppose

                 A95: not (f . y1) in ( dom q1) & not (f . y2) in ( dom q1);

                then (gg . j2) = (b - 1) by A30, A31, A83;

                then

                 A96: (gg . y2) = (b + ( - 1));

                (gg . j1) = (a - 1) by A30, A31, A82, A95;

                then (gg . j1) = (a + ( - 1));

                then a = b by A84, A96, XCMPLX_1: 2;

                hence thesis by A11, A26, A30, A82, A83, FUNCT_1:def 4;

              end;

            end;

            hence thesis;

          end;

          then

          reconsider gg as Permutation of ( dom q) by A59, FUNCT_2: 57;

          (( len (q1 ^ <*d*>)) + ( len q2)) = ((( len q1) + ( len <*d*>)) + m2) by A55, FINSEQ_1: 22

          .= (k + 1) by A17, A16, A52, FINSEQ_1: 40;

          then ( dom H1) = ( Seg (( len (q1 ^ <*d*>)) + ( len q2))) by A5, FINSEQ_1:def 3;

          then

           A97: H1 = ((q1 ^ <*d*>) ^ q2) by A76, A53, FINSEQ_1:def 7;

           A98:

          now

            let i;

            assume

             A99: i in ( dom p);

            then (f . i) in ( rng f) by A11, A26, A32, FUNCT_1:def 3;

            then

            reconsider j = (f . i) as Element of NAT by A8;

            now

              per cases ;

                suppose

                 A100: (f . i) in ( dom q1);

                then

                 A101: (f . i) = (gg . i) & (H1 . j) = (q1 . j) by A32, A31, A99, FUNCT_1: 47;

                (H2 . i) = (p . i) & (H2 . i) = (H1 . (f . i)) by A74, A14, A26, A32, A99, FUNCT_1: 47;

                hence (p . i) = (q . (gg . i)) by A100, A101, FINSEQ_1:def 7;

              end;

                suppose

                 A102: not (f . i) in ( dom q1);

                then (m1 + 2) <= j by A32, A30, A35, A99;

                then

                 A103: ((m1 + 2) - 1) <= (j - 1) by XREAL_1: 9;

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

                then

                 A104: m1 < (j - 1) by A103, XXREAL_0: 2;

                then m1 < j by XREAL_1: 146, XXREAL_0: 2;

                then

                reconsider j1 = (j - 1) as Element of NAT by NAT_1: 20;

                

                 A105: not j1 in ( dom q1) by A34, A104, FINSEQ_1: 1;

                

                 A106: (gg . i) = (j - 1) by A32, A31, A99, A102;

                then (j - 1) in ( dom q) by A32, A30, A59, A99, FUNCT_1:def 3;

                then

                consider a be Nat such that

                 A107: a in ( dom q2) and

                 A108: j1 = (( len q1) + a) by A105, FINSEQ_1: 25;

                

                 A109: ( len <*d*>) = 1 by FINSEQ_1: 39;

                

                 A110: (H2 . i) = (p . i) & (H2 . i) = (H1 . (f . i)) by A74, A14, A26, A32, A99, FUNCT_1: 47;

                

                 A111: H1 = (q1 ^ ( <*d*> ^ q2)) by A97, FINSEQ_1: 32;

                j in ( dom H1) by A7, A11, A8, A26, A32, A99, FUNCT_1:def 3;

                then

                consider b be Nat such that

                 A112: b in ( dom ( <*d*> ^ q2)) and

                 A113: j = (( len q1) + b) by A102, A111, FINSEQ_1: 25;

                

                 A114: (H1 . j) = (( <*d*> ^ q2) . b) by A111, A112, A113, FINSEQ_1:def 7;

                

                 A115: b = (1 + a) by A108, A113;

                (q . (j - 1)) = (q2 . a) by A107, A108, FINSEQ_1:def 7;

                hence (p . i) = (q . (gg . i)) by A106, A110, A107, A114, A115, A109, FINSEQ_1:def 7;

              end;

            end;

            hence (p . i) = (q . (gg . i));

          end;

          now

            per cases ;

              suppose

               A116: ( len p) <> 0 ;

              

               A117: H2 = (p ^ <*d*>) by A5, A6, FINSEQ_3: 55;

              (g "**" p) = (g "**" q) by A4, A17, A16, A58, A56, A98, A116, NAT_1: 14;

              then

               A118: (g "**" H2) = (g . ((g "**" q),d)) by A116, A117, Th4, NAT_1: 14;

              now

                per cases ;

                  suppose

                   A119: ( len q1) <> 0 & ( len q2) <> 0 ;

                  ( len ( <*d*> ^ q2)) = (( len <*d*>) + ( len q2)) & ( len <*d*>) = 1 by FINSEQ_1: 22, FINSEQ_1: 40;

                  then

                   A120: ( len ( <*d*> ^ q2)) >= 1 by NAT_1: 12;

                  

                   A121: ( len q1) >= 1 by A119, NAT_1: 14;

                  ( len q2) >= 1 by A119, NAT_1: 14;

                  

                  then (g "**" H2) = (g . ((g . ((g "**" q1),(g "**" q2))),d)) by A1, A118, A121, Th5

                  .= (g . ((g "**" q1),(g . ((g "**" q2),d)))) by A1, BINOP_1:def 3

                  .= (g . ((g "**" q1),(g . (d,(g "**" q2))))) by A2, BINOP_1:def 2

                  .= (g . ((g "**" q1),(g "**" ( <*d*> ^ q2)))) by A1, A119, Th6, NAT_1: 14

                  .= (g "**" (q1 ^ ( <*d*> ^ q2))) by A1, A121, A120, Th5

                  .= (g "**" H1) by A97, FINSEQ_1: 32;

                  hence thesis;

                end;

                  suppose ( len q1) = 0 & ( len q2) <> 0 ;

                  then

                   A122: q1 = {} ;

                  

                  then

                   A123: H1 = ( <*d*> ^ q2) by A97, FINSEQ_1: 34

                  .= ( <*d*> ^ q) by A122, FINSEQ_1: 34;

                  (g "**" H2) = (g . (d,(g "**" q))) by A2, A118, BINOP_1:def 2

                  .= (g "**" ( <*d*> ^ q)) by A1, A17, A16, A58, A56, A116, Th6, NAT_1: 14;

                  hence thesis by A123;

                end;

                  suppose ( len q1) <> 0 & ( len q2) = 0 ;

                  then

                   A124: q2 = {} ;

                  

                  then H1 = (q1 ^ <*d*>) by A97, FINSEQ_1: 34

                  .= (q ^ <*d*>) by A124, FINSEQ_1: 34;

                  hence thesis by A17, A16, A58, A56, A116, A118, Th4, NAT_1: 14;

                end;

                  suppose ( len q1) = 0 & ( len q2) = 0 ;

                  then ( len q) = ( 0 + 0 ) by FINSEQ_1: 22;

                  hence thesis by A6, A17, A16, A56, A116, FINSEQ_1: 17;

                end;

              end;

              hence thesis;

            end;

              suppose

               A125: ( len p) = 0 ;

              then ( dom H1) = {1} by A5, A58, FINSEQ_1: 2, FINSEQ_1:def 3;

              then

               A126: ( dom f) = {1} & ( rng f) = {1} by FUNCT_2:def 1, FUNCT_2:def 3;

              1 in {1} by TARSKI:def 1;

              then (f . 1) in {1} by A126, FUNCT_1:def 3;

              then (H1 . 1) = (H2 . 1) by A75, A58, A125, TARSKI:def 1;

              then H1 = <*d*> by A5, A58, A125, FINSEQ_1: 40;

              hence thesis by A5, A6, A58, A125, FINSEQ_1: 40;

            end;

          end;

          hence thesis;

        end;

      end;

      let f be Permutation of ( dom F);

      

       A127: P[ 0 ];

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

      hence thesis;

    end;

    

     Lm8: g is having_a_unity & ( len F) = 0 & G = (F * P) implies (g "**" F) = (g "**" G)

    proof

      assume that

       A1: g is having_a_unity and

       A2: ( len F) = 0 ;

      assume

       A3: G = (F * P);

      F = {} by A2;

      then G = {} by A3, RELAT_1: 39;

      then

       A4: ( len G) = 0 ;

      

      thus (g "**" F) = ( the_unity_wrt g) by A1, A2, Def1

      .= (g "**" G) by A1, A4, Def1;

    end;

    theorem :: FINSOP_1:7

    

     Th7: g is commutative associative & (g is having_a_unity or ( len F) >= 1) & G = (F * P) implies (g "**" F) = (g "**" G)

    proof

      assume that

       A1: g is commutative associative and

       A2: g is having_a_unity or ( len F) >= 1;

      assume

       A3: G = (F * P);

      now

        per cases ;

          suppose ( len F) = 0 ;

          hence thesis by A2, A3, Lm8;

        end;

          suppose

           A4: ( len F) <> 0 ;

          ( len F) = ( len G) & for i st i in ( dom G) holds (G . i) = (F . (P . i)) by A3, FINSEQ_2: 44, FUNCT_1: 12;

          hence thesis by A1, A4, Lm7, NAT_1: 14;

        end;

      end;

      hence thesis;

    end;

    

     Lm9: g is associative commutative & F is one-to-one & G is one-to-one & ( rng F) = ( rng G) & ( len F) >= 1 implies (g "**" F) = (g "**" G)

    proof

      assume that

       A1: g is associative commutative and

       A2: F is one-to-one and

       A3: G is one-to-one and

       A4: ( rng F) = ( rng G) and

       A5: ( len F) >= 1;

      

       A6: ( len F) = ( len G) by A2, A3, A4, FINSEQ_1: 48;

      set P = ((F " ) * G);

      

       A7: ( dom (F " )) = ( rng F) by A2, FUNCT_1: 33;

      

      then

       A8: ( dom P) = ( dom G) by A4, RELAT_1: 27

      .= ( Seg ( len F)) by A6, FINSEQ_1:def 3

      .= ( dom F) by FINSEQ_1:def 3;

      ( rng (F " )) = ( dom F) by A2, FUNCT_1: 33;

      then

       A9: ( rng P) c= ( dom F) by RELAT_1: 26;

      ( dom F) = ( Seg ( len F)) by FINSEQ_1:def 3;

      then

      reconsider P as Function of ( dom F), ( dom F) by A5, A8, A9, FUNCT_2:def 1, RELSET_1: 4;

      ( rng P) = ( rng (F " )) by A4, A7, RELAT_1: 28

      .= ( dom F) by A2, FUNCT_1: 33;

      then

      reconsider P as Permutation of ( dom F) by A2, A3, FUNCT_2: 57;

      (F * P) = ((F * (F " )) * G) by RELAT_1: 36

      .= (( id ( rng G)) * G) by A2, A4, FUNCT_1: 39

      .= G by RELAT_1: 54;

      hence thesis by A1, A5, Th7;

    end;

    

     Lm10: ( len F) = 0 & g is having_a_unity & F is one-to-one & G is one-to-one & ( rng F) = ( rng G) implies (g "**" F) = (g "**" G)

    proof

      assume that

       A1: ( len F) = 0 & g is having_a_unity and

       A2: F is one-to-one & G is one-to-one & ( rng F) = ( rng G);

      ( len G) = ( len F) & (g "**" F) = ( the_unity_wrt g) by A1, A2, Def1, FINSEQ_1: 48;

      hence thesis by A1, Def1;

    end;

    theorem :: FINSOP_1:8

    (g is having_a_unity or ( len F) >= 1) & g is associative commutative & F is one-to-one & G is one-to-one & ( rng F) = ( rng G) implies (g "**" F) = (g "**" G)

    proof

      ( len F) >= 1 or ( len F) = 0 by NAT_1: 14;

      hence thesis by Lm9, Lm10;

    end;

    

     Lm11: ( len F) = 1 implies (g "**" F) = (F . 1)

    proof

      assume

       A1: ( len F) = 1;

      

      then F = <*(F . 1)*> by FINSEQ_1: 40

      .= <*(F /. 1)*> by A1, FINSEQ_4: 15;

      

      hence (g "**" F) = (F /. 1) by Lm4

      .= (F . 1) by A1, FINSEQ_4: 15;

    end;

    

     Lm12: g is associative & g is commutative & ( len F) >= 1 & ( len F) = ( len G) & ( len F) = ( len H) & (for k be Nat st k in ( dom F) holds (H . k) = (g . ((F . k),(G . k)))) implies (g "**" H) = (g . ((g "**" F),(g "**" G)))

    proof

      assume that

       A1: g is associative and

       A2: g is commutative;

      defpred P[ Nat] means for F, G, H st ( len F) >= 1 & ( len F) = $1 & ( len F) = ( len G) & ( len F) = ( len H) & (for n be Nat st n in ( dom F) holds (H . n) = (g . ((F . n),(G . n)))) holds (g "**" H) = (g . ((g "**" F),(g "**" G)));

       A3:

      now

        let k be Nat;

        assume

         A4: P[k];

        thus P[(k + 1)]

        proof

          let F, G, H;

          assume that ( len F) >= 1 and

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

           A6: ( len F) = ( len G) and

           A7: ( len F) = ( len H) and

           A8: for k be Nat st k in ( dom F) holds (H . k) = (g . ((F . k),(G . k)));

          reconsider f = (F | ( Seg k)), gg = (G | ( Seg k)), h = (H | ( Seg k)) as FinSequence of D by FINSEQ_1: 18;

          

           A9: ( len h) = k by A5, A7, FINSEQ_3: 53;

          

           A10: ( len f) = k by A5, FINSEQ_3: 53;

          

           A11: ( len gg) = k by A5, A6, FINSEQ_3: 53;

           A12:

          now

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

            then ( Seg ( len f)) c= ( Seg ( len F)) by A5, A10, FINSEQ_1: 5;

            then ( Seg ( len f)) c= ( dom F) by FINSEQ_1:def 3;

            then

             A13: ( dom f) c= ( dom F) by FINSEQ_1:def 3;

            let i be Nat;

            assume

             A14: i in ( dom f);

            then i in ( Seg ( len gg)) by A10, A11, FINSEQ_1:def 3;

            then i in ( dom gg) by FINSEQ_1:def 3;

            then

             A15: (G . i) = (gg . i) by FUNCT_1: 47;

            i in ( Seg ( len h)) by A10, A9, A14, FINSEQ_1:def 3;

            then i in ( dom h) by FINSEQ_1:def 3;

            then

             A16: (H . i) = (h . i) by FUNCT_1: 47;

            (F . i) = (f . i) by A14, FUNCT_1: 47;

            hence (h . i) = (g . ((f . i),(gg . i))) by A8, A14, A15, A16, A13;

          end;

          now

            per cases by NAT_1: 14;

              suppose

               A17: ( len f) >= 1;

              

               A18: ( rng H) c= D by FINSEQ_1:def 4;

              

               A19: ( rng F) c= D & ( rng G) c= D by FINSEQ_1:def 4;

              

               A20: (k + 1) in ( Seg (k + 1)) by FINSEQ_1: 4;

              then (k + 1) in ( dom G) by A5, A6, FINSEQ_1:def 3;

              then

               A21: (G . (k + 1)) in ( rng G) by FUNCT_1:def 3;

              (k + 1) in ( dom H) by A5, A7, A20, FINSEQ_1:def 3;

              then

               A22: (H . (k + 1)) in ( rng H) by FUNCT_1:def 3;

              

               A23: (k + 1) in ( dom F) by A5, A20, FINSEQ_1:def 3;

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

              then

              reconsider d = (F . (k + 1)), d1 = (G . (k + 1)), d2 = (H . (k + 1)) as Element of D by A21, A22, A19, A18;

              

               A24: d2 = (g . ((F . (k + 1)),(G . (k + 1)))) by A8, A23;

              F = (f ^ <*d*>) by A5, FINSEQ_3: 55;

              then

               A25: (g "**" F) = (g . ((g "**" f),d)) by A17, Th4;

              G = (gg ^ <*d1*>) by A5, A6, FINSEQ_3: 55;

              then

               A26: (g "**" G) = (g . ((g "**" gg),d1)) by A10, A11, A17, Th4;

              

               A27: H = (h ^ <*d2*>) by A5, A7, FINSEQ_3: 55;

              (g "**" h) = (g . ((g "**" f),(g "**" gg))) by A4, A10, A11, A9, A12, A17;

              

              hence (g "**" H) = (g . ((g . ((g "**" f),(g "**" gg))),(g . (d,d1)))) by A10, A9, A17, A27, A24, Th4

              .= (g . ((g . ((g . ((g "**" f),(g "**" gg))),d)),d1)) by A1, BINOP_1:def 3

              .= (g . ((g . ((g "**" f),(g . ((g "**" gg),d)))),d1)) by A1, BINOP_1:def 3

              .= (g . ((g . ((g "**" f),(g . (d,(g "**" gg))))),d1)) by A2, BINOP_1:def 2

              .= (g . ((g . ((g "**" F),(g "**" gg))),d1)) by A1, A25, BINOP_1:def 3

              .= (g . ((g "**" F),(g "**" G))) by A1, A26, BINOP_1:def 3;

            end;

              suppose

               A28: ( len f) = 0 ;

              then

               A29: (g "**" G) = (G . 1) & 1 in ( dom F) by A5, A6, A10, Lm11, FINSEQ_3: 25;

              (g "**" H) = (H . 1) & (g "**" F) = (F . 1) by A5, A7, A10, A28, Lm11;

              hence thesis by A8, A29;

            end;

          end;

          hence thesis;

        end;

      end;

      assume

       A30: ( len F) >= 1 & ( len F) = ( len G) & ( len F) = ( len H);

      

       A31: P[ 0 ];

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

      hence thesis by A30;

    end;

    

     Lm13: g is having_a_unity & ( len F) = 0 & ( len F) = ( len G) & ( len F) = ( len H) implies (g "**" F) = (g . ((g "**" G),(g "**" H)))

    proof

      assume that

       A1: g is having_a_unity and

       A2: ( len F) = 0 and

       A3: ( len F) = ( len G) and

       A4: ( len F) = ( len H);

      

      thus (g "**" F) = ( the_unity_wrt g) by A1, A2, Def1

      .= (g . (( the_unity_wrt g),( the_unity_wrt g))) by A1, SETWISEO: 15

      .= (g . ((g "**" G),( the_unity_wrt g))) by A1, A2, A3, Def1

      .= (g . ((g "**" G),(g "**" H))) by A1, A2, A4, Def1;

    end;

    theorem :: FINSOP_1:9

    g is associative commutative & (g is having_a_unity or ( len F) >= 1) & ( len F) = ( len G) & ( len F) = ( len H) & (for k be Nat st k in ( dom F) holds (F . k) = (g . ((G . k),(H . k)))) implies (g "**" F) = (g . ((g "**" G),(g "**" H)))

    proof

      

       A1: ( dom F) = ( Seg ( len F)) & ( dom G) = ( Seg ( len G)) by FINSEQ_1:def 3;

      

       A2: ( len F) = 0 or ( len F) >= 1 by NAT_1: 14;

      assume g is associative commutative & (g is having_a_unity or ( len F) >= 1);

      hence thesis by A1, A2, Lm12, Lm13;

    end;

    theorem :: FINSOP_1:10

    g is having_a_unity implies (g "**" ( <*> D)) = ( the_unity_wrt g) by Lm3;

    theorem :: FINSOP_1:11

    (g "**" <*d*>) = d by Lm4;

    theorem :: FINSOP_1:12

    

     Th12: (g "**" <*d1, d2*>) = (g . (d1,d2))

    proof

      

       A1: ( len <*d1*>) = 1 by FINSEQ_1: 39;

      

      thus (g "**" <*d1, d2*>) = (g "**" ( <*d1*> ^ <*d2*>)) by FINSEQ_1:def 9

      .= (g . ((g "**" <*d1*>),d2)) by A1, Th4

      .= (g . (d1,d2)) by Lm4;

    end;

    theorem :: FINSOP_1:13

    g is commutative implies (g "**" <*d1, d2*>) = (g "**" <*d2, d1*>)

    proof

      assume

       A1: g is commutative;

      

      thus (g "**" <*d1, d2*>) = (g . (d1,d2)) by Th12

      .= (g . (d2,d1)) by A1, BINOP_1:def 2

      .= (g "**" <*d2, d1*>) by Th12;

    end;

    theorem :: FINSOP_1:14

    

     Th14: (g "**" <*d1, d2, d3*>) = (g . ((g . (d1,d2)),d3))

    proof

      

       A1: ( len <*d1, d2*>) = 2 by FINSEQ_1: 44;

      

      thus (g "**" <*d1, d2, d3*>) = (g "**" ( <*d1, d2*> ^ <*d3*>)) by FINSEQ_1: 43

      .= (g . ((g "**" <*d1, d2*>),d3)) by A1, Th4

      .= (g . ((g . (d1,d2)),d3)) by Th12;

    end;

    theorem :: FINSOP_1:15

    g is commutative implies (g "**" <*d1, d2, d3*>) = (g "**" <*d2, d1, d3*>)

    proof

      assume

       A1: g is commutative;

      

      thus (g "**" <*d1, d2, d3*>) = (g . ((g . (d1,d2)),d3)) by Th14

      .= (g . ((g . (d2,d1)),d3)) by A1, BINOP_1:def 2

      .= (g "**" <*d2, d1, d3*>) by Th14;

    end;

    theorem :: FINSOP_1:16

    

     Th16: (g "**" (1 |-> d)) = d

    proof

      

      thus (g "**" (1 |-> d)) = (g "**" <*d*>) by FINSEQ_2: 59

      .= d by Lm4;

    end;

    theorem :: FINSOP_1:17

    (g "**" (2 |-> d)) = (g . (d,d))

    proof

      

      thus (g "**" (2 |-> d)) = (g "**" <*d, d*>) by FINSEQ_2: 61

      .= (g . (d,d)) by Th12;

    end;

    theorem :: FINSOP_1:18

    

     Th18: g is associative & (g is having_a_unity or k <> 0 & l <> 0 ) implies (g "**" ((k + l) |-> d)) = (g . ((g "**" (k |-> d)),(g "**" (l |-> d))))

    proof

      

       A1: k <> 0 & l <> 0 implies ( len (k |-> d)) >= 1 & ( len (l |-> d)) >= 1 by NAT_1: 14;

      ((k + l) |-> d) = ((k |-> d) ^ (l |-> d)) by FINSEQ_2: 123;

      hence thesis by A1, Th5;

    end;

    theorem :: FINSOP_1:19

    g is associative & (g is having_a_unity or k <> 0 & l <> 0 ) implies (g "**" ((k * l) |-> d)) = (g "**" (l |-> (g "**" (k |-> d))))

    proof

      defpred P[ Nat] means for g, k, d st g is associative & (g is having_a_unity or k <> 0 & $1 <> 0 ) holds (g "**" ((k * $1) |-> d)) = (g "**" ($1 |-> (g "**" (k |-> d))));

      

       A1: for l st P[l] holds P[(l + 1)]

      proof

        let l;

        assume

         A2: P[l];

        let g, k, d;

        assume that

         A3: g is associative and

         A4: g is having_a_unity or k <> 0 & (l + 1) <> 0 ;

        now

          per cases ;

            suppose l = 0 ;

            hence thesis by Th16;

          end;

            suppose

             A5: l <> 0 ;

            then

             A6: k <> 0 implies (k * l) <> 0 by XCMPLX_1: 6;

            (g "**" ((k * (l + 1)) |-> d)) = (g "**" (((k * l) + (k * 1)) |-> d))

            .= (g . ((g "**" ((k * l) |-> d)),(g "**" (k |-> d)))) by A3, A4, A6, Th18

            .= (g . ((g "**" (l |-> (g "**" (k |-> d)))),(g "**" (k |-> d)))) by A2, A3, A4, A5

            .= (g . ((g "**" (l |-> (g "**" (k |-> d)))),(g "**" (1 |-> (g "**" (k |-> d)))))) by Th16;

            hence thesis by A3, A5, Th18;

          end;

        end;

        hence thesis;

      end;

      

       A7: P[ 0 ];

      for l holds P[l] from NAT_1:sch 2( A7, A1);

      hence thesis;

    end;

    theorem :: FINSOP_1:20

    ( len F) = 1 implies (g "**" F) = (F . 1) by Lm11;

    theorem :: FINSOP_1:21

    ( len F) = 2 implies (g "**" F) = (g . ((F . 1),(F . 2)))

    proof

      assume

       A1: ( len F) = 2;

      

      then F = <*(F . 1), (F . 2)*> by FINSEQ_1: 44

      .= <*(F /. 1), (F . 2)*> by A1, FINSEQ_4: 15

      .= <*(F /. 1), (F /. 2)*> by A1, FINSEQ_4: 15;

      

      hence (g "**" F) = (g . ((F /. 1),(F /. 2))) by Th12

      .= (g . ((F . 1),(F /. 2))) by A1, FINSEQ_4: 15

      .= (g . ((F . 1),(F . 2))) by A1, FINSEQ_4: 15;

    end;