setwop_2.miz



    begin

    reserve x,y for set;

    reserve C,C9,D,E for non empty set;

    reserve c,c9,c1,c2,c3 for Element of C;

    reserve B,B9,B1,B2 for Element of ( Fin C);

    reserve A for Element of ( Fin C9);

    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,f9 for Function of C, D;

    reserve g for Function of C9, 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: for i be Nat holds ( Seg i) is Element of ( Fin NAT ) by FINSUB_1:def 5;

    

     Lm2: for i holds not (i + 1) in ( Seg i) by FINSEQ_1: 1, XREAL_1: 29;

    theorem :: SETWOP_2:1

    

     Th1: 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 be 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 <> {} holds 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: 62;

      then

       A6: c2 in ( {c1, c2} \ {c1}) by TARSKI:def 1;

      

      thus (F $$ ( {.c1, c2.},f)) = (g . ( {.c1.} \/ {.c2.})) by A3, ENUMSET1: 1

      .= (F . ((g . {c1}),(f . c2))) by A5, A6, ZFMISC_1: 7

      .= (F . ((f . c1),(f . c2))) by A4;

    end;

    theorem :: SETWOP_2:2

    

     Th2: F is commutative associative & (B <> {} or F is having_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 is having_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: 31;

        

        hence (F . ((F $$ (B,f)),(f . c))) = (f . c) by A2, A4, SETWISEO: 15

        .= (F $$ ((B \/ {.c.}),f)) by A1, A4, SETWISEO: 17;

      end;

        suppose

         A5: B <> {} ;

        consider g9 be Function of ( Fin C), D such that

         A6: (F $$ (B,f)) = (g9 . B) and for e st e is_a_unity_wrt F holds (g9 . {} ) = e and

         A7: for c9 holds (g9 . {c9}) = (f . c9) and

         A8: for B9 st B9 c= B & B9 <> {} holds for c9 st c9 in (B \ B9) holds (g9 . (B9 \/ {c9})) = (F . ((g9 . B9),(f . c9))) by A1, A2, SETWISEO:def 3;

        consider g be Function of ( Fin C), D such that

         A9: (F $$ ((B \/ {.c.}),f)) = (g . (B \/ {c})) and for e st e is_a_unity_wrt F holds (g . {} ) = e and

         A10: for c9 holds (g . {c9}) = (f . c9) and

         A11: for B9 st B9 c= (B \/ {c}) & B9 <> {} holds for c9 st c9 in ((B \/ {c}) \ B9) holds (g . (B9 \/ {c9})) = (F . ((g . B9),(f . c9))) by A1, SETWISEO:def 3;

        defpred X[ set] means $1 <> {} & $1 c= B implies (g . $1) = (g9 . $1);

        

         A12: for B9 be Element of ( Fin C), b be Element of C holds X[B9] & not b in B9 implies X[(B9 \/ {b})]

        proof

          

           A13: B c= (B \/ {c}) by XBOOLE_1: 7;

          let B9, c9 such that

           A14: B9 <> {} & B9 c= B implies (g . B9) = (g9 . B9) and

           A15: not c9 in B9 and (B9 \/ {c9}) <> {} and

           A16: (B9 \/ {c9}) c= B;

          

           A17: c9 in B by A16, ZFMISC_1: 137;

          then

           A18: c9 in (B \ B9) by A15, XBOOLE_0:def 5;

          c9 in (B \/ {c}) by A17, XBOOLE_0:def 3;

          then

           A19: c9 in ((B \/ {c}) \ B9) by A15, XBOOLE_0:def 5;

          B9 c= B by A16, XBOOLE_1: 11;

          then

           A20: B9 c= (B \/ {c}) by A13, XBOOLE_1: 1;

          per cases ;

            suppose

             A21: B9 = {} ;

            then (g . (B9 \/ {c9})) = (f . c9) by A10;

            hence thesis by A7, A21;

          end;

            suppose

             A22: B9 <> {} ;

            

            hence (g . (B9 \/ {c9})) = (F . ((g9 . B9),(f . c9))) by A11, A14, A16, A20, A19, XBOOLE_1: 11

            .= (g9 . (B9 \/ {c9})) by A8, A16, A18, A22, XBOOLE_1: 11;

          end;

        end;

        

         A23: X[( {}. C)];

        

         A24: for B9 holds X[B9] from SETWISEO:sch 2( A23, A12);

        c in (B \/ {c}) by ZFMISC_1: 136;

        then c in ((B \/ {c}) \ B) by A3, XBOOLE_0:def 5;

        

        hence (F $$ ((B \/ {.c.}),f)) = (F . ((g . B),(f . c))) by A5, A9, A11, XBOOLE_1: 7

        .= (F . ((F $$ (B,f)),(f . c))) by A5, A6, A24;

      end;

    end;

    theorem :: SETWOP_2:3

    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} by TARSKI:def 2;

      

      thus (F $$ ( {.c1, c2, c3.},f)) = (F $$ (( {.c1, c2.} \/ {.c3.}),f)) by ENUMSET1: 3

      .= (F . ((F $$ ( {.c1, c2.},f)),(f . c3))) by A1, A3, Th2

      .= (F . ((F . ((f . c1),(f . c2))),(f . c3))) by A1, A2, Th1;

    end;

    theorem :: SETWOP_2:4

    F is commutative associative & (B1 <> {} & B2 <> {} or F is having_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 is having_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: 15

              .= (F . ((F $$ (( {}. C),f)),(F $$ (B2,f)))) by A1, A2, A4, SETWISEO: 31

              .= (F . ((F $$ (B1,f)),(F $$ (B2,f)))) by A5;

            end;

              suppose

               A6: B2 = {} ;

              

              hence (F $$ ((B1 \/ B2),f)) = (F . ((F $$ (B1,f)),( the_unity_wrt F))) by A2, SETWISEO: 15

              .= (F . ((F $$ (B1,f)),(F $$ (( {}. C),f)))) by A1, A2, A4, SETWISEO: 31

              .= (F . ((F $$ (B1,f)),(F $$ (B2,f)))) by A6;

            end;

          end;

          hence thesis;

        end;

          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: for B9 be Element of ( Fin C), b be Element of C holds X[B9] & not b in B9 implies X[(B9 \/ {.b.})]

          proof

            let B, c such that

             A9: B <> {} & (B1 /\ B) = {} implies (F $$ ((B1 \/ B),f)) = (F . ((F $$ (B1,f)),(F $$ (B,f)))) and

             A10: not c in B and (B \/ {c}) <> {} ;

            assume

             A11: (B1 /\ (B \/ {c})) = {} ;

            then

             A12: B1 misses (B \/ {c});

            c in (B \/ {c}) by ZFMISC_1: 136;

            then

             A13: not c in B1 by A11, XBOOLE_0:def 4;

            

             A14: B <> {} & B1 misses B implies (F $$ ((B1 \/ B),f)) = (F . ((F $$ (B1,f)),(F $$ (B,f)))) by A9;

            now

              per cases ;

                suppose

                 A15: B = {} ;

                

                hence (F $$ ((B1 \/ (B \/ {.c.})),f)) = (F . ((F $$ (B1,f)),(f . c))) by A1, A7, A13, Th2

                .= (F . ((F $$ (B1,f)),(F $$ ((B \/ {.c.}),f)))) by A1, A15, SETWISEO: 17;

              end;

                suppose

                 A16: B <> {} ;

                

                 A17: not c in (B1 \/ B) by A10, A13, XBOOLE_0:def 3;

                

                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, A14, A12, A16, A17, Th2, XBOOLE_1: 7, XBOOLE_1: 63

                .= (F . ((F $$ (B1,f)),(F . ((F $$ (B,f)),(f . c))))) by A1

                .= (F . ((F $$ (B1,f)),(F $$ ((B \/ {.c.}),f)))) by A1, A10, A16, Th2;

              end;

            end;

            hence thesis;

          end;

          

           A18: X[( {}. C)];

          for B2 holds X[B2] from SETWISEO:sch 2( A18, A8);

          hence thesis by A3, A7;

        end;

      end;

      hence thesis;

    end;

    theorem :: SETWOP_2:5

    

     Th5: F is commutative associative & (A <> {} or F is having_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

      defpred X[ Element of ( Fin C9)] means $1 <> {} or F is having_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));

      assume

       A1: F is commutative associative;

      

       A2: for B9 be Element of ( Fin C9), b be Element of C9 holds X[B9] & not b in B9 implies X[(B9 \/ {.b.})]

      proof

        let A9 be Element of ( Fin C9), a be Element of C9 such that

         A3: A9 <> {} or F is having_a_unity implies for B st ex s st ( dom s) = A9 & ( rng s) = B & s is one-to-one & (g | A9) = (f * s) holds (F $$ (A9,g)) = (F $$ (B,f)) and

         A4: not a in A9;

        assume (A9 \/ {a}) <> {} or F is having_a_unity;

        let B;

        set A = (A9 \/ {.a.});

        given s such that

         A5: ( dom s) = A and

         A6: ( rng s) = B and

         A7: s is one-to-one and

         A8: (g | A) = (f * s);

        

         A9: a in A by ZFMISC_1: 136;

        then

         A10: (s . a) in B by A5, A6, FUNCT_1:def 3;

        B c= C by FINSUB_1:def 5;

        then

        reconsider c = (s . a) as Element of C by A10;

        set B9 = (B \ {.c.});

        set s9 = (s | A9);

        

         A11: s9 is one-to-one by A7, FUNCT_1: 52;

        now

          let y be object;

          thus y in ( rng s9) implies y in B9

          proof

            assume y in ( rng s9);

            then

            consider x be object such that

             A12: x in ( dom s9) and

             A13: y = (s9 . x) by FUNCT_1:def 3;

            

             A14: (s9 . x) = (s . x) by A12, FUNCT_1: 47;

            

             A15: x in (( dom s) /\ A9) by A12, RELAT_1: 61;

            then x in ( dom s) & x <> a by A4, XBOOLE_0:def 4;

            then (s . x) <> c by A5, A7, A9, FUNCT_1:def 4;

            then

             A16: not y in {c} by A13, A14, TARSKI:def 1;

            x in ( dom s) by A15, XBOOLE_0:def 4;

            then y in B by A6, A13, A14, FUNCT_1:def 3;

            hence thesis by A16, XBOOLE_0:def 5;

          end;

          assume

           A17: y in B9;

          then y in B by XBOOLE_0:def 5;

          then

          consider x be object such that

           A18: x in ( dom s) and

           A19: y = (s . x) by A6, FUNCT_1:def 3;

          

           A20: x in A9 or x in {a} by A5, A18, XBOOLE_0:def 3;

           not y in {c} by A17, XBOOLE_0:def 5;

          then x <> a by A19, TARSKI:def 1;

          then x in (( dom s) /\ A9) by A18, A20, TARSKI:def 1, XBOOLE_0:def 4;

          then x in ( dom s9) & (s9 . x) = (s . x) by FUNCT_1: 48, RELAT_1: 61;

          hence y in ( rng s9) by A19, FUNCT_1:def 3;

        end;

        then

         A21: ( rng s9) = B9 by TARSKI: 2;

        now

          let x be object;

          thus x in ( dom (g | A9)) implies x in ( dom (f * s9))

          proof

            assume x in ( dom (g | A9));

            then

             A22: x in (( dom g) /\ A9) by RELAT_1: 61;

            then

             A23: x in A9 by XBOOLE_0:def 4;

            

             A24: x in ( dom g) by A22, XBOOLE_0:def 4;

            x in A by A23, ZFMISC_1: 136;

            then x in (( dom g) /\ A) by A24, XBOOLE_0:def 4;

            then

             A25: x in ( dom (f * s)) by A8, RELAT_1: 61;

            then

             A26: (s . x) in ( dom f) by FUNCT_1: 11;

            x in ( dom s) by A25, FUNCT_1: 11;

            then x in (( dom s) /\ A9) by A23, XBOOLE_0:def 4;

            then

             A27: x in ( dom s9) by RELAT_1: 61;

            then (s9 . x) = (s . x) by FUNCT_1: 47;

            hence thesis by A26, A27, FUNCT_1: 11;

          end;

          assume

           A28: x in ( dom (f * s9));

          then

           A29: x in ( dom s9) by FUNCT_1: 11;

          then

           A30: x in (( dom s) /\ A9) by RELAT_1: 61;

          then

           A31: x in ( dom s) by XBOOLE_0:def 4;

          (s9 . x) in ( dom f) by A28, FUNCT_1: 11;

          then (s . x) in ( dom f) by A29, FUNCT_1: 47;

          then x in ( dom (g | A)) by A8, A31, FUNCT_1: 11;

          then x in (( dom g) /\ A) by RELAT_1: 61;

          then

           A32: x in ( dom g) by XBOOLE_0:def 4;

          x in A9 by A30, XBOOLE_0:def 4;

          then x in (( dom g) /\ A9) by A32, XBOOLE_0:def 4;

          hence x in ( dom (g | A9)) by RELAT_1: 61;

        end;

        then

         A33: ( dom (g | A9)) = ( dom (f * s9)) by TARSKI: 2;

        a in C9;

        then a in ( dom g) by FUNCT_2:def 1;

        then a in (( dom g) /\ A) by A9, XBOOLE_0:def 4;

        then a in ( dom (f * s)) & (g . a) = ((f * s) . a) by A8, FUNCT_1: 48, RELAT_1: 61;

        then

         A34: (g . a) = (f . c) by FUNCT_1: 12;

        (B9 \/ {c}) = (B \/ {c}) by XBOOLE_1: 39;

        then

         A35: B = (B9 \/ {c}) by A10, ZFMISC_1: 40;

        

         A36: ( dom s9) = A9 by A5, RELAT_1: 62, XBOOLE_1: 7;

        

         A37: for x be object st x in ( dom (g | A9)) holds ((g | A9) . x) = ((f * s9) . x)

        proof

          let x be object;

          assume x in ( dom (g | A9));

          then

           A38: x in (( dom g) /\ A9) by RELAT_1: 61;

          then

           A39: x in A9 by XBOOLE_0:def 4;

          then

           A40: x in A by ZFMISC_1: 136;

          x in ( dom g) by A38, XBOOLE_0:def 4;

          then x in (( dom g) /\ A) by A40, XBOOLE_0:def 4;

          then x in ( dom (f * s)) by A8, RELAT_1: 61;

          then

           A41: x in ( dom s) by FUNCT_1: 11;

          then x in (( dom s) /\ A9) by A39, XBOOLE_0:def 4;

          then

           A42: x in ( dom s9) by RELAT_1: 61;

          then

           A43: (s9 . x) = (s . x) by FUNCT_1: 47;

          

          thus ((g | A9) . x) = (g . x) by A39, FUNCT_1: 49

          .= ((f * s) . x) by A8, A40, FUNCT_1: 49

          .= (f . (s . x)) by A41, FUNCT_1: 13

          .= ((f * s9) . x) by A42, A43, FUNCT_1: 13;

        end;

        then

         A44: (g | A9) = (f * s9) by A33, FUNCT_1: 2;

        now

          let y be object;

          thus y in (g .: A9) implies y in (f .: B9)

          proof

            assume y in (g .: A9);

            then

            consider x be object such that

             A45: x in ( dom g) and

             A46: x in A9 and

             A47: y = (g . x) by FUNCT_1:def 6;

            x in (( dom g) /\ A9) by A45, A46, XBOOLE_0:def 4;

            then

             A48: x in ( dom (g | A9)) by RELAT_1: 61;

            then x in ( dom s9) by A33, FUNCT_1: 11;

            then

             A49: (s9 . x) in B9 by A21, FUNCT_1:def 3;

            y = ((f * s9) . x) by A44, A46, A47, FUNCT_1: 49;

            then

             A50: y = (f . (s9 . x)) by A33, A48, FUNCT_1: 12;

            (s9 . x) in ( dom f) by A33, A48, FUNCT_1: 11;

            hence thesis by A50, A49, FUNCT_1:def 6;

          end;

          assume y in (f .: B9);

          then

          consider x be object such that x in ( dom f) and

           A51: x in B9 and

           A52: y = (f . x) by FUNCT_1:def 6;

          set x9 = ((s9 " ) . x);

          

           A53: x9 in A9 by A11, A36, A21, A51, FUNCT_1: 32;

          A9 c= C9 by FINSUB_1:def 5;

          then x9 in C9 by A53;

          then

           A54: x9 in ( dom g) by FUNCT_2:def 1;

          (s9 . x9) = x by A11, A21, A51, FUNCT_1: 35;

          

          then y = ((f * s9) . x9) by A36, A52, A53, FUNCT_1: 13

          .= (g . x9) by A44, A53, FUNCT_1: 49;

          hence y in (g .: A9) by A53, A54, FUNCT_1:def 6;

        end;

        then

         A55: (f .: B9) = (g .: A9) by TARSKI: 2;

        

         A56: not c in B9 by ZFMISC_1: 56;

        now

          per cases ;

            suppose

             A57: A9 = {} ;

            B9 c= C by FINSUB_1:def 5;

            then B9 c= ( dom f) by FUNCT_2:def 1;

            then

             A58: B9 = {} by A55, A57;

            

            thus (F $$ (A,g)) = (f . c) by A1, A34, A57, SETWISEO: 17

            .= (F $$ (B,f)) by A1, A35, A58, SETWISEO: 17;

          end;

            suppose

             A59: A9 <> {} ;

            A9 c= C9 by FINSUB_1:def 5;

            then A9 c= ( dom g) by FUNCT_2:def 1;

            then

             A60: B9 <> {} by A55, A59;

            

            thus (F $$ (A,g)) = (F . ((F $$ (A9,g)),(g . a))) by A1, A4, A59, Th2

            .= (F . ((F $$ (B9,f)),(f . c))) by A3, A34, A11, A36, A21, A33, A37, A59, FUNCT_1: 2

            .= (F $$ (B,f)) by A1, A35, A56, A60, Th2;

          end;

        end;

        hence thesis;

      end;

      

       A61: X[( {}. C9)]

      proof

        assume

         A62: ( {}. C9) <> {} or F is having_a_unity;

        let B;

        given s such that

         A63: ( dom s) = ( {}. C9) & ( rng s) = B & s is one-to-one and (g | ( {}. C9)) = (f * s);

        (B, {} ) are_equipotent by A63, WELLORD2:def 4;

        then

         A64: B = ( {}. C) by CARD_1: 26;

        (F $$ (( {}. C9),g)) = ( the_unity_wrt F) by A1, A62, SETWISEO: 31;

        hence thesis by A1, A62, A64, SETWISEO: 31;

      end;

      for A holds X[A] from SETWISEO:sch 2( A61, A2);

      hence thesis;

    end;

    theorem :: SETWOP_2:6

    H is commutative associative & (B <> {} or H is having_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 is having_a_unity) and

       A2: f is one-to-one;

      set s = (f | B);

      

       A3: ( rng s) = (f .: B) & ((h * f) | B) = (h * s) by RELAT_1: 83, RELAT_1: 115;

      B c= C by FINSUB_1:def 5;

      then B c= ( dom f) by FUNCT_2:def 1;

      then

       A4: ( dom s) = B by RELAT_1: 62;

      s is one-to-one by A2, FUNCT_1: 52;

      hence thesis by A1, A4, A3, Th5;

    end;

    theorem :: SETWOP_2:7

    F is commutative associative & (B <> {} or F is having_a_unity) & (f | B) = (f9 | B) implies (F $$ (B,f)) = (F $$ (B,f9))

    proof

      assume

       A1: F is commutative associative & (B <> {} or F is having_a_unity);

      set s = ( id B);

      

       A2: ( dom s) = B & ( rng s) = B;

      assume (f | B) = (f9 | B);

      then (f | B) = (f9 * s) by RELAT_1: 65;

      hence thesis by A1, A2, Th5;

    end;

    theorem :: SETWOP_2:8

    F is commutative associative & F is having_a_unity & e = ( the_unity_wrt F) & (f .: B) = {e} implies (F $$ (B,f)) = e

    proof

      assume that

       A1: F is commutative associative and

       A2: F is having_a_unity and

       A3: e = ( the_unity_wrt F);

      defpred X[ Element of ( Fin C)] means (f .: $1) = {e} implies (F $$ ($1,f)) = e;

      

       A4: for B9 be Element of ( Fin C), b be Element of C holds X[B9] & not b in B9 implies X[(B9 \/ {.b.})]

      proof

        let B9, c such that

         A5: (f .: B9) = {e} implies (F $$ (B9,f)) = e and

         A6: not c in B9 and

         A7: (f .: (B9 \/ {c})) = {e};

         A8:

        now

          per cases ;

            suppose B9 = {} ;

            then

             A9: B9 = ( {}. C);

            

            thus (F $$ ((B9 \/ {.c.}),f)) = (F . ((F $$ (B9,f)),(f . c))) by A1, A2, A6, Th2

            .= (F . (e,(f . c))) by A1, A2, A3, A9, SETWISEO: 31;

          end;

            suppose

             A10: B9 <> {} ;

            B9 c= C by FINSUB_1:def 5;

            then

             A11: B9 c= ( dom f) by FUNCT_2:def 1;

            (f .: B9) c= {e} by A7, RELAT_1: 123, XBOOLE_1: 7;

            hence (F $$ ((B9 \/ {.c.}),f)) = (F . (e,(f . c))) by A1, A5, A6, A10, A11, Th2, ZFMISC_1: 33;

          end;

        end;

         {.c.} c= C by FINSUB_1:def 5;

        then

         A12: {c} c= ( dom f) by FUNCT_2:def 1;

        then

         A13: c in ( dom f) by ZFMISC_1: 31;

        ( Im (f,c)) c= {e} by A7, RELAT_1: 123, XBOOLE_1: 7;

        then ( Im (f,c)) = {e} by A12, ZFMISC_1: 33;

        then {e} = {(f . c)} by A13, FUNCT_1: 59;

        then (f . c) = e by ZFMISC_1: 3;

        hence thesis by A2, A3, A8, SETWISEO: 15;

      end;

      

       A14: X[( {}. C)];

      for B holds X[B] from SETWISEO:sch 2( A14, A4);

      hence thesis;

    end;

    theorem :: SETWOP_2:9

    

     Th9: F is commutative associative & F is having_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,f9)))) = (F $$ (B,(G .: (f,f9))))

    proof

      assume that

       A1: F is commutative associative & F is having_a_unity and

       A2: e = ( the_unity_wrt F) and

       A3: (G . (e,e)) = e and

       A4: 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,f9)))) = (F $$ ($1,(G .: (f,f9))));

      

       A5: for B9 be Element of ( Fin C), b be Element of C holds X[B9] & not b in B9 implies X[(B9 \/ {.b.})]

      proof

        let B, c such that

         A6: (G . ((F $$ (B,f)),(F $$ (B,f9)))) = (F $$ (B,(G .: (f,f9)))) and

         A7: not c in B;

        set s9 = (F $$ (B,f9));

        set s = (F $$ (B,f));

        (F $$ ((B \/ {.c.}),f)) = (F . (s,(f . c))) & (F $$ ((B \/ {.c.}),f9)) = (F . (s9,(f9 . c))) by A1, A7, Th2;

        

        hence (G . ((F $$ ((B \/ {.c.}),f)),(F $$ ((B \/ {.c.}),f9)))) = (F . ((G . (s,s9)),(G . ((f . c),(f9 . c))))) by A4

        .= (F . ((G . (s,s9)),((G .: (f,f9)) . c))) by FUNCOP_1: 37

        .= (F $$ ((B \/ {.c.}),(G .: (f,f9)))) by A1, A6, A7, Th2;

      end;

      (F $$ (( {}. C),f)) = e & (F $$ (( {}. C),f9)) = e by A1, A2, SETWISEO: 31;

      then

       A8: X[( {}. C)] by A1, A2, A3, SETWISEO: 31;

      for B holds X[B] from SETWISEO:sch 2( A8, A5);

      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

      .= (F . (d1,(F . ((F . (d2,d3)),d4)))) by A2

      .= (F . (d1,(F . ((F . (d3,d2)),d4)))) by A1

      .= (F . (d1,(F . (d3,(F . (d2,d4)))))) by A2

      .= (F . ((F . (d1,d3)),(F . (d2,d4)))) by A2;

    end;

    theorem :: SETWOP_2:10

    F is commutative associative & F is having_a_unity implies (F . ((F $$ (B,f)),(F $$ (B,f9)))) = (F $$ (B,(F .: (f,f9))))

    proof

      set e = ( the_unity_wrt F);

      assume

       A1: F is commutative & F is associative & F is having_a_unity;

      then (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 Lm3, SETWISEO: 15;

      hence thesis by A1, Th9;

    end;

    theorem :: SETWOP_2:11

    F is commutative associative & F is having_a_unity & F is having_an_inverseOp & G = (F * (( id D),( the_inverseOp_wrt F))) implies (G . ((F $$ (B,f)),(F $$ (B,f9)))) = (F $$ (B,(G .: (f,f9))))

    proof

      assume that

       A1: F is commutative associative & F is having_a_unity and

       A2: F is having_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, A2, FINSEQOP: 86, FINSEQOP: 89;

      hence thesis by A1, Th9;

    end;

    theorem :: SETWOP_2:12

    

     Th12: F is commutative associative & F is having_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 & F is having_a_unity and

       A2: e = ( the_unity_wrt F) and

       A3: G is_distributive_wrt F;

      defpred X[ Element of ( Fin C)] means (G . (d,(F $$ ($1,f)))) = (F $$ ($1,(G [;] (d,f))));

      

       A4: for B9 be Element of ( Fin C), b be Element of C holds X[B9] & not b in B9 implies X[(B9 \/ {.b.})]

      proof

        let B9, c such that

         A5: (G . (d,(F $$ (B9,f)))) = (F $$ (B9,(G [;] (d,f)))) and

         A6: not c in B9;

        

        thus (G . (d,(F $$ ((B9 \/ {.c.}),f)))) = (G . (d,(F . ((F $$ (B9,f)),(f . c))))) by A1, A6, Th2

        .= (F . ((G . (d,(F $$ (B9,f)))),(G . (d,(f . c))))) by A3, BINOP_1: 11

        .= (F . ((F $$ (B9,(G [;] (d,f)))),((G [;] (d,f)) . c))) by A5, FUNCOP_1: 53

        .= (F $$ ((B9 \/ {.c.}),(G [;] (d,f)))) by A1, A6, Th2;

      end;

      assume (G . (d,e)) = e;

      

      then (G . (d,(F $$ (( {}. C),f)))) = e by A1, A2, SETWISEO: 31

      .= (F $$ (( {}. C),(G [;] (d,f)))) by A1, A2, SETWISEO: 31;

      then

       A7: X[( {}. C)];

      for B holds X[B] from SETWISEO:sch 2( A7, A4);

      hence thesis;

    end;

    theorem :: SETWOP_2:13

    

     Th13: F is commutative associative & F is having_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 & F is having_a_unity and

       A2: e = ( the_unity_wrt F) and

       A3: G is_distributive_wrt F;

      defpred X[ Element of ( Fin C)] means (G . ((F $$ ($1,f)),d)) = (F $$ ($1,(G [:] (f,d))));

      

       A4: for B9 be Element of ( Fin C), b be Element of C holds X[B9] & not b in B9 implies X[(B9 \/ {.b.})]

      proof

        let B9, c such that

         A5: (G . ((F $$ (B9,f)),d)) = (F $$ (B9,(G [:] (f,d)))) and

         A6: not c in B9;

        

        thus (G . ((F $$ ((B9 \/ {.c.}),f)),d)) = (G . ((F . ((F $$ (B9,f)),(f . c))),d)) by A1, A6, Th2

        .= (F . ((G . ((F $$ (B9,f)),d)),(G . ((f . c),d)))) by A3, BINOP_1: 11

        .= (F . ((F $$ (B9,(G [:] (f,d)))),((G [:] (f,d)) . c))) by A5, FUNCOP_1: 48

        .= (F $$ ((B9 \/ {.c.}),(G [:] (f,d)))) by A1, A6, Th2;

      end;

      assume (G . (e,d)) = e;

      

      then (G . ((F $$ (( {}. C),f)),d)) = e by A1, A2, SETWISEO: 31

      .= (F $$ (( {}. C),(G [:] (f,d)))) by A1, A2, SETWISEO: 31;

      then

       A7: X[( {}. C)];

      for B holds X[B] from SETWISEO:sch 2( A7, A4);

      hence thesis;

    end;

    theorem :: SETWOP_2:14

    F is commutative associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F implies (G . (d,(F $$ (B,f)))) = (F $$ (B,(G [;] (d,f))))

    proof

      assume that

       A1: F is commutative associative & F is having_a_unity and

       A2: F is having_an_inverseOp and

       A3: G is_distributive_wrt F;

      set e = ( the_unity_wrt F);

      (G . (d,e)) = e by A1, A2, A3, FINSEQOP: 66;

      hence thesis by A1, A3, Th12;

    end;

    theorem :: SETWOP_2:15

    F is commutative associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F implies (G . ((F $$ (B,f)),d)) = (F $$ (B,(G [:] (f,d))))

    proof

      assume that

       A1: F is commutative associative & F is having_a_unity and

       A2: F is having_an_inverseOp and

       A3: G is_distributive_wrt F;

      set e = ( the_unity_wrt F);

      (G . (e,d)) = e by A1, A2, A3, FINSEQOP: 66;

      hence thesis by A1, A3, Th13;

    end;

    theorem :: SETWOP_2:16

    

     Th16: F is commutative associative & F is having_a_unity & H is commutative associative & H is having_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 is having_a_unity and

       A2: H is commutative associative & H is having_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)));

      

       A5: for B9 be Element of ( Fin C), b be Element of C holds X[B9] & not b in B9 implies X[(B9 \/ {.b.})]

      proof

        let B, c such that

         A6: (h . (F $$ (B,f))) = (H $$ (B,(h * f))) and

         A7: not c in B;

        

        thus (h . (F $$ ((B \/ {.c.}),f))) = (h . (F . ((F $$ (B,f)),(f . c)))) by A1, A7, Th2

        .= (H . ((H $$ (B,(h * f))),(h . (f . c)))) by A4, A6

        .= (H . ((H $$ (B,(h * f))),((h * f) . c))) by FUNCT_2: 15

        .= (H $$ ((B \/ {.c.}),(h * f))) by A2, A7, Th2;

      end;

      (h . (F $$ (( {}. C),f))) = ( the_unity_wrt H) by A1, A3, SETWISEO: 31

      .= (H $$ (( {}. C),(h * f))) by A2, SETWISEO: 31;

      then

       A8: X[( {}. C)];

      for B holds X[B] from SETWISEO:sch 2( A8, A5);

      hence thesis;

    end;

    theorem :: SETWOP_2:17

    F is commutative associative & F is having_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))) by Th16;

    theorem :: SETWOP_2:18

    F is commutative associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F implies ((G [;] (d,( id D))) . (F $$ (B,f))) = (F $$ (B,((G [;] (d,( id D))) * f)))

    proof

      assume that

       A1: F is commutative associative & F is having_a_unity and

       A2: F is having_an_inverseOp and

       A3: G is_distributive_wrt F;

      set e = ( the_unity_wrt F);

      set u = (G [;] (d,( id D)));

      u is_distributive_wrt F by A3, FINSEQOP: 54;

      then

       A4: for d1, d2 holds (u . (F . (d1,d2))) = (F . ((u . d1),(u . d2)));

      ((G [;] (d,( id D))) . e) = e by A1, A2, A3, FINSEQOP: 69;

      hence thesis by A1, A4, Th16;

    end;

    theorem :: SETWOP_2:19

    F is commutative associative & F is having_a_unity & F is having_an_inverseOp implies (( the_inverseOp_wrt F) . (F $$ (B,f))) = (F $$ (B,(( the_inverseOp_wrt F) * f)))

    proof

      assume that

       A1: F is commutative associative & F is having_a_unity and

       A2: F is having_an_inverseOp;

      set e = ( the_unity_wrt F), u = ( the_inverseOp_wrt F);

      u is_distributive_wrt F by A1, A2, FINSEQOP: 63;

      then

       A3: for d1, d2 holds (u . (F . (d1,d2))) = (F . ((u . d1),(u . d2)));

      (u . e) = e by A1, A2, FINSEQOP: 61;

      hence thesis by A1, A3, Th16;

    end;

    definition

      let D, p, d;

      :: SETWOP_2:def1

      func [#] (p,d) -> sequence of D equals (( NAT --> d) +* p);

      coherence ;

    end

    theorem :: SETWOP_2:20

    

     Th20: (i in ( dom p) implies (( [#] (p,d)) . i) = (p . i)) & ( not i in ( dom p) implies (( [#] (p,d)) . i) = d)

    proof

      thus i in ( dom p) implies (( [#] (p,d)) . i) = (p . i) by FUNCT_4: 13;

      

       A1: i in NAT by ORDINAL1:def 12;

      assume not i in ( dom p);

      

      hence (( [#] (p,d)) . i) = (( NAT --> d) . i) by FUNCT_4: 11

      .= d by A1, FUNCOP_1: 7;

    end;

    theorem :: SETWOP_2:21

    (( [#] (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) by RELAT_1: 62;

      

       A2: ( dom p) = ( Seg k) by FINSEQ_1:def 3;

      now

        let x be object;

        assume

         A3: x in ( Seg k);

        then ((f | ( Seg k)) . x) = (f . x) by A1, FUNCT_1: 47;

        hence ((f | ( Seg k)) . x) = (p . x) by A2, A3, Th20;

      end;

      hence thesis by A1, A2, FUNCT_1: 2;

    end;

    theorem :: SETWOP_2:22

    (( [#] ((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) by RELAT_1: 62;

      

       A2: ( dom p) = ( Seg k) by FINSEQ_1:def 3;

      now

        let x be object;

        k <= (k + ( len q)) by NAT_1: 12;

        then k <= ( len (p ^ q)) by FINSEQ_1: 22;

        then

         A3: ( Seg ( len (p ^ q))) = ( dom (p ^ q)) & ( Seg k) c= ( Seg ( len (p ^ q))) by FINSEQ_1: 5, FINSEQ_1:def 3;

        assume

         A4: x in ( Seg k);

        then ((f | ( Seg k)) . x) = (f . x) by A1, FUNCT_1: 47;

        

        hence ((f | ( Seg k)) . x) = ((p ^ q) . x) by A4, A3, Th20

        .= (p . x) by A2, A4, FINSEQ_1:def 7;

      end;

      hence thesis by A1, A2, FUNCT_1: 2;

    end;

    theorem :: SETWOP_2:23

    ( rng ( [#] (p,d))) = (( rng p) \/ {d})

    proof

      now

        let y be object;

        thus y in ( rng ( [#] (p,d))) implies y in (( rng p) \/ {d})

        proof

          assume y in ( rng ( [#] (p,d)));

          then

          consider x be object such that

           A1: x in ( dom ( [#] (p,d))) and

           A2: y = (( [#] (p,d)) . x) by FUNCT_1:def 3;

          reconsider i = x as Element of NAT by A1;

          now

            per cases ;

              case

               A3: i in ( dom p);

              then y = (p . i) by A2, Th20;

              hence y in ( rng p) by A3, FUNCT_1:def 3;

            end;

              case not i in ( dom p);

              then y = d by A2, Th20;

              hence y in {d} by TARSKI:def 1;

            end;

          end;

          hence thesis by XBOOLE_0:def 3;

        end;

        assume

         A4: y in (( rng p) \/ {d});

        now

          per cases by A4, XBOOLE_0:def 3;

            suppose y in ( rng p);

            then

            consider i be Nat such that

             A5: i in ( dom p) and

             A6: y = (p . i) by FINSEQ_2: 10;

            y = (( [#] (p,d)) . i) by A5, A6, Th20;

            hence y in ( rng ( [#] (p,d))) by A5, FUNCT_2: 4;

          end;

            suppose

             A7: y in {d};

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

            then

             A8: not (( len p) + 1) in ( dom p) by Lm2;

            y = d by A7, TARSKI:def 1;

            then y = (( [#] (p,d)) . (( len p) + 1)) by A8, Th20;

            hence y in ( rng ( [#] (p,d))) by FUNCT_2: 4;

          end;

        end;

        hence y in ( rng ( [#] (p,d)));

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: SETWOP_2:24

    (h * ( [#] (p,d))) = ( [#] ((h * p),(h . d)))

    proof

      now

        let i be Element of NAT ;

        

         A1: ( dom (h * p)) = ( Seg ( len (h * p))) by FINSEQ_1:def 3;

        

         A2: ( len (h * p)) = ( len p) & ( Seg ( len p)) = ( dom p) by FINSEQ_1:def 3, FINSEQ_2: 33;

        now

          per cases ;

            suppose

             A3: i in ( dom p);

            

            hence (h . (( [#] (p,d)) . i)) = (h . (p . i)) by Th20

            .= ((h * p) . i) by A3, FUNCT_1: 13

            .= (( [#] ((h * p),(h . d))) . i) by A2, A1, A3, Th20;

          end;

            suppose

             A4: not i in ( dom p);

            

            hence (h . (( [#] (p,d)) . i)) = (h . d) by Th20

            .= (( [#] ((h * p),(h . d))) . i) by A2, A1, A4, Th20;

          end;

        end;

        hence ((h * ( [#] (p,d))) . i) = (( [#] ((h * p),(h . d))) . i) by FUNCT_2: 15;

      end;

      hence thesis by FUNCT_2: 63;

    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: 72;

      

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

      

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

      

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

      now

        let i be Element of NAT ;

        now

          per cases ;

            suppose

             A7: i in ( dom p);

            

            hence (F . ((( [#] (p,e)) . i),(( [#] (q,e)) . i))) = (F . ((p . i),(( [#] (q,e)) . i))) by Th20

            .= (F . ((p . i),(q . i))) by A1, A5, A6, A7, Th20

            .= (r . i) by A3, A5, A4, A7, FUNCOP_1: 22

            .= (( [#] (r,e)) . i) by A3, A5, A4, A7, Th20;

          end;

            suppose

             A8: not i in ( dom p);

            

            hence (F . ((( [#] (p,e)) . i),(( [#] (q,e)) . i))) = (F . (e,(( [#] (q,e)) . i))) by Th20

            .= e by A1, A2, A5, A6, A8, Th20

            .= (( [#] (r,e)) . i) by A3, A5, A4, A8, Th20;

          end;

        end;

        hence ((F .: (( [#] (p,e)),( [#] (q,e)))) . i) = (( [#] (r,e)) . i) by FUNCOP_1: 37;

      end;

      hence thesis by FUNCT_2: 63;

    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: ( dom p) = ( Seg ( len p)) by FINSEQ_1:def 3;

        

         A3: ( len (F [:] (p,d))) = ( len p) & ( dom (F [:] (p,d))) = ( Seg ( len (F [:] (p,d)))) by FINSEQ_1:def 3, FINSEQ_2: 84;

        now

          per cases ;

            suppose

             A4: i in ( dom p);

            

            hence (F . ((( [#] (p,e)) . i),d)) = (F . ((p . i),d)) by Th20

            .= ((F [:] (p,d)) . i) by A3, A2, A4, FUNCOP_1: 27

            .= (( [#] ((F [:] (p,d)),e)) . i) by A3, A2, A4, Th20;

          end;

            suppose

             A5: not i in ( dom p);

            

            hence (F . ((( [#] (p,e)) . i),d)) = (F . (e,d)) by Th20

            .= (( [#] ((F [:] (p,d)),e)) . i) by A1, A3, A2, A5, Th20;

          end;

        end;

        hence ((F [:] (( [#] (p,e)),d)) . i) = (( [#] ((F [:] (p,d)),e)) . i) by FUNCOP_1: 48;

      end;

      hence thesis by FUNCT_2: 63;

    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: ( dom p) = ( Seg ( len p)) by FINSEQ_1:def 3;

        

         A3: ( len (F [;] (d,p))) = ( len p) & ( dom (F [;] (d,p))) = ( Seg ( len (F [;] (d,p)))) by FINSEQ_1:def 3, FINSEQ_2: 78;

        now

          per cases ;

            suppose

             A4: i in ( dom p);

            

            hence (F . (d,(( [#] (p,e)) . i))) = (F . (d,(p . i))) by Th20

            .= ((F [;] (d,p)) . i) by A3, A2, A4, FUNCOP_1: 32

            .= (( [#] ((F [;] (d,p)),e)) . i) by A3, A2, A4, Th20;

          end;

            suppose

             A5: not i in ( dom p);

            

            hence (F . (d,(( [#] (p,e)) . i))) = (F . (d,e)) by Th20

            .= (( [#] ((F [;] (d,p)),e)) . i) by A1, A3, A2, A5, Th20;

          end;

        end;

        hence ((F [;] (d,( [#] (p,e)))) . i) = (( [#] ((F [;] (d,p)),e)) . i) by FUNCOP_1: 53;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    notation

      let i be Nat;

      synonym finSeg i for Seg i;

    end

    definition

      let i be Nat;

      :: original: finSeg

      redefine

      func finSeg i -> Element of ( Fin NAT ) ;

      coherence by Lm1;

    end

    notation

      let D, p, F;

      synonym F $$ p for F "**" p;

    end

    definition

      let D, p, F;

      assume

       A1: (F is having_a_unity or ( len p) >= 1) & F is associative commutative;

      :: original: $$

      redefine

      :: SETWOP_2:def2

      func F $$ p equals

      : Def2: (F $$ (( findom p),( [#] (p,( the_unity_wrt F)))));

      compatibility by A1, FINSOP_1: 3;

    end

    theorem :: SETWOP_2:25

    

     Th25: F is having_a_unity implies (F "**" (i |-> ( the_unity_wrt F))) = ( the_unity_wrt F)

    proof

      set e = ( the_unity_wrt F);

      defpred X[ Nat] means (F "**" ($1 |-> e)) = e;

      assume

       A1: F is having_a_unity;

      

       A2: for i st X[i] holds X[(i + 1)]

      proof

        let i;

        assume

         A3: (F "**" (i |-> e)) = e;

        

        thus (F "**" ((i + 1) |-> e)) = (F "**" ((i |-> e) ^ <*e*>)) by FINSEQ_2: 60

        .= (F . ((F "**" (i |-> e)),e)) by A1, FINSOP_1: 4

        .= e by A1, A3, SETWISEO: 15;

      end;

      (F "**" ( 0 |-> e)) = (F "**" ( <*> D))

      .= e by A1, FINSOP_1: 10;

      then

       A4: X[ 0 ];

      for i holds X[i] from NAT_1:sch 2( A4, A2);

      hence thesis;

    end;

    theorem :: SETWOP_2:26

    

     Th26: F is associative & (i >= 1 & j >= 1 or F is having_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 is having_a_unity;

      then ( len p1) >= 1 & ( len p2) >= 1 or F is having_a_unity by CARD_1:def 7;

      then (F "**" (p1 ^ p2)) = (F . ((F "**" p1),(F "**" p2))) by A1, FINSOP_1: 5;

      hence thesis by FINSEQ_2: 123;

    end;

    theorem :: SETWOP_2:27

    F is commutative associative & (i >= 1 & j >= 1 or F is having_a_unity) implies (F "**" ((i * j) |-> d)) = (F "**" (j |-> (F "**" (i |-> d))))

    proof

      assume that

       A1: F is commutative associative and

       A2: i >= 1 & j >= 1 or F is having_a_unity;

      per cases ;

        suppose

         A3: i = 0 or j = 0 ;

        set e = ( the_unity_wrt F);

         A4:

        now

          per cases by A3;

            suppose i = 0 ;

            then (i |-> d) = ( <*> D);

            then (F "**" (i |-> d)) = e by A2, A3, FINSOP_1: 10;

            hence (F "**" (j |-> (F "**" (i |-> d)))) = e by A2, A3, Th25;

          end;

            suppose j = 0 ;

            then (j |-> (F "**" (i |-> d))) = ( <*> D);

            hence (F "**" (j |-> (F "**" (i |-> d)))) = e by A2, A3, FINSOP_1: 10;

          end;

        end;

        ((i * j) |-> d) = ( <*> D) by A3;

        hence thesis by A2, A3, A4, FINSOP_1: 10;

      end;

        suppose

         A5: i > 0 & j > 0 ;

        defpred X[ Nat] means $1 <> 0 implies (F "**" ((i * $1) |-> d)) = (F "**" ($1 |-> (F "**" (i |-> d))));

        

         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 NAT_1: 14;

              suppose

               A8: j = 0 ;

              (1 |-> (F "**" (i |-> d))) = <*(F "**" (i |-> d))*> by FINSEQ_2: 59;

              hence thesis by A8, FINSOP_1: 11;

            end;

              suppose

               A9: j >= (1 + 0 );

              then j > 0 ;

              then (i * j) > (i * 0 ) by A5, XREAL_1: 68;

              then

               A10: (i * j) >= (1 + 0 ) by NAT_1: 13;

              (F "**" ((i * (j + 1)) |-> d)) = (F "**" (((i * j) + (i * 1)) |-> d))

              .= (F . ((F "**" ((i * j) |-> d)),(F "**" (i |-> d)))) by A1, A2, A10, Th26

              .= (F . ((F "**" ((i * j) |-> d)),(F "**" (1 |-> (F "**" (i |-> d)))))) by FINSOP_1: 16

              .= (F "**" ((j + 1) |-> (F "**" (i |-> d)))) by A1, A7, A9, Th26;

              hence thesis;

            end;

          end;

          hence thesis;

        end;

        

         A11: X[ 0 ];

        for j holds X[j] from NAT_1:sch 2( A11, A6);

        hence thesis by A5;

      end;

    end;

    theorem :: SETWOP_2:28

    

     Th28: F is having_a_unity & H is having_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 is having_a_unity and

       A2: H is having_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));

      

       A5: for q, d st X[q] holds X[(q ^ <*d*>)]

      proof

        let q, d such that

         A6: (h . (F "**" q)) = (H "**" (h * q));

        

        thus (h . (F "**" (q ^ <*d*>))) = (h . (F . ((F "**" q),d))) by A1, FINSOP_1: 4

        .= (H . ((H "**" (h * q)),(h . d))) by A4, A6

        .= (H "**" ((h * q) ^ <*(h . d)*>)) by A2, FINSOP_1: 4

        .= (H "**" (h * (q ^ <*d*>))) by FINSEQOP: 8;

      end;

      (h . (F "**" ( <*> D))) = (h . ( the_unity_wrt F)) by A1, FINSOP_1: 10

      .= (H "**" ( <*> E)) by A2, A3, FINSOP_1: 10

      .= (H "**" (h * ( <*> D)));

      then

       A7: X[( <*> D)];

       X[q] from FINSEQ_2:sch 2( A7, A5);

      hence thesis;

    end;

    theorem :: SETWOP_2:29

    F is having_a_unity & (u . ( the_unity_wrt F)) = ( the_unity_wrt F) & u is_distributive_wrt F implies (u . (F "**" p)) = (F "**" (u * p)) by Th28;

    theorem :: SETWOP_2:30

    F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F implies ((G [;] (d,( id D))) . (F "**" p)) = (F "**" ((G [;] (d,( id D))) * p))

    proof

      assume that

       A1: F is associative and

       A2: F is having_a_unity and

       A3: F is having_an_inverseOp and

       A4: G is_distributive_wrt F;

      set e = ( the_unity_wrt F);

      set u = (G [;] (d,( id D)));

      u is_distributive_wrt F by A4, FINSEQOP: 54;

      then

       A5: for d1, d2 holds (u . (F . (d1,d2))) = (F . ((u . d1),(u . d2)));

      ((G [;] (d,( id D))) . e) = e by A1, A2, A3, A4, FINSEQOP: 69;

      hence thesis by A2, A5, Th28;

    end;

    theorem :: SETWOP_2:31

    F is commutative associative & F is having_a_unity & F is having_an_inverseOp implies (( the_inverseOp_wrt F) . (F "**" p)) = (F "**" (( the_inverseOp_wrt F) * p))

    proof

      assume that

       A1: F is commutative associative and

       A2: F is having_a_unity and

       A3: F is having_an_inverseOp;

      set e = ( the_unity_wrt F), u = ( the_inverseOp_wrt F);

      u is_distributive_wrt F by A1, A2, A3, FINSEQOP: 63;

      then

       A4: for d1, d2 holds (u . (F . (d1,d2))) = (F . ((u . d1),(u . d2)));

      (u . e) = e by A1, A2, A3, FINSEQOP: 61;

      hence thesis by A2, A4, Th28;

    end;

    theorem :: SETWOP_2:32

    

     Th32: F is commutative associative & F is having_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 & F is having_a_unity & e = ( the_unity_wrt F) and

       A2: (G . (e,e)) = e and

       A3: (F . ((G . (d1,d2)),(G . (d3,d4)))) = (G . ((F . (d1,d3)),(F . (d2,d4)))) and

       A4: ( len p) = ( len q);

      

       A5: ( len p) = ( len (G .: (p,q))) by A4, FINSEQ_2: 72;

      

       A6: ( dom (G .: (p,q))) = ( Seg ( len (G .: (p,q)))) by FINSEQ_1:def 3;

      

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

      

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

      

      thus (G . ((F "**" p),(F "**" q))) = (G . ((F $$ (( findom p),( [#] (p,e)))),(F "**" q))) by A1, Def2

      .= (G . ((F $$ (( findom p),( [#] (p,e)))),(F $$ (( findom q),( [#] (q,e)))))) by A1, Def2

      .= (F $$ (( findom p),(G .: (( [#] (p,e)),( [#] (q,e)))))) by A1, A2, A3, A4, A8, A7, Th9

      .= (F $$ (( findom (G .: (p,q))),( [#] ((G .: (p,q)),e)))) by A2, A4, A5, A8, A6, Lm4

      .= (F "**" (G .: (p,q))) by A1, Def2;

    end;

    theorem :: SETWOP_2:33

    

     Th33: F is commutative associative & F is having_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 CARD_1:def 7;

      hence thesis by Th32;

    end;

    theorem :: SETWOP_2:34

    

     Th34: F is commutative associative & F is having_a_unity & ( len p) = ( len q) implies (F . ((F "**" p),(F "**" q))) = (F "**" (F .: (p,q)))

    proof

      set e = ( the_unity_wrt F);

      assume

       A1: F is commutative & F is associative & F is having_a_unity;

      then (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 Lm3, SETWISEO: 15;

      hence thesis by A1, Th32;

    end;

    theorem :: SETWOP_2:35

    

     Th35: F is commutative associative & F is having_a_unity implies (F . ((F "**" T1),(F "**" T2))) = (F "**" (F .: (T1,T2)))

    proof

      ( len T1) = i & ( len T2) = i by CARD_1:def 7;

      hence thesis by Th34;

    end;

    theorem :: SETWOP_2:36

    F is commutative associative & F is having_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);

      (i |-> (F . (d1,d2))) = (F .: (T1,T2)) by FINSEQOP: 17;

      hence thesis by Th35;

    end;

    theorem :: SETWOP_2:37

    F is commutative associative & F is having_a_unity & F is having_an_inverseOp & G = (F * (( id D),( the_inverseOp_wrt F))) implies (G . ((F "**" T1),(F "**" T2))) = (F "**" (G .: (T1,T2)))

    proof

      assume that

       A1: F is commutative associative & F is having_a_unity and

       A2: F is having_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, A2, FINSEQOP: 86, FINSEQOP: 89;

      hence thesis by A1, Th33;

    end;

    theorem :: SETWOP_2:38

    

     Th38: F is commutative associative & F is having_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 is having_a_unity & e = ( the_unity_wrt F) and

       A2: G is_distributive_wrt F and

       A3: (G . (d,e)) = e;

      

       A4: ( len p) = ( len (G [;] (d,p))) & ( Seg ( len p)) = ( dom p) by FINSEQ_1:def 3, FINSEQ_2: 78;

      

       A5: ( Seg ( len (G [;] (d,p)))) = ( dom (G [;] (d,p))) by FINSEQ_1:def 3;

      

      thus (G . (d,(F "**" p))) = (G . (d,(F $$ (( findom p),( [#] (p,e)))))) by A1, Def2

      .= (F $$ (( findom p),(G [;] (d,( [#] (p,e)))))) by A1, A2, A3, Th12

      .= (F $$ (( findom p),( [#] ((G [;] (d,p)),e)))) by A3, Lm6

      .= (F "**" (G [;] (d,p))) by A1, A4, A5, Def2;

    end;

    theorem :: SETWOP_2:39

    

     Th39: F is commutative associative & F is having_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 is having_a_unity & e = ( the_unity_wrt F) and

       A2: G is_distributive_wrt F and

       A3: (G . (e,d)) = e;

      

       A4: ( len p) = ( len (G [:] (p,d))) & ( Seg ( len p)) = ( dom p) by FINSEQ_1:def 3, FINSEQ_2: 84;

      

       A5: ( Seg ( len (G [:] (p,d)))) = ( dom (G [:] (p,d))) by FINSEQ_1:def 3;

      

      thus (G . ((F "**" p),d)) = (G . ((F $$ (( findom p),( [#] (p,e)))),d)) by A1, Def2

      .= (F $$ (( findom p),(G [:] (( [#] (p,e)),d)))) by A1, A2, A3, Th13

      .= (F $$ (( findom p),( [#] ((G [:] (p,d)),e)))) by A3, Lm5

      .= (F "**" (G [:] (p,d))) by A1, A4, A5, Def2;

    end;

    theorem :: SETWOP_2:40

    F is commutative associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F implies (G . (d,(F "**" p))) = (F "**" (G [;] (d,p)))

    proof

      assume that

       A1: F is commutative associative & F is having_a_unity and

       A2: F is having_an_inverseOp and

       A3: G is_distributive_wrt F;

      set e = ( the_unity_wrt F);

      (G . (d,e)) = e by A1, A2, A3, FINSEQOP: 66;

      hence thesis by A1, A3, Th38;

    end;

    theorem :: SETWOP_2:41

    F is commutative associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F implies (G . ((F "**" p),d)) = (F "**" (G [:] (p,d)))

    proof

      assume that

       A1: F is commutative associative & F is having_a_unity and

       A2: F is having_an_inverseOp and

       A3: G is_distributive_wrt F;

      set e = ( the_unity_wrt F);

      (G . (e,d)) = e by A1, A2, A3, FINSEQOP: 66;

      hence thesis by A1, A3, Th39;

    end;