The Mizar article:

Semigroup Operations on Finite Subsets

by
Czeslaw Bylinski

Received May 4, 1990

Copyright (c) 1990 Association of Mizar Users

MML identifier: SETWOP_2
[ MML identifier index ]


environ

 vocabulary FINSUB_1, BINOP_1, FUNCT_1, FINSEQ_1, FINSEQ_2, SETWISEO, BOOLE,
      RELAT_1, TARSKI, FINSEQOP, FUNCOP_1, SUBSET_1, FUNCT_4, FINSOP_1;
 notation TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XREAL_0, NAT_1, RELAT_1,
      RELSET_1, FUNCT_1, FINSEQ_1, FINSUB_1, PARTFUN1, FUNCT_2, BINOP_1,
      FUNCOP_1, SETWISEO, FINSEQ_2, FINSEQOP, FINSOP_1;
 constructors NAT_1, BINOP_1, WELLORD2, SETWISEO, FINSEQOP, FINSOP_1, XREAL_0,
      MEMBERED, PARTFUN1, XBOOLE_0;
 clusters SUBSET_1, FUNCT_1, RELSET_1, FINSEQ_2, FINSUB_1, FINSEQ_1, ARYTM_3,
      MEMBERED, ZFMISC_1, FUNCT_2, XBOOLE_0, ORDINAL2;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
 definitions BINOP_1, XBOOLE_0;
 theorems TARSKI, ENUMSET1, ZFMISC_1, REAL_1, NAT_1, FUNCT_1, FUNCT_2,
      FUNCOP_1, FINSEQ_1, FINSUB_1, BINOP_1, SETWISEO, FINSEQ_2, RLVECT_1,
      WELLORD2, CARD_1, FINSEQOP, RELAT_1, FUNCT_4, FINSOP_1, XBOOLE_0,
      XBOOLE_1, XCMPLX_1;
 schemes NAT_1, SETWISEO, FINSEQ_2;

begin

 reserve x,y for set;
 reserve C,C',D,E for non empty set;
 reserve c,c',c1,c2,c3 for Element of C;
 reserve B,B',B1,B2 for Element of Fin C;
 reserve A for Element of Fin C';
 reserve d,d1,d2,d3,d4,e for Element of D;
 reserve F,G for BinOp of D;
 reserve u for UnOp of D;
 reserve f,f' for Function of C,D;
 reserve g for Function of C',D;
 reserve H for BinOp of E;
 reserve h for Function of D,E;
 reserve i,j for Nat;
 reserve s for Function;
 reserve p,q for FinSequence of D;
 reserve T1,T2 for Element of i-tuples_on D;

 Lm1:
   Seg i is Element of Fin NAT by FINSUB_1:def 5;

Lm2:
  now let i;
   assume i+1 in Seg i; then i+1 <= i & i < i+1 by FINSEQ_1:3,REAL_1:69;
   hence contradiction;
  end;
canceled 2;

theorem Th3:
  F is commutative associative & c1 <> c2
    implies F $$ ({c1,c2},f) = F.(f.c1, f.c2)
 proof assume that
A1:  F is commutative associative and
A2:  c1 <> c2;
   consider g being Function of Fin C, D such that
A3: F $$ ({c1,c2},f) = g.{c1,c2} and
      for e st e is_a_unity_wrt F holds g.{} = e and
A4: for c holds g.{c} = f.c and
A5: for B st B c= { c1,c2 } & B <> {}
      for c st c in { c1,c2 } \ B holds g.(B \/ {c}) = F.(g.B,f.c)
     by A1,SETWISEO:def 3;
      c1 in {c1} & not c2 in {c1} by A2,TARSKI:def 1;
    then {c1,c2} \ {c1} = {c2} by ZFMISC_1:70;
then A6: {c1} c= {c1,c2} & {c1} <> {} & c2 in {c1,c2} & c2 in {c1,c2} \ {c1}
      by TARSKI:def 1,def 2,ZFMISC_1:12;
  thus F $$ ({c1,c2},f) = g.({c1} \/ {c2}) by A3,ENUMSET1:41
                       .= F.(g.{c1}, f.c2) by A5,A6
                       .= F.(f.c1, f.c2) by A4;
 end;

theorem Th4:
  F is commutative associative & (B <> {} or F has_a_unity) & not c in B
   implies F $$(B \/ {c}, f) = F.(F $$(B,f),f.c)
 proof assume that
A1:  F is commutative associative and
A2:  B <> {} or F has_a_unity and
A3:   not c in B;
  per cases;
   suppose
A4:   B = {};
    then B = {}.C;
    then F $$(B,f) = the_unity_wrt F by A1,A2,SETWISEO:40;
    hence F.(F $$(B,f),f.c) = f.c by A2,A4,SETWISEO:23
                           .= F $$(B \/ {c}, f) by A1,A4,SETWISEO:26;
   suppose
A5:   B <> {};
     consider g being Function of Fin C, D such that
A6:  F $$ (B \/ {c},f) = g.(B \/ {c}) and
       for e st e is_a_unity_wrt F holds g.{} = e and
A7:  for c' holds g.{c'} = f.c' and
A8:  for B' st B' c= B \/ {c} & B' <> {}
       for c' st c' in (B \/ {c}) \ B' holds g.(B' \/ {c'}) = F.(g.B',f.c')
     by A1,SETWISEO:def 3;
    consider g' being Function of Fin C, D such that
A9:  F $$ (B,f) = g'.B and
       for e st e is_a_unity_wrt F holds g'.{} = e and
A10:  for c' holds g'.{c'} = f.c' and
A11:  for B' st B' c= B & B' <> {}
       for c' st c' in B \ B' holds g'.(B' \/ {c'}) = F.(g'.B',f.c')
      by A1,A2,SETWISEO:def 3;
      defpred X[set] means $1 <> {} & $1 c= B implies g.($1) = g'.($1);
A12: X[{}.C];
A13: for B' being Element of Fin C, b being Element of C
      holds X[B'] & not b in B' implies X[B' \/ {b}]
 proof let B', c' such that
A14:   B' <> {} & B' c= B implies g.B' = g'.B' and
A15:   not c' in B' and B' \/ {c'} <> {} and
A16:   B' \/ {c'} c= B;
A17:   c' in B by A16,SETWISEO:8;
then A18:   B' c= B & c' in B \ B' by A15,A16,XBOOLE_0:def 4,XBOOLE_1:11;
        B c= B \/ {c} by XBOOLE_1:7;
then A19:   B' c= B \/ {c} by A18,XBOOLE_1:1;
        c' in (B \/ {c}) by A17,XBOOLE_0:def 2;
then A20:   c' in (B \/ {c}) \ B' by A15,XBOOLE_0:def 4;
      per cases;
       suppose B' = {};
        then g.(B' \/ {c'}) = f.c' & g'.(B' \/ {c'}) = f.c' by A7,A10;
        hence g.(B' \/ {c'}) = g'.(B' \/ {c'});
       suppose
A21:      B' <> {};
       hence g.(B' \/ {c'}) = F.(g'.B', f.c') by A8,A14,A16,A19,A20,XBOOLE_1:11
                        .= g'.(B' \/ {c'}) by A11,A18,A21;
    end;
A22:  for B' holds X[B'] from FinSubInd1(A12,A13);
     c in B \/ {c} by SETWISEO:6;
   then B c= B \/ {c} & c in (B \/ {c}) \ B by A3,XBOOLE_0:def 4,XBOOLE_1:7;
   hence F $$(B \/ {c}, f) = F.(g.B, f.c) by A5,A6,A8
                        .= F.(F $$(B,f),f.c) by A5,A9,A22;
 end;

theorem
    F is commutative associative & c1 <> c2 & c1 <> c3 & c2 <> c3
   implies F $$ ({c1,c2,c3},f) = F.(F.(f.c1, f.c2),f.c3)
 proof assume that
A1:  F is commutative associative and
A2:  c1 <> c2;
  assume c1 <> c3 & c2 <> c3;
then A3:  not c3 in {c1,c2} & {c1,c2} <> {} by TARSKI:def 2;
  thus F $$ ({c1,c2,c3},f) = F $$ ({c1,c2} \/ {c3},f) by ENUMSET1:43
                          .= F.(F $$ ({c1,c2},f),f.c3) by A1,A3,Th4
                          .= F.(F.(f.c1, f.c2),f.c3) by A1,A2,Th3;
 end;

theorem
    F is commutative associative &
   (B1 <> {} & B2 <> {} or F has_a_unity) & B1 misses B2
    implies F $$(B1 \/ B2, f) = F.(F $$(B1,f),F $$(B2,f))
 proof assume that
A1:  F is commutative associative and
A2:  B1 <> {} & B2 <> {} or F has_a_unity and
A3:  B1 /\ B2 = {};
    now per cases;
   suppose
A4:   B1 = {} or B2 = {};
      now per cases by A4;
     suppose
A5:      B1 = {};
      hence F $$(B1 \/ B2, f)
           = F.(the_unity_wrt F,F $$(B2,f)) by A2,SETWISEO:23
          .= F.(F $$({}.C,f),F $$(B2,f)) by A1,A2,A4,SETWISEO:40
          .= F.(F $$(B1,f),F $$(B2,f)) by A5;
     suppose
A6:     B2 = {};
      hence F $$(B1 \/ B2, f)
           = F.(F $$(B1,f),the_unity_wrt F) by A2,SETWISEO:23
          .= F.(F $$(B1,f),F $$({}.C,f)) by A1,A2,A4,SETWISEO:40
          .= F.(F $$(B1,f),F $$(B2,f)) by A6;
    end;
    hence F $$(B1 \/ B2, f) = F.(F $$(B1,f),F $$(B2,f));
   suppose
A7:   B1 <> {} & B2 <> {};
     defpred X[Element of Fin C] means $1 <> {} & B1 /\ $1 = {} implies
        F $$(B1 \/ $1,f) = F.(F $$(B1,f),F $$($1,f));
A8:  X[{}.C];
A9: for B' being Element of Fin C, b being Element of C
      holds X[B'] & not b in B' implies X[B' \/ {b}]
   proof let B,c such that
A10:     B <> {} & B1 /\ B = {} implies
            F $$(B1 \/ B,f) = F.(F $$ (B1,f),F $$(B,f)) and
A11:     not c in B and B \/ {c} <> {};
A12:    B <> {} & B1 misses B implies
            F $$(B1 \/ B,f) = F.(F $$ (B1,f),F $$(B,f)) by A10,XBOOLE_0:def 7;
      assume
A13:  B1 /\ (B \/ {c}) = {};
then A14:    B1 misses (B \/ {c}) by XBOOLE_0:def 7;
        c in B \/ {c} & not c in B1 /\ (B \/ {c}) by A13,SETWISEO:6;
then A15:     not c in B1 by XBOOLE_0:def 3;
        now per cases;
       suppose
A16:      B = {};
        hence F $$ (B1 \/ (B \/ {c}),f) = F.(F $$ (B1,f), f.c) by A1,A7,A15,Th4
                .= F.(F $$ (B1,f),F $$(B \/ {c},f)) by A1,A16,SETWISEO:26;
       suppose
A17:      B <> {};
then A18:      B1 \/ B <> {} & not c in B1 \/ B by A11,A15,XBOOLE_0:def 2,
XBOOLE_1:15;
A19:       B c= B \/ {c} & (B \/ {c}) /\ B1 = {} & B1 /\ B = B /\ B1
           by A13,XBOOLE_1:7;
        thus F $$ (B1 \/ (B \/ {c}),f) = F $$ (B1 \/ B \/ {c},f) by XBOOLE_1:4
            .= F.(F.(F $$ (B1,f),F $$(B,f)), f.c)
              by A1,A12,A14,A17,A18,A19,Th4,XBOOLE_1:63
                   .= F.(F $$ (B1,f),F.(F $$(B,f), f.c)) by A1,BINOP_1:def 3
                   .= F.(F $$(B1,f),F $$(B \/ {c},f)) by A1,A11,A17,Th4;
      end;
     hence F $$ (B1 \/ (B \/ {c}),f) = F.(F $$ (B1,f),F $$ (B \/ {c},f));
    end;
      for B2 holds X[B2] from FinSubInd1(A8,A9);
    hence F $$(B1 \/ B2, f) = F.(F $$(B1,f),F $$(B2,f)) by A3,A7;
  end;
  hence thesis;
 end;

theorem Th7:
   F is commutative associative & (A <> {} or F has_a_unity) &
    (ex s st dom s = A & rng s = B & s is one-to-one & g|A = f*s)
     implies F $$(A,g) = F $$(B,f)
 proof assume
A1:   F is commutative associative;
  defpred X[Element of Fin C'] means $1 <> {} or F has_a_unity implies
    for B st ex s st dom s = $1 & rng s = B & s is one-to-one & g|$1 = f*s
     holds F $$($1,g) = F $$(B,f);
A2: X[{}.C']
   proof assume
A3:    {}.C' <> {} or F has_a_unity;
      let B;
      given s such that
A4:    dom s = {}.C' & rng s = B & s is one-to-one and g|({}.C') = f*s;
        B,{} are_equipotent & {} = {}.C by A4,WELLORD2:def 4;
      then B = {}.C & F $$({}.C',g) = the_unity_wrt F
         by A1,A3,CARD_1:46,SETWISEO:40;
      hence F $$({}.C',g) = F $$(B,f) by A1,A3,SETWISEO:40;
    end;
A5: for B' being Element of Fin C', b being Element of C'
      holds X[B'] & not b in B' implies X[B' \/ {b}]
   proof let A' be Element of Fin C',a be Element of C' such that
A6:   A' <> {} or F has_a_unity implies
       for B st ex s st dom s = A' & rng s = B & s is one-to-one & g|A' = f*s
        holds F $$(A',g) = F $$(B,f) and
A7:   not a in A';
     set A = A' \/ {a};
     assume A' \/ {a} <> {} or F has_a_unity;
     let B;
     given s such that
A8:     dom s = A & rng s = B & s is one-to-one and
A9:     g|A = f*s;
A10:   a in A by SETWISEO:6;
then A11:    s.a in B by A8,FUNCT_1:def 5;
       B c= C by FINSUB_1:def 5;
     then reconsider c = s.a as Element of C by A11;
       a in C';
     then a in dom g by FUNCT_2:def 1;
     then a in dom g /\ A by A10,XBOOLE_0:def 3;
     then a in dom(f*s) & g.a = (f*s).a by A9,FUNCT_1:71,RELAT_1:90;
then A12:    g.a = f.c by FUNCT_1:22;
     set B' = B \ {c};
     set s' = s|A';
A13:   now let y;
       thus y in rng s' implies y in B'
        proof assume y in rng s';
         then consider x such that
A14:       x in dom s' and
A15:       y = s'.x by FUNCT_1:def 5;
A16:         x in dom s /\ A' by A14,RELAT_1:90;
then A17:       x in dom s & x in A' by XBOOLE_0:def 3;
           x in dom s & x <> a by A7,A16,XBOOLE_0:def 3;
         then s'.x = s.x & s.x <> c by A8,A10,A14,FUNCT_1:70,def 8;
         then y in B & not y in {c} by A8,A15,A17,FUNCT_1:def 5,TARSKI:def 1;
         hence y in B' by XBOOLE_0:def 4;
        end;
       assume y in B';
then A18:       y in B & not y in {c} by XBOOLE_0:def 4;
       then consider x such that
A19:       x in dom s and
A20:       y = s.x by A8,FUNCT_1:def 5;
         x <> a & (x in A' or x in
 {a}) by A8,A18,A19,A20,TARSKI:def 1,XBOOLE_0:def 2;
       then x in dom s /\ A' by A19,TARSKI:def 1,XBOOLE_0:def 3;
       then x in dom s' & s'.x = s.x by FUNCT_1:71,RELAT_1:90;
       hence y in rng s' by A20,FUNCT_1:def 5;
      end;
       A' c= A by XBOOLE_1:7;
then A21:     s' is one-to-one & dom s' = A' & rng s' = B'
      by A8,A13,FUNCT_1:84,RELAT_1:91,TARSKI:2;
      now let x;
     thus x in dom(g|A') implies x in dom(f*s')
      proof assume x in dom(g|A');
       then x in dom g /\ A' by RELAT_1:90;
       then A22:      x in dom g & x in A' by XBOOLE_0:def 3;
       then x in dom g & x in A by SETWISEO:6;
       then x in dom g /\ A by XBOOLE_0:def 3;
       then x in dom(f*s) by A9,RELAT_1:90;
then A23:      x in dom s & s.x in dom f by FUNCT_1:21;
       then x in dom s /\ A' by A22,XBOOLE_0:def 3;
then A24:       x in dom s' by RELAT_1:90;
       then s'.x = s.x by FUNCT_1:70;
       hence x in dom(f*s') by A23,A24,FUNCT_1:21;
      end;
     assume x in dom(f*s');
     then x in dom s' & s'.x in dom f by FUNCT_1:21;
     then x in dom s /\ A' & s.x in dom f by FUNCT_1:70,RELAT_1:90;
     then x in dom s & x in A' & s.x in dom f by XBOOLE_0:def 3;
     then x in A' & x in dom(g|A) by A9,FUNCT_1:21;
     then x in A' & x in dom g /\ A by RELAT_1:90;
     then x in A' & x in dom g by XBOOLE_0:def 3;
     then x in dom g /\ A' by XBOOLE_0:def 3;
     hence x in dom(g|A') by RELAT_1:90;
    end;
then A25:    dom(g|A') = dom(f*s') by TARSKI:2;
       for x st x in dom(g|A') holds (g|A').x = (f*s').x
      proof let x;
       assume x in dom(g|A');
       then x in dom g /\ A' by RELAT_1:90;
then A26:      x in dom g & x in A' by XBOOLE_0:def 3;
then A27:      x in dom g & x in A by SETWISEO:6;
       then x in dom g /\ A by XBOOLE_0:def 3;
       then x in dom(f*s) by A9,RELAT_1:90;
then A28:      x in dom s & s.x in dom f by FUNCT_1:21;
       then x in dom s /\ A' by A26,XBOOLE_0:def 3;
then A29:       x in dom s' by RELAT_1:90;
then A30:    s'.x = s.x by FUNCT_1:70;
       thus (g|A').x = g.x by A26,FUNCT_1:72
                    .= (f*s).x by A9,A27,FUNCT_1:72
                    .= f.(s.x) by A28,FUNCT_1:23
                    .= (f*s').x by A29,A30,FUNCT_1:23;
      end;
then A31:  g|A' = f*s' by A25,FUNCT_1:9;
       B' \/ {c} = B \/ {c} by XBOOLE_1:39;
then A32:   B = B' \/ {c} & not c in B' by A11,ZFMISC_1:46,64;
       now let y;
      thus y in g.:A' implies y in f.:B'
       proof assume y in g.:A';
        then consider x such that
A33:      x in dom g and
A34:      x in A' and
A35:      y = g.x by FUNCT_1:def 12;
          x in dom g /\ A' by A33,A34,XBOOLE_0:def 3;
        then x in dom(g|A') & y = (f*s').x
           by A31,A34,A35,FUNCT_1:72,RELAT_1:90;
        then s'.x in dom f & y = f.(s'.x) & x in dom s'
          by A25,FUNCT_1:21,22;
        then s'.x in dom f & y = f.(s'.x) & s'.x in B' by A21,FUNCT_1:def 5;
        hence y in f.:B' by FUNCT_1:def 12;
       end;
      assume y in f.:B';
      then consider x such that
        x in dom f and
A36:      x in B' and
A37:      y = f.x by FUNCT_1:def 12;
      set x' = s'".x;
A38:    x' in A' by A21,A36,FUNCT_1:54;
        A' c= C' by FINSUB_1:def 5;
      then x' in C' by A38;
then A39:     x' in dom g by FUNCT_2:def 1;
        s'.x' = x by A21,A36,FUNCT_1:57;
      then y = (f*s').x' by A21,A37,A38,FUNCT_1:23
            .= g.x' by A31,A38,FUNCT_1:72;
      hence y in g.:A' by A38,A39,FUNCT_1:def 12;
     end;
then A40:   f.:B' = g.:A' by TARSKI:2;
       now per cases;
      suppose
A41:      A' = {};
        B' c= C by FINSUB_1:def 5;
      then B' c= dom f & g.:A' = {} by A41,FUNCT_2:def 1,RELAT_1:149;
then A42:      B' = {} by A40,RELAT_1:152;
       thus F $$(A,g) = f.c by A1,A12,A41,SETWISEO:26
                     .= F $$(B,f) by A1,A32,A42,SETWISEO:26;
      suppose
A43:     A' <> {};
         A' c= C' by FINSUB_1:def 5;
       then A' c= dom g by FUNCT_2:def 1;
       then f.:B' <> {} by A40,A43,RELAT_1:152;
then A44:     B' <> {} by RELAT_1:149;
       thus F $$(A,g) = F.(F $$(A',g),g.a) by A1,A7,A43,Th4
                     .= F.(F $$(B',f),f.c) by A6,A12,A21,A31,A43
                     .= F $$(B,f) by A1,A32,A44,Th4;
     end;
     hence F $$(A,g) = F $$(B,f);
    end;
     for A holds X[A] from FinSubInd1(A2,A5);
   hence thesis;
 end;

theorem
     H is commutative associative & (B <> {} or H has_a_unity) &
    f is one-to-one implies H $$(f.:B,h) = H $$(B,h*f)
 proof assume that
A1:  H is commutative associative & (B <> {} or H has_a_unity) and
A2:  f is one-to-one;
   set s = f|B;
     B c= C by FINSUB_1:def 5;
   then B c= dom f by FUNCT_2:def 1;
   then dom s = B & rng s = f.:B & s is one-to-one & (h*f)|B = h*s
     by A2,FUNCT_1:84,RELAT_1:91,112,148;
   hence thesis by A1,Th7;
 end;

theorem
     F is commutative associative & (B <> {} or F has_a_unity) &
    f|B = f'|B implies F $$(B,f) = F $$(B,f')
 proof assume
A1:  F is commutative associative & (B <> {} or F has_a_unity);
  set s = id B;
  assume f|B = f'|B;
  then dom s = B & rng s = B & s is one-to-one & f|B = f'*s
    by FUNCT_1:52,RELAT_1:71,94;
  hence thesis by A1,Th7;
 end;

theorem
     F is commutative associative & F has_a_unity &
      e = the_unity_wrt F & f.:B = {e} implies F$$(B,f) = e
 proof assume that
A1:  F is commutative associative & F has_a_unity and
A2:  e = the_unity_wrt F;
   defpred X[Element of Fin C] means f.:($1) = {e} implies F$$($1,f) = e;
A3:  X[{}.C] by RELAT_1:149;
A4: for B' being Element of Fin C, b being Element of C
      holds X[B'] & not b in B' implies X[B' \/ {b}]
  proof let B',c such that
A5:   f.:(B') = {e} implies F$$(B',f) = e and
A6:   not c in B' and
A7:   f.:(B' \/ {c}) = {e};
        {c} c= C by FINSUB_1:def 5;
      then {c} c= B' \/ {c} & {c} c= dom f & {c} <> {}
         by FUNCT_2:def 1,XBOOLE_1:7;
      then f.:{c} c= {e} & f.:{c} <> {} & c in dom f
         by A7,RELAT_1:152,156,ZFMISC_1:37;
      then f.:{c} = {e} & c in dom f by ZFMISC_1:39;
      then {e} = {f.c} by FUNCT_1:117;
then A8:    f.c = e by ZFMISC_1:6;
       now per cases;
      suppose B' = {};
then A9:     B' = {}.C;
      thus F$$(B' \/ {c},f) = F.(F $$(B',f),f.c) by A1,A6,Th4
                          .= F.(e ,f.c) by A1,A2,A9,SETWISEO:40;
      suppose
A10:     B' <> {};
        B' c= C by FINSUB_1:def 5;
      then B' c= B' \/ {c} & B' c= dom f by FUNCT_2:def 1,XBOOLE_1:7;
      then f.:B' c= {e} & f.:B' <> {} by A7,A10,RELAT_1:152,156;
      hence F$$(B' \/ {c},f) = F.(e ,f.c) by A1,A5,A6,Th4,ZFMISC_1:39;
     end;
     hence F$$(B' \/ {c},f) = e by A1,A2,A8,SETWISEO:23;
    end;
    for B holds X[B] from FinSubInd1(A3,A4);
  hence thesis;
 end;

theorem Th11:
   F is commutative associative &
   F has_a_unity & e = the_unity_wrt F & G.(e,e) = e &
   (for d1,d2,d3,d4 holds F.(G.(d1,d2),G.(d3,d4))= G.(F.(d1,d3),F.(d2,d4)))
     implies G.(F$$(B,f),F$$(B,f')) = F $$(B,G.:(f,f'))
 proof assume that
A1:   F is commutative associative and
A2:   F has_a_unity and
A3:   e = the_unity_wrt F and
A4:   G.(e,e) = e and
A5:   for d1,d2,d3,d4 holds F.(G.(d1,d2),G.(d3,d4))= G.(F.(d1,d3),F.(d2,d4));
      defpred X[Element of Fin C] means
          G.(F$$($1,f),F$$($1,f')) = F $$($1,G.:(f,f'));
      F$$({}.C,f) = e & F$$({}.C,f') = e by A1,A2,A3,SETWISEO:40;
then A6: X[{}.C] by A1,A2,A3,A4,SETWISEO:40;
A7: for B' being Element of Fin C, b being Element of C
      holds X[B'] & not b in B' implies X[B' \/ {b}]
   proof let B,c such that
A8:   G.(F$$(B,f),F$$(B,f')) = F $$(B,G.:(f,f')) and
A9:   not c in B;
     set s = F$$(B,f);
     set s' = F$$(B,f');
       F$$(B \/ {c},f) = F.(s,f.c) & F$$(B \/ {c},f') = F.(s',f'.c)
      by A1,A2,A9,Th4;
    hence G.(F$$(B \/ {c},f),F$$(B \/ {c},f'))
        = F.(G.(s,s'),G.(f.c,f'.c)) by A5
       .= F.(G.(s,s'),G.:(f,f').c) by FUNCOP_1:48
       .= F $$(B \/ {c},G.:(f,f')) by A1,A2,A8,A9,Th4;
    end;
    for B holds X[B] from FinSubInd1(A6,A7);
  hence thesis;
 end;

Lm3: F is commutative associative implies
     for d1,d2,d3,d4 holds F.(F.(d1,d2),F.(d3,d4))= F.(F.(d1,d3),F.(d2,d4))
 proof assume that
A1: F is commutative and
A2: F is associative;
  let d1,d2,d3,d4;
  thus F.(F.(d1,d2),F.(d3,d4)) = F.(d1,F.(d2,F.(d3,d4))) by A2,BINOP_1:def 3
                               .= F.(d1,F.(F.(d2,d3),d4)) by A2,BINOP_1:def 3
                               .= F.(d1,F.(F.(d3,d2),d4)) by A1,BINOP_1:def 2
                               .= F.(d1,F.(d3,F.(d2,d4))) by A2,BINOP_1:def 3
                               .= F.(F.(d1,d3),F.(d2,d4)) by A2,BINOP_1:def 3;
 end;

theorem
     F is commutative associative & F has_a_unity
     implies F.(F$$(B,f),F$$(B,f')) = F $$(B,F.:(f,f'))
 proof assume
A1:  F is commutative & F is associative & F has_a_unity;
   set e = the_unity_wrt F;
     F.(e,e) = e &
    for d1,d2,d3,d4 holds F.(F.(d1,d2),F.(d3,d4))= F.(F.(d1,d3),F.(d2,d4))
     by A1,Lm3,SETWISEO:23;
   hence thesis by A1,Th11;
 end;

theorem
     F is commutative associative & F has_a_unity &
    F has_an_inverseOp & G = F*(id D,the_inverseOp_wrt F)
     implies G.(F$$(B,f),F$$(B,f')) = F $$(B,G.:(f,f'))
 proof assume
A1:   F is commutative associative & F has_a_unity &
      F has_an_inverseOp & G = F*(id D,the_inverseOp_wrt F);
   set e = the_unity_wrt F;
     G.(e,e) = e &
     for d1,d2,d3,d4 holds F.(G.(d1,d2),G.(d3,d4))= G.(F.(d1,d3),F.(d2,d4))
    by A1,FINSEQOP:91,94;
   hence thesis by A1,Th11;
 end;

theorem Th14:
   F is commutative associative & F has_a_unity & e = the_unity_wrt F &
   G is_distributive_wrt F & G.(d,e) = e
    implies G.(d,F$$(B,f)) = F $$(B,G[;](d,f))
 proof assume that
A1:   F is commutative associative and
A2:   F has_a_unity and
A3:   e = the_unity_wrt F and
A4:   G is_distributive_wrt F;
   defpred X[Element of Fin C] means G.(d,F$$($1,f)) = F $$($1,G[;](d,f));
  assume G.(d,e) = e;
   then G.(d,F$$({}.C,f)) = e by A1,A2,A3,SETWISEO:40
                      .= F $$({}.C,G[;](d,f)) by A1,A2,A3,SETWISEO:40;
   then A5: X[{}.C];
A6:
  for B' being Element of Fin C, b being Element of C
      holds X[B'] & not b in B' implies X[B' \/ {b}]
  proof let B',c such that
A7:   G.(d,F$$(B',f)) = F $$(B',G[;](d,f)) and
A8:   not c in B';
     thus G.(d,F$$(B' \/ {c},f))
         = G.(d,F.(F$$(B',f),f.c)) by A1,A2,A8,Th4
        .= F.(G.(d,F$$(B',f)),G.(d,f.c)) by A4,BINOP_1:23
        .= F.(F $$(B',G[;](d,f)),(G[;](d,f)).c) by A7,FUNCOP_1:66
        .= F $$(B' \/ {c},G[;](d,f)) by A1,A2,A8,Th4;
     end;
    for B holds X[B] from FinSubInd1(A5,A6);
  hence thesis;
 end;

theorem Th15:
   F is commutative associative & F has_a_unity & e = the_unity_wrt F &
   G is_distributive_wrt F & G.(e,d) = e
    implies G.(F$$(B,f),d) = F $$(B,G[:](f,d))
 proof assume that
A1:   F is commutative associative and
A2:   F has_a_unity and
A3:   e = the_unity_wrt F and
A4:   G is_distributive_wrt F;
    defpred X[Element of Fin C] means G.(F$$($1,f),d) = F $$($1,G[:](f,d));
   assume G.(e,d) = e;
then    G.(F$$({}.C,f),d) = e by A1,A2,A3,SETWISEO:40
                      .= F $$({}.C,G[:](f,d)) by A1,A2,A3,SETWISEO:40;
    then
A5:   X[{}.C];
A6: for B' being (Element of Fin C), b being Element of C
      holds X[B'] & not b in B' implies X[B' \/ {b}]
  proof let B',c such that
A7:   G.(F$$(B',f),d) = F $$(B',G[:](f,d)) and
A8:   not c in B';
     thus G.(F$$(B' \/ {c},f),d)
         = G.(F.(F$$(B',f),f.c),d) by A1,A2,A8,Th4
        .= F.(G.(F$$(B',f),d),G.(f.c,d)) by A4,BINOP_1:23
        .= F.(F $$(B',G[:](f,d)),(G[:](f,d)).c) by A7,FUNCOP_1:60
        .= F $$(B' \/ {c},G[:](f,d)) by A1,A2,A8,Th4;
     end;
    for B holds X[B] from FinSubInd1(A5,A6);
  hence thesis;
 end;

theorem
     F is commutative associative & F has_a_unity & F has_an_inverseOp &
    G is_distributive_wrt F
     implies G.(d,F$$(B,f)) = F $$(B,G[;](d,f))
 proof assume
A1:   F is commutative associative & F has_a_unity &
      F has_an_inverseOp & G is_distributive_wrt F;
  set e = the_unity_wrt F;
    G.(d,e) = e by A1,FINSEQOP:70;
  hence thesis by A1,Th14;
 end;

theorem
     F is commutative associative & F has_a_unity & F has_an_inverseOp &
    G is_distributive_wrt F
    implies G.(F$$(B,f),d) = F $$(B,G[:](f,d))
 proof assume
A1:   F is commutative associative & F has_a_unity &
      F has_an_inverseOp & G is_distributive_wrt F;
   set e = the_unity_wrt F;
    G.(e,d) = e by A1,FINSEQOP:70;
  hence thesis by A1,Th15;
 end;

theorem Th18:
   F is commutative associative & F has_a_unity &
   H is commutative associative & H has_a_unity &
   h.the_unity_wrt F = the_unity_wrt H &
   (for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2))
     implies h.(F$$(B,f)) = H $$(B,h*f)
 proof assume that
A1: F is commutative associative & F has_a_unity and
A2: H is commutative associative & H has_a_unity and
A3: h.the_unity_wrt F = the_unity_wrt H and
A4: for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2);
   defpred X[Element of Fin C] means h.(F$$($1,f)) = H $$($1,h*f);
  h.(F$$({}.C,f)) = the_unity_wrt H by A1,A3,SETWISEO:40
                   .= H $$({}.C,h*f) by A2,SETWISEO:40;
   then
A5:    X[{}.C];
A6: for B' being (Element of Fin C), b being Element of C
      holds X[B'] & not b in B' implies X[B' \/ {b}]
  proof let B,c such that
A7:   h.(F$$(B,f)) = H $$(B,h*f) and
A8:   not c in B;
     thus h.(F$$(B \/ {c},f)) = h.(F.(F$$(B,f),f.c)) by A1,A8,Th4
                            .= H.(H $$(B,h*f),h.(f.c)) by A4,A7
                            .= H.(H $$(B,h*f),(h*f).c) by FUNCT_2:21
                            .= H $$(B \/ {c},h*f) by A2,A8,Th4;
    end;
     for B holds X[B] from FinSubInd1(A5,A6);
   hence thesis;
 end;

theorem
     F is commutative associative & F has_a_unity &
   u.the_unity_wrt F = the_unity_wrt F & u is_distributive_wrt F
     implies u.(F$$(B,f)) = F $$(B,u*f)
 proof assume
A1: F is commutative associative & F has_a_unity &
    u.the_unity_wrt F = the_unity_wrt F;
  assume for d1,d2 holds u.(F.(d1,d2)) = F.(u.d1,u.d2);
  hence thesis by A1,Th18;
 end;

theorem
     F is commutative associative & F has_a_unity & F has_an_inverseOp &
     G is_distributive_wrt F
      implies G[;](d,id D).(F$$(B,f)) = F $$(B,G[;](d,id D)*f)
 proof assume
A1:  F is commutative associative & F has_a_unity & F has_an_inverseOp &
     G is_distributive_wrt F;
  set e = the_unity_wrt F;
  set u = G[;](d,id D);
    u is_distributive_wrt F by A1,FINSEQOP:55;
  then G[;](d,id D).e = e & for d1,d2 holds u.(F.(d1,d2)) = F.(u.d1,u.d2)
   by A1,BINOP_1:def 12,FINSEQOP:73;
  hence thesis by A1,Th18;
 end;

theorem
     F is commutative associative & F has_a_unity & F has_an_inverseOp
    implies (the_inverseOp_wrt F).(F$$(B,f)) = F $$(B,(the_inverseOp_wrt F)*f)
 proof assume
A1: F is commutative associative & F has_a_unity & F has_an_inverseOp;
  set e = the_unity_wrt F, u = the_inverseOp_wrt F;
    u is_distributive_wrt F by A1,FINSEQOP:67;
  then u.e = e & for d1,d2 holds u.(F.(d1,d2)) = F.(u.d1,u.d2)
   by A1,BINOP_1:def 12,FINSEQOP:65;
  hence thesis by A1,Th18;
 end;

definition let D,p,d;
  func [#](p,d) -> Function of NAT,D equals
:Def1: (NAT --> d) +* p;
 coherence;
end;

theorem Th22:
   (i in dom p implies [#](p,d).i = p.i) &
   (not i in dom p implies [#](p,d).i = d)
proof
A1: [#](p,d) = (NAT --> d) +* p by Def1;
 hence i in dom p implies [#](p,d).i = p.i by FUNCT_4:14;
 assume
   not i in dom p;
 hence [#](p,d).i = (NAT --> d).i by A1,FUNCT_4:12 .= d by FUNCOP_1:13;
end;

theorem
     [#](p,d)|(dom p) = p
 proof set k = len p, f = [#](p,d);
    Seg k c= NAT;
  then Seg k c= dom f by FUNCT_2:def 1;
then A1:  dom (f|Seg k) = Seg k & dom p = Seg k by FINSEQ_1:def 3,RELAT_1:91;
    now let x;
   assume
A2:   x in Seg k;
   then x is Nat & (f|Seg k).x = f.x by A1,FUNCT_1:70;
   hence (f|Seg k).x = p.x by A1,A2,Th22;
  end;
  hence thesis by A1,FUNCT_1:9;
 end;

theorem
     [#](p^q,d)|(dom p) = p
 proof set k = len p, f = [#](p^q,d);
    Seg k c= NAT;
  then Seg k c= dom f by FUNCT_2:def 1;
then A1:  dom (f|Seg k) = Seg k & dom p = Seg k by FINSEQ_1:def 3,RELAT_1:91;
    now let x;
   assume
A2:   x in Seg k;
A3:   Seg(len(p^q)) = dom (p^q) by FINSEQ_1:def 3;
     k <= k + len q by NAT_1:37;
   then k <= len (p^q) by FINSEQ_1:35;
   then Seg k c= Seg len(p^q) by FINSEQ_1:7;
   then (f|Seg k).x = f.x & x in Seg(len(p^q)) by A1,A2,FUNCT_1:70;
   hence (f|Seg k).x = (p^q).x by A3,Th22
                    .= p.x by A1,A2,FINSEQ_1:def 7;
  end;
  hence thesis by A1,FUNCT_1:9;
 end;

theorem
     rng [#](p,d) = rng p \/ {d}
 proof
    now let y;
   thus y in rng [#](p,d) implies y in rng p \/ {d}
    proof assume y in rng [#](p,d);
     then consider x such that
A1:   x in dom [#](p,d) and
A2:   y = [#](p,d).x by FUNCT_1:def 5;
     reconsider i = x as Nat by A1;
       now per cases;
      case
A3:      i in dom p;
       then y = p.i by A2,Th22;
       hence y in rng p by A3,FUNCT_1:def 5;
      case not i in dom p;
       then y = d by A2,Th22;
       hence y in {d} by TARSKI:def 1;
     end;
     hence y in rng p \/ {d} by XBOOLE_0:def 2;
    end;
   assume
A4:   y in rng p \/ {d};
      now per cases by A4,XBOOLE_0:def 2;
     suppose y in rng p;
       then consider i such that
A5:     i in dom p & y = p.i by FINSEQ_2:11;
        i in NAT & y = [#](p,d).i by A5,Th22;
      hence y in rng [#](p,d) by FUNCT_2:6;
     suppose
A6:     y in {d};
        dom p = Seg len p by FINSEQ_1:def 3;
      then y = d & not len p + 1 in dom p & len p + 1 is Element of NAT
        by A6,Lm2,TARSKI:def 1;
      then y = [#](p,d).(len p + 1) & len p + 1 in NAT by Th22;
     hence y in rng [#](p,d) by FUNCT_2:6;
    end;
   hence y in rng [#](p,d);
  end;
  hence thesis by TARSKI:2;
 end;

theorem
     h*[#](p,d) = [#](h*p,h.d)
 proof
    now let i be Element of NAT;
A1:  len(h*p) = len p by FINSEQ_2:37;
A2:  Seg len p = dom p & dom(h*p)=Seg len(h*p) by FINSEQ_1:def 3;
     now per cases;
    suppose
A3:    i in dom p;
     hence h.([#](p,d).i) = h.(p.i) by Th22
                      .= (h*p).i by A3,FUNCT_1:23
                      .= [#](h*p,h.d).i by A1,A2,A3,Th22;
    suppose
A4:    not i in dom p;
     hence h.([#](p,d).i) = h.d by Th22
                       .= [#](h*p,h.d).i by A1,A2,A4,Th22;
   end;
   hence (h*[#](p,d)).i = [#](h*p,h.d).i by FUNCT_2:21;
  end;
  hence thesis by FUNCT_2:113;
 end;

Lm4:
   len p = len q & F.(e,e) = e implies F.:([#](p,e),[#](q,e)) = [#](F.:(p,q),e)
 proof assume that
A1:  len p = len q and
A2:  F.(e,e) = e;
  set r = F.:(p,q);
A3: len r = len p by A1,FINSEQ_2:86;
A4:  dom p = Seg len p & dom r = Seg len r & dom q = Seg len q
         by FINSEQ_1:def 3;
    now let i be Element of NAT;
     now per cases;
    suppose
A5:    i in dom p;
     hence F.([#](p,e).i,[#](q,e).i) = F.(p.i,[#](q,e).i) by Th22
                               .= F.(p.i,q.i) by A1,A4,A5,Th22
                               .= r.i by A3,A4,A5,FUNCOP_1:28
                               .= [#](r,e).i by A3,A4,A5,Th22;
    suppose
A6:    not i in dom p;
     hence F.([#](p,e).i,[#](q,e).i) = F.(e,[#](q,e).i) by Th22
                               .= e by A1,A2,A4,A6,Th22
                               .= [#](r,e).i by A3,A4,A6,Th22;
   end;
   hence F.:([#](p,e),[#](q,e)).i = [#](r,e).i by FUNCOP_1:48;
  end;
  hence thesis by FUNCT_2:113;
 end;

Lm5:
   F.(e,d) = e implies F[:]([#](p,e),d) = [#](F[:](p,d),e)
 proof assume
A1:  F.(e,d) = e;
    now let i be Element of NAT;
A2:  len(F[:](p,d)) = len p by FINSEQ_2:98;
A3:  dom(F[:](p,d)) = Seg len(F[:](p,d)) & dom p = Seg len p by FINSEQ_1:def 3;
     now per cases;
    suppose
A4:    i in dom p;
     hence F.([#](p,e).i,d) = F.(p.i,d) by Th22
                        .= (F[:](p,d)).i by A2,A3,A4,FUNCOP_1:35
                        .= ([#](F[:](p,d),e)).i by A2,A3,A4,Th22;
    suppose
A5:    not i in dom p;
     hence F.([#](p,e).i,d) = F.(e,d) by Th22
                        .= ([#](F[:](p,d),e)).i by A1,A2,A3,A5,Th22;
   end;
   hence (F[:]([#](p,e),d)).i = ([#](F[:](p,d),e)).i by FUNCOP_1:60;
  end;
  hence thesis by FUNCT_2:113;
 end;

Lm6:
   F.(d,e) = e implies F[;](d,[#](p,e)) = [#](F[;](d,p),e)
 proof assume
A1:  F.(d,e) = e;
    now let i be Element of NAT;
A2:  len(F[;](d,p)) = len p by FINSEQ_2:92;
A3:  dom(F[;](d,p)) = Seg len(F[;](d,p)) & dom p = Seg len p by FINSEQ_1:def 3;
     now per cases;
    suppose
A4:    i in dom p;
     hence F.(d,[#](p,e).i) = F.(d,p.i) by Th22
                        .= (F[;](d,p)).i by A2,A3,A4,FUNCOP_1:42
                        .= ([#](F[;](d,p),e)).i by A2,A3,A4,Th22;
    suppose
A5:    not i in dom p;
     hence F.(d,[#](p,e).i) = F.(d,e) by Th22
                        .= ([#](F[;](d,p),e)).i by A1,A2,A3,A5,Th22;
   end;
   hence (F[;](d,[#](p,e))).i = ([#](F[;](d,p),e)).i by FUNCOP_1:66;
  end;
  hence thesis by FUNCT_2:113;
 end;

definition let i;
 redefine func Seg i -> Element of Fin NAT;
  coherence by Lm1;
end;

definition let f be FinSequence;
 redefine func dom f -> Element of Fin NAT;
  coherence
 proof dom f = Seg len f by FINSEQ_1:def 3;
  hence thesis;
 end;
end;

definition let D,p,F;
 assume
A1: (F has_a_unity or len p >= 1) & F is associative commutative;
 redefine func F "**" p equals
:Def2: F $$(dom p,[#](p,the_unity_wrt F));
  compatibility
   proof
      F "**" p = F $$(dom p,(NAT-->the_unity_wrt F)+*p) by A1,FINSOP_1:4
          .= F $$(dom p,[#](p,the_unity_wrt F)) by Def1;
    hence thesis;
   end;
 synonym F $$ p;
end;

canceled 8;

theorem Th35:
   F has_a_unity implies F"**"(i|->the_unity_wrt F) = the_unity_wrt F
 proof assume
A1:  F has_a_unity;
   set e = the_unity_wrt F;
    defpred X[Nat] means F"**"($1|->e) = e;
 F"**"(0|->e) = F"**" <*>D by FINSEQ_2:72
      .= e by A1,FINSOP_1:11;
    then
A2:  X[0];
A3: for i st X[i] holds X[i+1]
   proof let i;
    assume
A4:   F"**"(i|->e) = e;
    thus F"**"((i+1)|->e) = F"**"((i|->e)^<*e*>) by FINSEQ_2:74
          .= F.(F"**"(i|->e),e) by A1,FINSOP_1:5
          .= e by A1,A4,SETWISEO:23;
   end;
     for i holds X[i] from Ind(A2,A3);
  hence thesis;
 end;

canceled;

theorem Th37:
   F is associative & (i>=1 & j>=1 or F has_a_unity)
    implies F"**"((i+j)|->d) = F.(F"**"(i|->d),F"**"(j|->d))
 proof assume
A1:  F is associative;
  set p1 = (i|->d),p2 = (j|->d);
  assume i>=1 & j>=1 or F has_a_unity;
  then len p1 >= 1 & len p2 >= 1 or F has_a_unity by FINSEQ_2:69;
  then F "**"(p1^p2) = F.(F"**"p1,F"**"p2) by A1,FINSOP_1:6;
  hence thesis by FINSEQ_2:143;
 end;

theorem
     F is commutative associative & (i>=1 & j>=1 or F has_a_unity)
    implies F"**"((i*j)|->d) = F"**"(j|->(F"**"(i|->d)))
 proof assume
A1:  F is commutative associative & (i>=1 & j>=1 or F has_a_unity);
  per cases by NAT_1:19;
   suppose
A2:   i = 0 or j = 0;
    set e = the_unity_wrt F;
A3:  now per cases by A2;
      suppose i = 0;
       then i|->d = <*>D by FINSEQ_2:72;
       then F"**"(i|->d) = e by A1,A2,FINSOP_1:11;
       hence F"**"(j|->(F"**"(i|->d))) = e by A1,A2,Th35;
      suppose j = 0;
       then j|->(F"**"(i|->d)) = <*>D by FINSEQ_2:72;
       hence F"**"(j|->(F"**"(i|->d))) = e by A1,A2,FINSOP_1:11;
     end;
      (i*j)|->d = <*>D by A2,FINSEQ_2:72;
    hence thesis by A1,A2,A3,FINSOP_1:11;
   suppose
A4:   i > 0 & j > 0;
      defpred X[Nat] means $1 <> 0
        implies F"**"((i*$1)|->d) = F"**"($1|->(F"**"(i|->d)));
A5:  X[0];
A6:  for j st X[j] holds X[j+1]
   proof let j such that
A7:  j <> 0 implies F"**"((i*j)|->d) = F"**"(j|->(F"**"(i|->d)));
      now per cases by RLVECT_1:99;
     suppose j = 0;
      then j+1 = 1 & 1|->(F"**"(i|->d)) = <*F"**"(i|->d)*> by FINSEQ_2:73;
      hence thesis by FINSOP_1:12;
     suppose
A8:     j >= 1+0;
       then j > 0 by NAT_1:38;
       then i*j > i*0 by A4,REAL_1:70;
then A9:     i*j >= 1+0 by NAT_1:38;
      F"**"((i*(j+1))|->d)
         = F"**"((i*j+i*1)|->d) by XCMPLX_1:8
        .= F.(F"**"((i*j)|->d),F"**"(i|->d)) by A1,A9,Th37
        .= F.(F"**"((i*j)|->d),F"**"(1|->(F"**"(i|->d)))) by FINSOP_1:17
        .= F"**"((j+1)|->(F"**"(i|->d))) by A1,A7,A8,Th37;
     hence thesis;
    end;
    hence thesis;
   end;
     for j holds X[j] from Ind(A5,A6);
   hence thesis by A4;
 end;

theorem Th39:
   F has_a_unity & H has_a_unity & h.the_unity_wrt F = the_unity_wrt H &
   (for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2))
     implies h.(F"**"p) = H "**"(h*p)
 proof assume that
A1: F has_a_unity and
A2: H has_a_unity and
A3: h.the_unity_wrt F = the_unity_wrt H and
A4: for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2);
    defpred X[FinSequence of D] means h.(F"**"$1) = H "**"(h*$1);
    h.(F"**"<*>D) = h.(the_unity_wrt F) by A1,FINSOP_1:11
      .= H "**"(<*>E) by A2,A3,FINSOP_1:11
      .= H "**"(h*<*>D) by RELAT_1:62;
    then
A5:  X[<*>D];
A6: for q,d st X[q] holds X[q^<*d*>]
  proof let q,d such that
A7:  h.(F"**"q) = H "**"(h*q);
   thus h.(F"**"(q^<*d*>)) = h.(F.(F"**"q,d)) by A1,FINSOP_1:5
         .= H.(H "**"(h*q),h.d) by A4,A7
         .= H "**" ((h*q)^<*h.d*>) by A2,FINSOP_1:5
         .= H "**"(h*(q^<*d*>)) by FINSEQOP:9;
  end;
     X[q] from IndSeqD(A5,A6);
  hence thesis;
 end;

theorem
     F has_a_unity & u.the_unity_wrt F = the_unity_wrt F &
   u is_distributive_wrt F
     implies u.(F"**"p) = F "**"(u*p)
 proof assume
A1: F has_a_unity &
    u.the_unity_wrt F = the_unity_wrt F;
  assume for d1,d2 holds u.(F.(d1,d2)) = F.(u.d1,u.d2);
  hence thesis by A1,Th39;
 end;

theorem
     F is associative & F has_a_unity & F has_an_inverseOp &
     G is_distributive_wrt F
      implies G[;](d,id D).(F"**"p) = F "**"(G[;](d,id D)*p)
 proof assume
A1:  F is associative & F has_a_unity & F has_an_inverseOp &
     G is_distributive_wrt F;
  set e = the_unity_wrt F;
  set u = G[;](d,id D);
    u is_distributive_wrt F by A1,FINSEQOP:55;
  then G[;](d,id D).e = e & for d1,d2 holds u.(F.(d1,d2)) = F.(u.d1,u.d2)
   by A1,BINOP_1:def 12,FINSEQOP:73;
  hence thesis by A1,Th39;
 end;

theorem
     F is commutative associative & F has_a_unity & F has_an_inverseOp
    implies (the_inverseOp_wrt F).(F"**"p) = F "**"((the_inverseOp_wrt F)*p)
 proof assume
A1: F is commutative associative & F has_a_unity & F has_an_inverseOp;
  set e = the_unity_wrt F, u = the_inverseOp_wrt F;
    u is_distributive_wrt F by A1,FINSEQOP:67;
  then u.e = e & for d1,d2 holds u.(F.(d1,d2)) = F.(u.d1,u.d2)
   by A1,BINOP_1:def 12,FINSEQOP:65;
  hence thesis by A1,Th39;
 end;

theorem Th43:
   F is commutative associative &
   F has_a_unity & e = the_unity_wrt F & G.(e,e) = e &
   (for d1,d2,d3,d4 holds F.(G.(d1,d2),G.(d3,d4))= G.(F.(d1,d3),F.(d2,d4))) &
    len p = len q implies G.(F"**"p,F"**"q) = F "**"(G.:(p,q))
 proof assume that
A1:   F is commutative & F is associative and
A2:   F has_a_unity and
A3:   e = the_unity_wrt F and
A4:   G.(e,e) = e and
A5:   F.(G.(d1,d2),G.(d3,d4))= G.(F.(d1,d3),F.(d2,d4)) and
A6:   len p = len q;
A7:   len p = len(G.:(p,q)) by A6,FINSEQ_2:86;
A8:   dom p = Seg len p & dom q = Seg len q by FINSEQ_1:def 3;
A9:   dom(G.:(p,q)) = Seg len(G.:(p,q)) by FINSEQ_1:def 3;
   thus G.(F "**"p,F "**"q)
      = G.(F $$(dom p,[#](p,e)),F "**"q) by A1,A2,A3,Def2
     .= G.(F $$(dom p,[#](p,e)),F $$(dom q,[#](q,e))) by A1,A2,A3,Def2
     .= F $$(dom p,G.:([#](p,e),[#](q,e))) by A1,A2,A3,A4,A5,A6,A8,Th11
     .= F $$(dom(G.:(p,q)),[#](G.:(p,q),e)) by A4,A6,A7,A8,A9,Lm4
     .= F "**"(G.:(p,q)) by A1,A2,A3,Def2;
 end;

theorem Th44:
   F is commutative associative &
   F has_a_unity & e = the_unity_wrt F & G.(e,e) = e &
   (for d1,d2,d3,d4 holds F.(G.(d1,d2),G.(d3,d4))= G.(F.(d1,d3),F.(d2,d4)))
     implies G.(F"**"T1,F"**"T2) = F "**"(G.:(T1,T2))
 proof len T1 = i & len T2 = i by FINSEQ_2:109; hence thesis by Th43; end;

theorem Th45:
   F is commutative associative & F has_a_unity &
    len p = len q implies F.(F"**"p,F"**"q) = F "**"(F.:(p,q))
 proof assume
A1:  F is commutative & F is associative & F has_a_unity;
   set e = the_unity_wrt F;
     F.(e,e) = e &
    for d1,d2,d3,d4 holds F.(F.(d1,d2),F.(d3,d4))= F.(F.(d1,d3),F.(d2,d4))
     by A1,Lm3,SETWISEO:23;
   hence thesis by A1,Th43;
 end;

theorem Th46:
   F is commutative associative & F has_a_unity
    implies F.(F"**"T1,F"**"T2) = F "**"(F.:(T1,T2))
 proof len T1 = i & len T2 = i by FINSEQ_2:109; hence thesis by Th45; end;

theorem
     F is commutative associative & F has_a_unity
    implies F"**"(i|->(F.(d1,d2))) = F.(F"**"(i|->d1),F"**"(i|->d2))
 proof
   reconsider T1 = i|->d1, T2 = i|->d2 as Element of i-tuples_on D
      by FINSEQ_2:132;
     i|->(F.(d1,d2)) = F.:(T1,T2) by FINSEQOP:18;
  hence thesis by Th46;
 end;

theorem
     F is commutative associative & F has_a_unity &
    F has_an_inverseOp & G = F*(id D,the_inverseOp_wrt F)
     implies G.(F"**"T1,F"**"T2) = F "**"(G.:(T1,T2))
 proof assume
A1:   F is commutative associative & F has_a_unity &
      F has_an_inverseOp & G = F*(id D,the_inverseOp_wrt F);
   set e = the_unity_wrt F;
     G.(e,e) = e &
     for d1,d2,d3,d4 holds F.(G.(d1,d2),G.(d3,d4))= G.(F.(d1,d3),F.(d2,d4))
    by A1,FINSEQOP:91,94;
   hence thesis by A1,Th44;
 end;

theorem Th49:
   F is commutative associative & F has_a_unity & e = the_unity_wrt F &
   G is_distributive_wrt F & G.(d,e) = e
    implies G.(d,F"**"p) = F "**"(G[;](d,p))
 proof assume that
A1:  F is commutative & F is associative & F has_a_unity and
A2:  e = the_unity_wrt F and
A3:  G is_distributive_wrt F and
A4:  G.(d,e) = e;
A5:  len p = len(G[;](d,p)) by FINSEQ_2:92;
A6:  Seg len p = dom p & Seg len(G[;](d,p)) = dom(G[;](d,p)) by FINSEQ_1:def 3;
   thus G.(d,F"**"p) = G.(d,F$$(dom p,[#](p,e))) by A1,A2,Def2
                  .= F $$(dom p,G[;](d,[#](p,e))) by A1,A2,A3,A4,Th14
                  .= F $$(dom p,[#](G[;](d,p),e)) by A4,Lm6
                  .= F "**"(G[;](d,p)) by A1,A2,A5,A6,Def2;
 end;

theorem Th50:
   F is commutative associative & F has_a_unity & e = the_unity_wrt F &
   G is_distributive_wrt F & G.(e,d) = e
    implies G.(F"**"p,d) = F "**"(G[:](p,d))
 proof assume that
A1:  F is commutative associative & F has_a_unity and
A2:  e = the_unity_wrt F and
A3:  G is_distributive_wrt F and
A4:  G.(e,d) = e;
A5:  len p = len(G[:](p,d)) by FINSEQ_2:98;
A6:  Seg len p = dom p & Seg len(G[:](p,d)) = dom(G[:](p,d)) by FINSEQ_1:def 3;
   thus G.(F"**"p,d) = G.(F$$(dom p,[#](p,e)),d) by A1,A2,Def2
                  .= F $$(dom p,G[:]([#](p,e),d)) by A1,A2,A3,A4,Th15
                  .= F $$(dom p,[#](G[:](p,d),e)) by A4,Lm5
                  .= F "**"(G[:](p,d)) by A1,A2,A5,A6,Def2;
 end;

theorem
     F is commutative associative & F has_a_unity & F has_an_inverseOp &
    G is_distributive_wrt F
     implies G.(d,F"**"p) = F "**"(G[;](d,p))
 proof assume
A1:   F is commutative associative & F has_a_unity &
      F has_an_inverseOp & G is_distributive_wrt F;
  set e = the_unity_wrt F;
    G.(d,e) = e by A1,FINSEQOP:70;
  hence thesis by A1,Th49;
 end;

theorem
     F is commutative associative & F has_a_unity & F has_an_inverseOp &
    G is_distributive_wrt F
     implies G.(F"**"p,d) = F "**"(G[:](p,d))
 proof assume
A1:   F is commutative associative & F has_a_unity &
      F has_an_inverseOp & G is_distributive_wrt F;
  set e = the_unity_wrt F;
    G.(e,d) = e by A1,FINSEQOP:70;
  hence thesis by A1,Th50;
 end;

Back to top