binom.miz



    begin

    registration

      cluster Abelian right_add-cancelable -> left_add-cancelable for non empty addLoopStr;

      coherence

      proof

        let R be non empty addLoopStr;

        assume R is Abelian right_add-cancelable;

        then

        reconsider R as Abelian right_add-cancelable non empty addLoopStr;

        R is left_add-cancelable

        proof

          let a,b,c be Element of R;

          assume (a + b) = (a + c);

          hence thesis by ALGSTR_0:def 4;

        end;

        hence thesis;

      end;

      cluster Abelian left_add-cancelable -> right_add-cancelable for non empty addLoopStr;

      coherence

      proof

        let R be non empty addLoopStr;

        assume R is Abelian left_add-cancelable;

        then

        reconsider R as Abelian left_add-cancelable non empty addLoopStr;

        R is right_add-cancelable

        proof

          let a,b,c be Element of R;

          assume (b + a) = (c + a);

          hence thesis by ALGSTR_0:def 3;

        end;

        hence thesis;

      end;

    end

    registration

      cluster right_zeroed right_complementable add-associative -> right_add-cancelable for non empty addLoopStr;

      coherence ;

    end

    registration

      cluster Abelian add-associative left_zeroed right_zeroed commutative associative add-cancelable distributive unital for non empty doubleLoopStr;

      existence

      proof

        set R = the comRing;

        take R;

        thus thesis;

      end;

    end

    theorem :: BINOM:1

    

     Th1: for R be right_zeroed left_add-cancelable left-distributive non empty doubleLoopStr, a be Element of R holds (( 0. R) * a) = ( 0. R)

    proof

      let R be right_zeroed left_add-cancelable left-distributive non empty doubleLoopStr, a be Element of R;

      (( 0. R) * a) = ((( 0. R) + ( 0. R)) * a) by RLVECT_1:def 4

      .= ((( 0. R) * a) + (( 0. R) * a)) by VECTSP_1:def 3;

      then ((( 0. R) * a) + (( 0. R) * a)) = ((( 0. R) * a) + ( 0. R)) by RLVECT_1:def 4;

      hence thesis by ALGSTR_0:def 3;

    end;

    theorem :: BINOM:2

    

     Th2: for R be left_zeroed right_add-cancelable right-distributive non empty doubleLoopStr, a be Element of R holds (a * ( 0. R)) = ( 0. R)

    proof

      let R be left_zeroed right_add-cancelable right-distributive non empty doubleLoopStr, a be Element of R;

      (a * ( 0. R)) = (a * (( 0. R) + ( 0. R))) by ALGSTR_1:def 2

      .= ((a * ( 0. R)) + (a * ( 0. R))) by VECTSP_1:def 2;

      then ((a * ( 0. R)) + (a * ( 0. R))) = (( 0. R) + (a * ( 0. R))) by ALGSTR_1:def 2;

      hence thesis by ALGSTR_0:def 4;

    end;

     Lm1:

    now

      let C,D be non empty set, b be Element of D, F be Function of [:C, D:], D;

      thus ex g be Function of [: NAT , C:], D st for a be Element of C holds (g . ( 0 ,a)) = b & for n be Nat holds (g . ((n + 1),a)) = (F . (a,(g . (n,a))))

      proof

        

         A1: for a be Element of C holds ex f be sequence of D st (f . 0 ) = b & for n be Nat holds (f . (n + 1)) = (F . (a,(f . n)))

        proof

          let a be Element of C;

          defpred P[ Nat, Element of D, Element of D] means $3 = (F . (a,$2));

          

           A2: for n be Nat holds for x be Element of D holds ex y be Element of D st P[n, x, y];

          ex f be sequence of D st (f . 0 ) = b & for n be Nat holds P[n, (f . n), (f . (n + 1))] from RECDEF_1:sch 2( A2);

          hence thesis;

        end;

        ex g be Function of C, ( Funcs ( NAT ,D)) st for a be Element of C holds ex f be sequence of D st (g . a) = f & (f . 0 ) = b & for n be Nat holds (f . (n + 1)) = (F . (a,(f . n)))

        proof

          set h = { [a, l] where a be Element of C, l be Element of ( Funcs ( NAT ,D)) : ex f be sequence of D st f = l & (f . 0 ) = b & for n be Nat holds (f . (n + 1)) = (F . (a,(f . n))) };

           A3:

          now

            let x,y1,y2 be object;

            assume that

             A4: [x, y1] in h and

             A5: [x, y2] in h;

            consider a1 be Element of C, l1 be Element of ( Funcs ( NAT ,D)) such that

             A6: [x, y1] = [a1, l1] and

             A7: ex f be sequence of D st f = l1 & (f . 0 ) = b & for n be Nat holds (f . (n + 1)) = (F . (a1,(f . n))) by A4;

            consider a2 be Element of C, l2 be Element of ( Funcs ( NAT ,D)) such that

             A8: [x, y2] = [a2, l2] and

             A9: ex f be sequence of D st f = l2 & (f . 0 ) = b & for n be Nat holds (f . (n + 1)) = (F . (a2,(f . n))) by A5;

            consider f1 be sequence of D such that

             A10: f1 = l1 and

             A11: (f1 . 0 ) = b and

             A12: for n be Nat holds (f1 . (n + 1)) = (F . (a1,(f1 . n))) by A7;

            consider f2 be sequence of D such that

             A13: f2 = l2 and

             A14: (f2 . 0 ) = b and

             A15: for n be Nat holds (f2 . (n + 1)) = (F . (a2,(f2 . n))) by A9;

            

             A16: a1 = ( [a1, l1] `1 )

            .= ( [x, y1] `1 ) by A6

            .= x

            .= ( [x, y2] `1 )

            .= ( [a2, l2] `1 ) by A8

            .= a2;

             A17:

            now

              defpred P[ Nat] means (f1 . $1) = (f2 . $1);

              let x be object;

              assume x in NAT ;

              then

              reconsider x9 = x as Element of NAT ;

               A18:

              now

                let n be Nat;

                assume

                 A19: P[n];

                (f1 . (n + 1)) = (F . (a2,(f1 . n))) by A12, A16

                .= (f2 . (n + 1)) by A15, A19;

                hence P[(n + 1)];

              end;

              

               A20: P[ 0 ] by A11, A14;

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

              

              hence (f1 . x) = (f2 . x9)

              .= (f2 . x);

            end;

            

             A21: NAT = ( dom f1) & NAT = ( dom f2) by FUNCT_2:def 1;

            

            thus y1 = ( [x, y1] `2 )

            .= ( [a1, l1] `2 ) by A6

            .= l1

            .= l2 by A10, A13, A21, A17, FUNCT_1: 2

            .= ( [a2, l2] `2 )

            .= ( [x, y2] `2 ) by A8

            .= y2;

          end;

          now

            let x be object;

            assume x in h;

            then ex a be Element of C, l be Element of ( Funcs ( NAT ,D)) st x = [a, l] & ex f be sequence of D st f = l & (f . 0 ) = b & for n be Nat holds (f . (n + 1)) = (F . (a,(f . n)));

            hence x in [:C, ( Funcs ( NAT ,D)):] by ZFMISC_1:def 2;

          end;

          then

          reconsider h as Relation of C, ( Funcs ( NAT ,D)) by TARSKI:def 3;

          

           A22: for x be object holds x in C implies x in ( dom h)

          proof

            let x be object;

            assume

             A23: x in C;

            then

            consider f be sequence of D such that

             A24: (f . 0 ) = b & for n be Nat holds (f . (n + 1)) = (F . (x,(f . n))) by A1;

            f in ( Funcs ( NAT ,D)) by FUNCT_2: 8;

            then [x, f] in h by A23, A24;

            hence thesis by XTUPLE_0:def 12;

          end;

          for x be object holds x in ( dom h) implies x in C;

          then ( dom h) = C by A22, TARSKI: 2;

          then

          reconsider h as Function of C, ( Funcs ( NAT ,D)) by A3, FUNCT_1:def 1, FUNCT_2:def 1;

          take h;

          for a be Element of C holds ex f be sequence of D st (h . a) = f & (f . 0 ) = b & for n be Nat holds (f . (n + 1)) = (F . (a,(f . n)))

          proof

            let a be Element of C;

            ( dom h) = C by FUNCT_2:def 1;

            then [a, (h . a)] in h by FUNCT_1: 1;

            then

            consider a9 be Element of C, l be Element of ( Funcs ( NAT ,D)) such that

             A25: [a, (h . a)] = [a9, l] and

             A26: ex f9 be sequence of D st f9 = l & (f9 . 0 ) = b & for n be Nat holds (f9 . (n + 1)) = (F . (a9,(f9 . n)));

            

             A27: (h . a) = ( [a, (h . a)] `2 )

            .= ( [a9, l] `2 ) by A25

            .= l;

            a = ( [a, (h . a)] `1 )

            .= ( [a9, l] `1 ) by A25

            .= a9;

            hence thesis by A26, A27;

          end;

          hence thesis;

        end;

        then

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

         A28: for a be Element of C holds ex f be sequence of D st (g . a) = f & (f . 0 ) = b & for n be Nat holds (f . (n + 1)) = (F . (a,(f . n)));

        set h = { [ [n, a], z] where n be Element of NAT , a be Element of C, z be Element of D : ex f be sequence of D st f = (g . a) & z = (f . n) };

         A29:

        now

          let x,y1,y2 be object;

          assume that

           A30: [x, y1] in h and

           A31: [x, y2] in h;

          consider n1 be Element of NAT , a1 be Element of C, z1 be Element of D such that

           A32: [x, y1] = [ [n1, a1], z1] and

           A33: ex f1 be sequence of D st f1 = (g . a1) & z1 = (f1 . n1) by A30;

          consider n2 be Element of NAT , a2 be Element of C, z2 be Element of D such that

           A34: [x, y2] = [ [n2, a2], z2] and

           A35: ex f2 be sequence of D st f2 = (g . a2) & z2 = (f2 . n2) by A31;

          

           A36: [n1, a1] = ( [ [n1, a1], z1] `1 )

          .= ( [x, y1] `1 ) by A32

          .= x

          .= ( [x, y2] `1 )

          .= ( [ [n2, a2], z2] `1 ) by A34

          .= [n2, a2];

          

           A37: a1 = ( [n1, a1] `2 )

          .= ( [n2, a2] `2 ) by A36

          .= a2;

          

           A38: n1 = ( [n1, a1] `1 )

          .= ( [n2, a2] `1 ) by A36

          .= n2;

          

          thus y1 = ( [x, y1] `2 )

          .= ( [x, y2] `2 ) by A32, A33, A34, A35, A37, A38

          .= y2;

        end;

        now

          let x be object;

          assume x in h;

          then

          consider n1 be Element of NAT , a1 be Element of C, z1 be Element of D such that

           A39: x = [ [n1, a1], z1] and ex f1 be sequence of D st f1 = (g . a1) & z1 = (f1 . n1);

           [n1, a1] in [: NAT , C:] by ZFMISC_1:def 2;

          hence x in [: [: NAT , C:], D:] by A39, ZFMISC_1:def 2;

        end;

        then

        reconsider h as Relation of [: NAT , C:], D by TARSKI:def 3;

        

         A40: for x be object holds x in [: NAT , C:] implies x in ( dom h)

        proof

          let x be object;

          assume x in [: NAT , C:];

          then

          consider n,d be object such that

           A41: n in NAT and

           A42: d in C and

           A43: x = [n, d] by ZFMISC_1:def 2;

          reconsider d as Element of C by A42;

          reconsider n as Element of NAT by A41;

          consider f9 be sequence of D such that

           A44: (g . d) = f9 and (f9 . 0 ) = b and for n be Nat holds (f9 . (n + 1)) = (F . (d,(f9 . n))) by A28;

          ex z be Element of D st ex f be sequence of D st f = (g . d) & z = (f . n)

          proof

            take (f9 . n);

            take f9;

            thus thesis by A44;

          end;

          then

          consider z be Element of D such that

           A45: ex f be sequence of D st f = (g . d) & z = (f . n);

           [x, z] in h by A43, A45;

          hence thesis by XTUPLE_0:def 12;

        end;

        for x be object holds x in ( dom h) implies x in [: NAT , C:];

        then ( dom h) = [: NAT , C:] by A40, TARSKI: 2;

        then

        reconsider h as Function of [: NAT , C:], D by A29, FUNCT_1:def 1, FUNCT_2:def 1;

        take h;

        for a be Element of C holds (h . ( 0 ,a)) = b & for n be Nat holds (h . ((n + 1),a)) = (F . (a,(h . (n,a))))

        proof

          let a be Element of C;

          consider f9 be sequence of D such that

           A46: (g . a) = f9 and

           A47: (f9 . 0 ) = b and

           A48: for n be Nat holds (f9 . (n + 1)) = (F . (a,(f9 . n))) by A28;

           A49:

          now

            let k be Nat;

             [(k + 1), a] in [: NAT , C:] by ZFMISC_1:def 2;

            then [(k + 1), a] in ( dom h) by FUNCT_2:def 1;

            then

            consider u be object such that

             A50: [ [(k + 1), a], u] in h by XTUPLE_0:def 12;

            k in NAT by ORDINAL1:def 12;

            then [k, a] in [: NAT , C:] by ZFMISC_1:def 2;

            then [k, a] in ( dom h) by FUNCT_2:def 1;

            then

            consider v be object such that

             A51: [ [k, a], v] in h by XTUPLE_0:def 12;

            consider n be Element of NAT , d be Element of C, z be Element of D such that

             A52: [ [(k + 1), a], u] = [ [n, d], z] and

             A53: ex f1 be sequence of D st f1 = (g . d) & z = (f1 . n) by A50;

            

             A54: u = ( [ [(k + 1), a], u] `2 )

            .= ( [ [n, d], z] `2 ) by A52

            .= z;

            consider n1 be Element of NAT , d1 be Element of C, z1 be Element of D such that

             A55: [ [k, a], v] = [ [n1, d1], z1] and

             A56: ex f2 be sequence of D st f2 = (g . d1) & z1 = (f2 . n1) by A51;

            

             A57: v = ( [ [k, a], v] `2 )

            .= ( [ [n1, d1], z1] `2 ) by A55

            .= z1;

            

             A58: [(k + 1), a] = ( [ [(k + 1), a], u] `1 )

            .= ( [ [n, d], z] `1 ) by A52

            .= [n, d];

            

             A59: d = ( [n, d] `2 )

            .= ( [(k + 1), a] `2 ) by A58

            .= a;

            

             A60: [k, a] = ( [ [k, a], v] `1 )

            .= ( [ [n1, d1], z1] `1 ) by A55

            .= [n1, d1];

            

             A61: n1 = ( [n1, d1] `1 )

            .= ( [k, a] `1 ) by A60

            .= k;

            

             A62: d1 = ( [n1, d1] `2 )

            .= ( [k, a] `2 ) by A60

            .= a;

            n = ( [n, d] `1 )

            .= ( [(k + 1), a] `1 ) by A58

            .= (k + 1);

            

            hence (h . ((k + 1),a)) = (f9 . (k + 1)) by A46, A50, A53, A54, A59, FUNCT_1: 1

            .= (F . (a,z1)) by A46, A48, A56, A61, A62

            .= (F . (a,(h . (k,a)))) by A51, A57, FUNCT_1: 1;

          end;

           [ 0 , a] in [: NAT , C:] by ZFMISC_1:def 2;

          then [ 0 , a] in ( dom h) by FUNCT_2:def 1;

          then

          consider u be object such that

           A63: [ [ 0 , a], u] in h by XTUPLE_0:def 12;

          consider n be Element of NAT , d be Element of C, z be Element of D such that

           A64: [ [ 0 , a], u] = [ [n, d], z] and

           A65: ex f1 be sequence of D st f1 = (g . d) & z = (f1 . n) by A63;

          

           A66: u = ( [ [ 0 , a], u] `2 )

          .= ( [ [n, d], z] `2 ) by A64

          .= z;

          

           A67: [ 0 , a] = ( [ [ 0 , a], u] `1 )

          .= ( [ [n, d], z] `1 ) by A64

          .= [n, d];

          

           A68: d = ( [n, d] `2 )

          .= ( [ 0 , a] `2 ) by A67

          .= a;

          n = ( [n, d] `1 )

          .= ( [ 0 , a] `1 ) by A67

          .= 0 ;

          hence thesis by A46, A47, A63, A65, A66, A68, A49, FUNCT_1: 1;

        end;

        hence thesis;

      end;

    end;

     Lm2:

    now

      let C,D be non empty set, b be Element of D, F be Function of [:D, C:], D;

      thus ex g be Function of [:C, NAT :], D st for a be Element of C holds (g . (a, 0 )) = b & for n be Element of NAT holds (g . (a,(n + 1))) = (F . ((g . (a,n)),a))

      proof

        

         A1: for a be Element of C holds ex f be sequence of D st (f . 0 ) = b & for n be Nat holds (f . (n + 1)) = (F . ((f . n),a))

        proof

          let a be Element of C;

          defpred P[ Nat, Element of D, Element of D] means $3 = (F . ($2,a));

          

           A2: for n be Nat holds for x be Element of D holds ex y be Element of D st P[n, x, y];

          ex f be sequence of D st (f . 0 ) = b & for n be Nat holds P[n, (f . n), (f . (n + 1))] from RECDEF_1:sch 2( A2);

          hence thesis;

        end;

        ex g be Function of C, ( Funcs ( NAT ,D)) st for a be Element of C holds ex f be sequence of D st (g . a) = f & (f . 0 ) = b & for n be Nat holds (f . (n + 1)) = (F . ((f . n),a))

        proof

          set h = { [a, l] where a be Element of C, l be Element of ( Funcs ( NAT ,D)) : ex f be sequence of D st f = l & (f . 0 ) = b & for n be Nat holds (f . (n + 1)) = (F . ((f . n),a)) };

           A3:

          now

            let x,y1,y2 be object;

            assume that

             A4: [x, y1] in h and

             A5: [x, y2] in h;

            consider a1 be Element of C, l1 be Element of ( Funcs ( NAT ,D)) such that

             A6: [x, y1] = [a1, l1] and

             A7: ex f be sequence of D st f = l1 & (f . 0 ) = b & for n be Nat holds (f . (n + 1)) = (F . ((f . n),a1)) by A4;

            consider a2 be Element of C, l2 be Element of ( Funcs ( NAT ,D)) such that

             A8: [x, y2] = [a2, l2] and

             A9: ex f be sequence of D st f = l2 & (f . 0 ) = b & for n be Nat holds (f . (n + 1)) = (F . ((f . n),a2)) by A5;

            consider f1 be sequence of D such that

             A10: f1 = l1 and

             A11: (f1 . 0 ) = b and

             A12: for n be Nat holds (f1 . (n + 1)) = (F . ((f1 . n),a1)) by A7;

            consider f2 be sequence of D such that

             A13: f2 = l2 and

             A14: (f2 . 0 ) = b and

             A15: for n be Nat holds (f2 . (n + 1)) = (F . ((f2 . n),a2)) by A9;

            

             A16: a1 = ( [a1, l1] `1 )

            .= ( [x, y1] `1 ) by A6

            .= x

            .= ( [x, y2] `1 )

            .= ( [a2, l2] `1 ) by A8

            .= a2;

             A17:

            now

              defpred P[ Nat] means (f1 . $1) = (f2 . $1);

              let x be object;

              assume x in NAT ;

              then

              reconsider x9 = x as Element of NAT ;

               A18:

              now

                let n be Nat;

                assume

                 A19: P[n];

                (f1 . (n + 1)) = (F . ((f1 . n),a2)) by A12, A16

                .= (f2 . (n + 1)) by A15, A19;

                hence P[(n + 1)];

              end;

              

               A20: P[ 0 ] by A11, A14;

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

              

              hence (f1 . x) = (f2 . x9)

              .= (f2 . x);

            end;

            

             A21: NAT = ( dom f1) & NAT = ( dom f2) by FUNCT_2:def 1;

            

            thus y1 = ( [x, y1] `2 )

            .= ( [a1, l1] `2 ) by A6

            .= l1

            .= l2 by A10, A13, A21, A17, FUNCT_1: 2

            .= ( [a2, l2] `2 )

            .= ( [x, y2] `2 ) by A8

            .= y2;

          end;

          now

            let x be object;

            assume x in h;

            then ex a be Element of C, l be Element of ( Funcs ( NAT ,D)) st x = [a, l] & ex f be sequence of D st f = l & (f . 0 ) = b & for n be Nat holds (f . (n + 1)) = (F . ((f . n),a));

            hence x in [:C, ( Funcs ( NAT ,D)):] by ZFMISC_1:def 2;

          end;

          then

          reconsider h as Relation of C, ( Funcs ( NAT ,D)) by TARSKI:def 3;

          

           A22: for x be object holds x in C implies x in ( dom h)

          proof

            let x be object;

            assume

             A23: x in C;

            then

            consider f be sequence of D such that

             A24: (f . 0 ) = b & for n be Nat holds (f . (n + 1)) = (F . ((f . n),x)) by A1;

            reconsider f9 = f as Element of ( Funcs ( NAT ,D)) by FUNCT_2: 8;

            f in ( Funcs ( NAT ,D)) by FUNCT_2: 8;

            then [x, f] in h by A23, A24;

            hence thesis by XTUPLE_0:def 12;

          end;

          for x be object holds x in ( dom h) implies x in C;

          then ( dom h) = C by A22, TARSKI: 2;

          then

          reconsider h as Function of C, ( Funcs ( NAT ,D)) by A3, FUNCT_1:def 1, FUNCT_2:def 1;

          take h;

          for a be Element of C holds ex f be sequence of D st (h . a) = f & (f . 0 ) = b & for n be Nat holds (f . (n + 1)) = (F . ((f . n),a))

          proof

            let a be Element of C;

            ( dom h) = C by FUNCT_2:def 1;

            then [a, (h . a)] in h by FUNCT_1: 1;

            then

            consider a9 be Element of C, l be Element of ( Funcs ( NAT ,D)) such that

             A25: [a, (h . a)] = [a9, l] and

             A26: ex f9 be sequence of D st f9 = l & (f9 . 0 ) = b & for n be Nat holds (f9 . (n + 1)) = (F . ((f9 . n),a9));

            

             A27: (h . a) = ( [a, (h . a)] `2 )

            .= ( [a9, l] `2 ) by A25

            .= l;

            a = ( [a, (h . a)] `1 )

            .= ( [a9, l] `1 ) by A25

            .= a9;

            hence thesis by A26, A27;

          end;

          hence thesis;

        end;

        then

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

         A28: for a be Element of C holds ex f be sequence of D st (g . a) = f & (f . 0 ) = b & for n be Nat holds (f . (n + 1)) = (F . ((f . n),a));

        set h = { [ [a, n], z] where n be Element of NAT , a be Element of C, z be Element of D : ex f be sequence of D st f = (g . a) & z = (f . n) };

         A29:

        now

          let x,y1,y2 be object;

          assume that

           A30: [x, y1] in h and

           A31: [x, y2] in h;

          consider n1 be Element of NAT , a1 be Element of C, z1 be Element of D such that

           A32: [x, y1] = [ [a1, n1], z1] and

           A33: ex f1 be sequence of D st f1 = (g . a1) & z1 = (f1 . n1) by A30;

          consider n2 be Element of NAT , a2 be Element of C, z2 be Element of D such that

           A34: [x, y2] = [ [a2, n2], z2] and

           A35: ex f2 be sequence of D st f2 = (g . a2) & z2 = (f2 . n2) by A31;

          

           A36: [a1, n1] = ( [ [a1, n1], z1] `1 )

          .= ( [x, y1] `1 ) by A32

          .= x

          .= ( [x, y2] `1 )

          .= ( [ [a2, n2], z2] `1 ) by A34

          .= [a2, n2];

          

           A37: n1 = ( [a1, n1] `2 )

          .= ( [a2, n2] `2 ) by A36

          .= n2;

          

           A38: a1 = ( [a1, n1] `1 )

          .= ( [a2, n2] `1 ) by A36

          .= a2;

          

          thus y1 = ( [x, y1] `2 )

          .= ( [x, y2] `2 ) by A32, A33, A34, A35, A37, A38

          .= y2;

        end;

        now

          let x be object;

          assume x in h;

          then

          consider n1 be Element of NAT , a1 be Element of C, z1 be Element of D such that

           A39: x = [ [a1, n1], z1] and ex f1 be sequence of D st f1 = (g . a1) & z1 = (f1 . n1);

           [a1, n1] in [:C, NAT :] by ZFMISC_1:def 2;

          hence x in [: [:C, NAT :], D:] by A39, ZFMISC_1:def 2;

        end;

        then

        reconsider h as Relation of [:C, NAT :], D by TARSKI:def 3;

        

         A40: for x be object holds x in [:C, NAT :] implies x in ( dom h)

        proof

          let x be object;

          assume x in [:C, NAT :];

          then

          consider d,n be object such that

           A41: d in C and

           A42: n in NAT and

           A43: x = [d, n] by ZFMISC_1:def 2;

          reconsider d as Element of C by A41;

          reconsider n as Element of NAT by A42;

          consider f9 be sequence of D such that

           A44: (g . d) = f9 and (f9 . 0 ) = b and for n be Nat holds (f9 . (n + 1)) = (F . ((f9 . n),d)) by A28;

          ex z be Element of D st ex f be sequence of D st f = (g . d) & z = (f . n)

          proof

            take (f9 . n);

            take f9;

            thus thesis by A44;

          end;

          then

          consider z be Element of D such that

           A45: ex f be sequence of D st f = (g . d) & z = (f . n);

           [x, z] in h by A43, A45;

          hence thesis by XTUPLE_0:def 12;

        end;

        for x be object holds x in ( dom h) implies x in [:C, NAT :];

        then ( dom h) = [:C, NAT :] by A40, TARSKI: 2;

        then

        reconsider h as Function of [:C, NAT :], D by A29, FUNCT_1:def 1, FUNCT_2:def 1;

        take h;

        for a be Element of C holds (h . (a, 0 )) = b & for n be Element of NAT holds (h . (a,(n + 1))) = (F . ((h . (a,n)),a))

        proof

          let a be Element of C;

          consider f9 be sequence of D such that

           A46: (g . a) = f9 and

           A47: (f9 . 0 ) = b and

           A48: for n be Nat holds (f9 . (n + 1)) = (F . ((f9 . n),a)) by A28;

           A49:

          now

            let k be Element of NAT ;

             [a, (k + 1)] in [:C, NAT :] by ZFMISC_1:def 2;

            then [a, (k + 1)] in ( dom h) by FUNCT_2:def 1;

            then

            consider u be object such that

             A50: [ [a, (k + 1)], u] in h by XTUPLE_0:def 12;

             [a, k] in [:C, NAT :] by ZFMISC_1:def 2;

            then [a, k] in ( dom h) by FUNCT_2:def 1;

            then

            consider v be object such that

             A51: [ [a, k], v] in h by XTUPLE_0:def 12;

            consider n1 be Element of NAT , d1 be Element of C, z1 be Element of D such that

             A52: [ [a, k], v] = [ [d1, n1], z1] and

             A53: ex f2 be sequence of D st f2 = (g . d1) & z1 = (f2 . n1) by A51;

            

             A54: v = ( [ [a, k], v] `2 )

            .= ( [ [d1, n1], z1] `2 ) by A52

            .= z1;

            

             A55: [a, k] = ( [ [a, k], v] `1 )

            .= ( [ [d1, n1], z1] `1 ) by A52

            .= [d1, n1];

            

             A56: n1 = ( [d1, n1] `2 )

            .= ( [a, k] `2 ) by A55

            .= k;

            consider f2 be sequence of D such that

             A57: f2 = (g . d1) and

             A58: z1 = (f2 . n1) by A53;

            consider n be Element of NAT , d be Element of C, z be Element of D such that

             A59: [ [a, (k + 1)], u] = [ [d, n], z] and

             A60: ex f1 be sequence of D st f1 = (g . d) & z = (f1 . n) by A50;

            

             A61: [a, (k + 1)] = ( [ [a, (k + 1)], u] `1 )

            .= ( [ [d, n], z] `1 ) by A59

            .= [d, n];

            

             A62: n = ( [d, n] `2 )

            .= ( [a, (k + 1)] `2 ) by A61

            .= (k + 1);

            

             A63: d1 = ( [d1, n1] `1 )

            .= ( [a, k] `1 ) by A55

            .= a;

            

             A64: d = ( [d, n] `1 )

            .= ( [a, (k + 1)] `1 ) by A61

            .= a;

            u = ( [ [a, (k + 1)], u] `2 )

            .= ( [ [d, n], z] `2 ) by A59

            .= z;

            

            hence (h . (a,(k + 1))) = (f9 . n) by A46, A50, A60, A64, FUNCT_1: 1

            .= (F . ((f2 . n1),a)) by A46, A48, A62, A57, A56, A63

            .= (F . ((h . (a,k)),a)) by A51, A58, A54, FUNCT_1: 1;

          end;

           [a, 0 ] in [:C, NAT :] by ZFMISC_1:def 2;

          then [a, 0 ] in ( dom h) by FUNCT_2:def 1;

          then

          consider u be object such that

           A65: [ [a, 0 ], u] in h by XTUPLE_0:def 12;

          consider n be Element of NAT , d be Element of C, z be Element of D such that

           A66: [ [a, 0 ], u] = [ [d, n], z] and

           A67: ex f1 be sequence of D st f1 = (g . d) & z = (f1 . n) by A65;

          

           A68: u = ( [ [a, 0 ], u] `2 )

          .= ( [ [d, n], z] `2 ) by A66

          .= z;

          

           A69: [a, 0 ] = ( [ [a, 0 ], u] `1 )

          .= ( [ [d, n], z] `1 ) by A66

          .= [d, n];

          

           A70: d = ( [d, n] `1 )

          .= ( [a, 0 ] `1 ) by A69

          .= a;

          n = ( [d, n] `2 )

          .= ( [a, 0 ] `2 ) by A69

          .= 0 ;

          hence thesis by A46, A47, A65, A67, A68, A70, A49, FUNCT_1: 1;

        end;

        hence thesis;

      end;

    end;

    begin

    theorem :: BINOM:3

    

     Th3: for L be left_zeroed non empty addLoopStr, a be Element of L holds ( Sum <*a*>) = a

    proof

      let V be left_zeroed non empty addLoopStr, v be Element of V;

      reconsider a = v as Element of V;

      set S = <*v*>;

      consider f be sequence of the carrier of V such that

       A1: ( Sum S) = (f . ( len S)) and

       A2: (f . 0 ) = ( 0. V) & for j be Nat holds for v be Element of V st j < ( len S) & v = (S . (j + 1)) holds (f . (j + 1)) = ((f . j) + v) by RLVECT_1:def 12;

      

       A3: ( len <*a*>) = 1 by FINSEQ_1: 39;

       0 < 1;

      then

      consider j be Element of NAT such that

       A4: j < ( len S);

      

       A5: (S . (j + 1)) = (S . ( 0 + 1)) by A3, A4, NAT_1: 14

      .= v by FINSEQ_1: 40;

      j = 0 by A3, A4, NAT_1: 14;

      

      then (f . 1) = (( 0. V) + v) by A2, A5

      .= a by ALGSTR_1:def 2;

      hence thesis by A1, FINSEQ_1: 39;

    end;

    theorem :: BINOM:4

    for R be left_zeroed right_add-cancelable right-distributive non empty doubleLoopStr, a be Element of R, p be FinSequence of the carrier of R holds ( Sum (a * p)) = (a * ( Sum p))

    proof

      let R be left_zeroed right_add-cancelable right-distributive non empty doubleLoopStr, a be Element of R, p be FinSequence of the carrier of R;

      consider f be sequence of the carrier of R such that

       A1: ( Sum p) = (f . ( len p)) and

       A2: (f . 0 ) = ( 0. R) and

       A3: for j be Nat, v be Element of R st j < ( len p) & v = (p . (j + 1)) holds (f . (j + 1)) = ((f . j) + v) by RLVECT_1:def 12;

      consider fa be sequence of the carrier of R such that

       A4: ( Sum (a * p)) = (fa . ( len (a * p))) and

       A5: (fa . 0 ) = ( 0. R) and

       A6: for j be Nat, v be Element of R st j < ( len (a * p)) & v = ((a * p) . (j + 1)) holds (fa . (j + 1)) = ((fa . j) + v) by RLVECT_1:def 12;

      defpred P[ Nat] means (a * (f . $1)) = (fa . $1);

      

       A7: ( Seg ( len (a * p))) = ( dom (a * p)) by FINSEQ_1:def 3

      .= ( dom p) by POLYNOM1:def 1

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

       A8:

      now

        let j be Element of NAT ;

        assume that 0 <= j and

         A9: j < ( len p);

        thus P[j] implies P[(j + 1)]

        proof

          

           A10: ( 0 + 1) <= (j + 1) by XREAL_1: 6;

          

           A11: j < ( len (a * p)) by A7, A9, FINSEQ_1: 6;

          then (j + 1) <= ( len (a * p)) by NAT_1: 13;

          then (j + 1) in ( Seg ( len (a * p))) by A10, FINSEQ_1: 1;

          then (j + 1) in ( dom (a * p)) by FINSEQ_1:def 3;

          then

           A12: ((a * p) /. (j + 1)) = ((a * p) . (j + 1)) by PARTFUN1:def 6;

          (j + 1) <= ( len p) by A9, NAT_1: 13;

          then (j + 1) in ( Seg ( len p)) by A10, FINSEQ_1: 1;

          then

           A13: (j + 1) in ( dom p) by FINSEQ_1:def 3;

          then

           A14: (p /. (j + 1)) = (p . (j + 1)) by PARTFUN1:def 6;

          assume P[j];

          

          hence (fa . (j + 1)) = ((a * (f . j)) + ((a * p) /. (j + 1))) by A6, A11, A12

          .= ((a * (f . j)) + (a * (p /. (j + 1)))) by A13, POLYNOM1:def 1

          .= (a * ((f . j) + (p /. (j + 1)))) by VECTSP_1:def 2

          .= (a * (f . (j + 1))) by A3, A9, A14;

        end;

      end;

      

       A15: P[ 0 ] by A2, A5, Th2;

      

       A16: for i be Element of NAT st 0 <= i & i <= ( len p) holds P[i] from INT_1:sch 7( A15, A8);

      

      thus ( Sum (a * p)) = (fa . ( len p)) by A4, A7, FINSEQ_1: 6

      .= (a * ( Sum p)) by A1, A16;

    end;

    theorem :: BINOM:5

    

     Th5: for R be right_zeroed left_add-cancelable left-distributive non empty doubleLoopStr, a be Element of R, p be FinSequence of the carrier of R holds ( Sum (p * a)) = (( Sum p) * a)

    proof

      let R be right_zeroed left_add-cancelable left-distributive non empty doubleLoopStr, a be Element of R, p be FinSequence of the carrier of R;

      consider f be sequence of the carrier of R such that

       A1: ( Sum p) = (f . ( len p)) and

       A2: (f . 0 ) = ( 0. R) and

       A3: for j be Nat, v be Element of R st j < ( len p) & v = (p . (j + 1)) holds (f . (j + 1)) = ((f . j) + v) by RLVECT_1:def 12;

      consider fa be sequence of the carrier of R such that

       A4: ( Sum (p * a)) = (fa . ( len (p * a))) and

       A5: (fa . 0 ) = ( 0. R) and

       A6: for j be Nat, v be Element of R st j < ( len (p * a)) & v = ((p * a) . (j + 1)) holds (fa . (j + 1)) = ((fa . j) + v) by RLVECT_1:def 12;

      defpred P[ Nat] means ((f . $1) * a) = (fa . $1);

      

       A7: ( Seg ( len (p * a))) = ( dom (p * a)) by FINSEQ_1:def 3

      .= ( dom p) by POLYNOM1:def 2

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

       A8:

      now

        let j be Element of NAT ;

        assume that 0 <= j and

         A9: j < ( len p);

        thus P[j] implies P[(j + 1)]

        proof

          

           A10: j < ( len (p * a)) by A7, A9, FINSEQ_1: 6;

          then

           A11: (j + 1) <= ( len (p * a)) by NAT_1: 13;

          

           A12: ( 0 + 1) <= (j + 1) by XREAL_1: 6;

          then (j + 1) in ( Seg ( len (p * a))) by A11, FINSEQ_1: 1;

          then (j + 1) in ( dom (p * a)) by FINSEQ_1:def 3;

          then

           A13: ((p * a) /. (j + 1)) = ((p * a) . (j + 1)) by PARTFUN1:def 6;

          (j + 1) in ( Seg ( len p)) by A7, A11, A12, FINSEQ_1: 1;

          then

           A14: (j + 1) in ( dom p) by FINSEQ_1:def 3;

          then

           A15: (p /. (j + 1)) = (p . (j + 1)) by PARTFUN1:def 6;

          assume ((f . j) * a) = (fa . j);

          

          hence (fa . (j + 1)) = (((f . j) * a) + ((p * a) /. (j + 1))) by A6, A10, A13

          .= (((f . j) * a) + ((p /. (j + 1)) * a)) by A14, POLYNOM1:def 2

          .= (((f . j) + (p /. (j + 1))) * a) by VECTSP_1:def 3

          .= ((f . (j + 1)) * a) by A3, A9, A15;

        end;

      end;

      

       A16: P[ 0 ] by A2, A5, Th1;

      

       A17: for i be Element of NAT st 0 <= i & i <= ( len p) holds P[i] from INT_1:sch 7( A16, A8);

      

      thus ( Sum (p * a)) = (fa . ( len p)) by A4, A7, FINSEQ_1: 6

      .= (( Sum p) * a) by A1, A17;

    end;

    theorem :: BINOM:6

    for R be commutative non empty multMagma, a be Element of R, p be FinSequence of the carrier of R holds (p * a) = (a * p)

    proof

      let R be commutative non empty multMagma, a be Element of R, p be FinSequence of the carrier of R;

      set pa = (p * a), ap = (a * p);

      

       A1: ( dom pa) = ( dom p) by POLYNOM1:def 2;

      

       A2: ( dom ap) = ( dom p) by POLYNOM1:def 1;

      now

        let i be Nat such that

         A3: i in ( dom pa);

        

        thus (pa /. i) = ((p /. i) * a) by A1, A3, POLYNOM1:def 2

        .= (ap /. i) by A1, A3, POLYNOM1:def 1;

      end;

      hence thesis by A1, A2, FINSEQ_5: 12;

    end;

    definition

      let R be non empty addLoopStr, p,q be FinSequence of the carrier of R;

      :: BINOM:def1

      func p + q -> FinSequence of the carrier of R means

      : Def1: ( dom it ) = ( dom p) & for i be Nat st 1 <= i & i <= ( len it ) holds (it /. i) = ((p /. i) + (q /. i));

      existence

      proof

        defpred P[ Nat, Element of R] means $2 = ((p /. $1) + (q /. $1));

        

         A1: for k be Nat st k in ( Seg ( len p)) holds ex x be Element of R st P[k, x];

        consider f be FinSequence of the carrier of R such that

         A2: ( dom f) = ( Seg ( len p)) & for k be Nat st k in ( Seg ( len p)) holds P[k, (f /. k)] from RECDEF_1:sch 17( A1);

        take f;

        

         A3: ( len f) = ( len p) by A2, FINSEQ_1:def 3;

        for m be Nat st 1 <= m <= ( len f) holds (f /. m) = ((p /. m) + (q /. m)) by A2, A3, FINSEQ_1: 1;

        hence thesis by A2, FINSEQ_1:def 3;

      end;

      uniqueness

      proof

        let y1,y2 be FinSequence of the carrier of R;

        assume that

         A4: ( dom y1) = ( dom p) and

         A5: for i be Nat st 1 <= i & i <= ( len y1) holds (y1 /. i) = ((p /. i) + (q /. i)) and

         A6: ( dom y2) = ( dom p) and

         A7: for i be Nat st 1 <= i & i <= ( len y2) holds (y2 /. i) = ((p /. i) + (q /. i));

        

         A8: ( Seg ( len y1)) = ( dom y2) by A4, A6, FINSEQ_1:def 3

        .= ( Seg ( len y2)) by FINSEQ_1:def 3;

        then

         A9: ( len y1) = ( len y2) by FINSEQ_1: 6;

        now

          let i be Nat;

          assume

           A10: 1 <= i & i <= ( len y1);

          then i in ( Seg ( len y2)) by A8, FINSEQ_1: 1;

          then

           A11: i in ( dom y2) by FINSEQ_1:def 3;

          i in ( Seg ( len y1)) by A10, FINSEQ_1: 1;

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

          

          hence (y1 . i) = (y1 /. i) by PARTFUN1:def 6

          .= ((p /. i) + (q /. i)) by A5, A10

          .= (y2 /. i) by A7, A9, A10

          .= (y2 . i) by A11, PARTFUN1:def 6;

        end;

        hence thesis by A8, FINSEQ_1: 6, FINSEQ_1: 14;

      end;

    end

    theorem :: BINOM:7

    

     Th7: for R be Abelian right_zeroed add-associative non empty addLoopStr, p,q be FinSequence of the carrier of R st ( dom p) = ( dom q) holds ( Sum (p + q)) = (( Sum p) + ( Sum q))

    proof

      let R be Abelian right_zeroed add-associative non empty addLoopStr, p,q be FinSequence of the carrier of R;

      consider fp be sequence of the carrier of R such that

       A1: ( Sum p) = (fp . ( len p)) and

       A2: (fp . 0 ) = ( 0. R) and

       A3: for j be Nat, v be Element of R st j < ( len p) & v = (p . (j + 1)) holds (fp . (j + 1)) = ((fp . j) + v) by RLVECT_1:def 12;

      consider fq be sequence of the carrier of R such that

       A4: ( Sum q) = (fq . ( len q)) and

       A5: (fq . 0 ) = ( 0. R) and

       A6: for j be Nat, v be Element of R st j < ( len q) & v = (q . (j + 1)) holds (fq . (j + 1)) = ((fq . j) + v) by RLVECT_1:def 12;

      assume ( dom p) = ( dom q);

      

      then

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

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

      then

       A8: ( len q) = ( len p) by FINSEQ_1: 6;

      consider fa be sequence of the carrier of R such that

       A9: ( Sum (p + q)) = (fa . ( len (p + q))) and

       A10: (fa . 0 ) = ( 0. R) and

       A11: for j be Nat, v be Element of R st j < ( len (p + q)) & v = ((p + q) . (j + 1)) holds (fa . (j + 1)) = ((fa . j) + v) by RLVECT_1:def 12;

      defpred P[ Nat] means ((fp . $1) + (fq . $1)) = (fa . $1);

      

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

      .= ( dom (p + q)) by Def1

      .= ( Seg ( len (p + q))) by FINSEQ_1:def 3;

      then

       A13: ( len (p + q)) = ( len p) by FINSEQ_1: 6;

       A14:

      now

        let j be Element of NAT ;

        assume that 0 <= j and

         A15: j < ( len p);

        thus P[j] implies P[(j + 1)]

        proof

          assume

           A16: P[j];

          

           A17: ( 0 + 1) <= (j + 1) by XREAL_1: 6;

          

           A18: (j + 1) <= ( len p) by A15, NAT_1: 13;

          then (j + 1) in ( Seg ( len p)) by A17, FINSEQ_1: 1;

          then (j + 1) in ( dom p) by FINSEQ_1:def 3;

          then

           A19: (p /. (j + 1)) = (p . (j + 1)) by PARTFUN1:def 6;

          (j + 1) in ( Seg ( len q)) by A7, A18, A17, FINSEQ_1: 1;

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

          then

           A20: (q /. (j + 1)) = (q . (j + 1)) by PARTFUN1:def 6;

          

           A21: (j + 1) <= ( len (p + q)) by A13, A15, NAT_1: 13;

          then (j + 1) in ( Seg ( len (p + q))) by A17, FINSEQ_1: 1;

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

          then ((p + q) /. (j + 1)) = ((p + q) . (j + 1)) by PARTFUN1:def 6;

          

          then (fa . (j + 1)) = ((fa . j) + ((p + q) /. (j + 1))) by A13, A11, A15

          .= (((fp . j) + (fq . j)) + ((p /. (j + 1)) + (q /. (j + 1)))) by A16, A21, A17, Def1

          .= ((fp . j) + ((fq . j) + ((p /. (j + 1)) + (q /. (j + 1))))) by RLVECT_1:def 3

          .= ((fp . j) + ((p /. (j + 1)) + ((fq . j) + (q /. (j + 1))))) by RLVECT_1:def 3

          .= (((fp . j) + (p /. (j + 1))) + ((fq . j) + (q /. (j + 1)))) by RLVECT_1:def 3

          .= ((fp . (j + 1)) + ((fq . j) + (q /. (j + 1)))) by A3, A15, A19

          .= ((fp . (j + 1)) + (fq . (j + 1))) by A8, A6, A15, A20;

          hence thesis;

        end;

      end;

      

       A22: P[ 0 ] by A2, A5, A10, RLVECT_1:def 4;

      

       A23: for i be Element of NAT st 0 <= i & i <= ( len p) holds P[i] from INT_1:sch 7( A22, A14);

      

      thus ( Sum (p + q)) = (fa . ( len p)) by A12, A9, FINSEQ_1: 6

      .= (( Sum p) + ( Sum q)) by A8, A1, A4, A23;

    end;

    begin

    definition

      let R be unital non empty multMagma, a be Element of R, n be Nat;

      :: BINOM:def2

      func a |^ n -> Element of R equals (( power R) . (a,n));

      coherence ;

    end

    theorem :: BINOM:8

    

     Th8: for R be unital non empty multMagma, a be Element of R holds (a |^ 0 ) = ( 1_ R) & (a |^ 1) = a

    proof

      let R be unital non empty multMagma, a be Element of R;

      thus (a |^ 0 ) = ( 1_ R) by GROUP_1:def 7;

      ( 0 + 1) = 1;

      

      then (( power R) . (a,1)) = ((( power R) . (a, 0 )) * a) by GROUP_1:def 7

      .= (( 1_ R) * a) by GROUP_1:def 7

      .= a by GROUP_1:def 4;

      hence thesis;

    end;

    theorem :: BINOM:9

    for R be unital associative commutative non empty multMagma, a,b be Element of R, n be Nat holds ((a * b) |^ n) = ((a |^ n) * (b |^ n))

    proof

      let R be unital associative commutative non empty multMagma, a,b be Element of R, n be Nat;

      defpred P[ Nat] means (( power R) . ((a * b),$1)) = ((a |^ $1) * (b |^ $1));

       A1:

      now

        let m be Nat;

        reconsider mm = m as Element of NAT by ORDINAL1:def 12;

        assume P[m];

        

        then (( power R) . ((a * b),(m + 1))) = (((( power R) . (a,mm)) * (( power R) . (b,mm))) * (a * b)) by GROUP_1:def 7

        .= ((((( power R) . (a,mm)) * (( power R) . (b,mm))) * a) * b) by GROUP_1:def 3

        .= ((((( power R) . (a,mm)) * a) * (( power R) . (b,mm))) * b) by GROUP_1:def 3

        .= (((( power R) . (a,mm)) * a) * ((( power R) . (b,mm)) * b)) by GROUP_1:def 3

        .= ((a |^ (m + 1)) * ((( power R) . (b,mm)) * b)) by GROUP_1:def 7

        .= ((a |^ (m + 1)) * (b |^ (m + 1))) by GROUP_1:def 7;

        hence P[(m + 1)];

      end;

      (( power R) . ((a * b), 0 )) = ( 1_ R) by GROUP_1:def 7

      .= (( 1_ R) * ( 1_ R)) by GROUP_1:def 4

      .= ((( power R) . (a, 0 )) * ( 1_ R)) by GROUP_1:def 7

      .= ((( power R) . (a, 0 )) * (( power R) . (b, 0 ))) by GROUP_1:def 7;

      then

       A2: P[ 0 ];

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

      hence thesis;

    end;

    

     Lm3: for R be unital associative non empty multMagma, a be Element of R, n,m be Element of NAT holds (a |^ (n + m)) = ((a |^ n) * (a |^ m))

    proof

      let R be unital associative non empty multMagma, a be Element of R, n,m be Element of NAT ;

      defpred P[ Nat] means (( power R) . (a,(n + $1))) = ((( power R) . (a,n)) * (a |^ $1));

       A1:

      now

        let m be Nat;

        assume

         A2: P[m];

        reconsider mm = m as Element of NAT by ORDINAL1:def 12;

        (( power R) . (a,(n + (m + 1)))) = (( power R) . (a,((n + m) + 1)))

        .= (((( power R) . (a,n)) * (( power R) . (a,mm))) * a) by A2, GROUP_1:def 7

        .= ((( power R) . (a,n)) * ((( power R) . (a,mm)) * a)) by GROUP_1:def 3

        .= ((( power R) . (a,n)) * (a |^ (m + 1))) by GROUP_1:def 7;

        hence P[(m + 1)];

      end;

      (( power R) . (a,(n + 0 ))) = ((( power R) . (a,n)) * ( 1_ R)) by GROUP_1:def 4

      .= ((( power R) . (a,n)) * (( power R) . (a, 0 ))) by GROUP_1:def 7;

      then

       A3: P[ 0 ];

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

      hence thesis;

    end;

    theorem :: BINOM:10

    

     Th10: for R be unital associative non empty multMagma, a be Element of R, n,m be Nat holds (a |^ (n + m)) = ((a |^ n) * (a |^ m))

    proof

      let R be unital associative non empty multMagma, a be Element of R, n,m be Nat;

      reconsider n1 = n, m1 = m as Element of NAT by ORDINAL1:def 12;

      (a |^ (n1 + m1)) = ((a |^ n1) * (a |^ m1)) by Lm3;

      hence thesis;

    end;

    theorem :: BINOM:11

    for R be unital associative non empty multMagma, a be Element of R, n,m be Nat holds ((a |^ n) |^ m) = (a |^ (n * m))

    proof

      let R be unital associative non empty multMagma, a be Element of R, n,m be Nat;

      defpred P[ Nat] means (( power R) . ((a |^ n),$1)) = (( power R) . (a,(n * $1)));

       A1:

      now

        let m be Nat;

        assume P[m];

        

        then (( power R) . ((a |^ n),(m + 1))) = ((a |^ (n * m)) * (a |^ n)) by GROUP_1:def 7

        .= (a |^ ((n * m) + n)) by Th10

        .= (( power R) . (a,(n * (m + 1))));

        hence P[(m + 1)];

      end;

      (( power R) . ((a |^ n), 0 )) = ( 1_ R) by GROUP_1:def 7

      .= (( power R) . (a,(n * 0 ))) by GROUP_1:def 7;

      then

       A2: P[ 0 ];

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

      hence thesis;

    end;

    begin

    definition

      let R be non empty addLoopStr;

      :: BINOM:def3

      func Nat-mult-left (R) -> Function of [: NAT , the carrier of R:], the carrier of R means

      : Def3: for a be Element of R holds (it . ( 0 ,a)) = ( 0. R) & for n be Nat holds (it . ((n + 1),a)) = (a + (it . (n,a)));

      existence

      proof

        set D = the carrier of R;

        consider g be Function of [: NAT , D:], D such that

         A1: for a be Element of D holds (g . ( 0 ,a)) = ( 0. R) & for n be Nat holds (g . ((n + 1),a)) = (the addF of R . (a,(g . (n,a)))) by Lm1;

        take g;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let f,g be Function of [: NAT , the carrier of R:], the carrier of R;

        assume

         A2: for a be Element of R holds (f . ( 0 ,a)) = ( 0. R) & for n be Nat holds (f . ((n + 1),a)) = (a + (f . (n,a)));

        defpred P[ Nat] means for a be Element of R holds (f . ($1,a)) = (g . ($1,a));

        assume

         A3: for a be Element of R holds (g . ( 0 ,a)) = ( 0. R) & for n be Nat holds (g . ((n + 1),a)) = (a + (g . (n,a)));

         A4:

        now

          let n be Nat;

          assume

           A5: P[n];

          now

            let a be Element of R;

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

            

            thus (f . ((n + 1),a)) = (a + (f . (nn,a))) by A2

            .= (a + (g . (nn,a))) by A5

            .= (g . ((n + 1),a)) by A3;

          end;

          hence P[(n + 1)];

        end;

        

         A6: P[ 0 ]

        proof

          let a be Element of R;

          

          thus (f . ( 0 ,a)) = ( 0. R) by A2

          .= (g . ( 0 ,a)) by A3;

        end;

        

         A7: for n be Nat holds P[n] from NAT_1:sch 2( A6, A4);

         A8:

        now

          let x be object;

          assume x in [: NAT , the carrier of R:];

          then

          consider u,v be object such that

           A9: u in NAT and

           A10: v in the carrier of R and

           A11: x = [u, v] by ZFMISC_1:def 2;

          reconsider v as Element of R by A10;

          reconsider u as Element of NAT by A9;

          

          thus (f . x) = (f . (u,v)) by A11

          .= (g . (u,v)) by A7

          .= (g . x) by A11;

        end;

        ( dom f) = [: NAT , the carrier of R:] & ( dom g) = [: NAT , the carrier of R:] by FUNCT_2:def 1;

        hence thesis by A8, FUNCT_1: 2;

      end;

      :: BINOM:def4

      func Nat-mult-right (R) -> Function of [:the carrier of R, NAT :], the carrier of R means

      : Def4: for a be Element of R holds (it . (a, 0 )) = ( 0. R) & for n be Element of NAT holds (it . (a,(n + 1))) = ((it . (a,n)) + a);

      existence

      proof

        consider g be Function of [:the carrier of R, NAT :], the carrier of R such that

         A12: for a be Element of R holds (g . (a, 0 )) = ( 0. R) & for n be Element of NAT holds (g . (a,(n + 1))) = (the addF of R . ((g . (a,n)),a)) by Lm2;

        take g;

        thus thesis by A12;

      end;

      uniqueness

      proof

        let f,g be Function of [:the carrier of R, NAT :], the carrier of R;

        assume

         A13: for a be Element of R holds (f . (a, 0 )) = ( 0. R) & for n be Element of NAT holds (f . (a,(n + 1))) = ((f . (a,n)) + a);

        defpred P[ Nat] means for a be Element of R holds (f . (a,$1)) = (g . (a,$1));

        assume

         A14: for a be Element of R holds (g . (a, 0 )) = ( 0. R) & for n be Element of NAT holds (g . (a,(n + 1))) = ((g . (a,n)) + a);

         A15:

        now

          let n be Nat;

          assume

           A16: P[n];

          now

            let a be Element of R;

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

            

            thus (f . (a,(n + 1))) = ((f . (a,nn)) + a) by A13

            .= ((g . (a,nn)) + a) by A16

            .= (g . (a,(n + 1))) by A14;

          end;

          hence P[(n + 1)];

        end;

        

         A17: P[ 0 ]

        proof

          let a be Element of R;

          

          thus (f . (a, 0 )) = ( 0. R) by A13

          .= (g . (a, 0 )) by A14;

        end;

        

         A18: for n be Nat holds P[n] from NAT_1:sch 2( A17, A15);

         A19:

        now

          let x be object;

          assume x in [:the carrier of R, NAT :];

          then

          consider v,u be object such that

           A20: v in the carrier of R and

           A21: u in NAT and

           A22: x = [v, u] by ZFMISC_1:def 2;

          reconsider v as Element of R by A20;

          reconsider u as Element of NAT by A21;

          

          thus (f . x) = (f . (v,u)) by A22

          .= (g . (v,u)) by A18

          .= (g . x) by A22;

        end;

        ( dom f) = [:the carrier of R, NAT :] & ( dom g) = [:the carrier of R, NAT :] by FUNCT_2:def 1;

        hence thesis by A19, FUNCT_1: 2;

      end;

    end

    definition

      let R be non empty addLoopStr, a be Element of R, n be Nat;

      :: BINOM:def5

      func n * a -> Element of R equals (( Nat-mult-left R) . (n,a));

      coherence ;

      :: BINOM:def6

      func a * n -> Element of R equals (( Nat-mult-right R) . (a,n));

      coherence ;

    end

    theorem :: BINOM:12

    for R be non empty addLoopStr, a be Element of R holds ( 0 * a) = ( 0. R) & (a * 0 ) = ( 0. R) by Def3, Def4;

    theorem :: BINOM:13

    

     Th13: for R be right_zeroed non empty addLoopStr, a be Element of R holds (1 * a) = a

    proof

      let R be right_zeroed non empty addLoopStr, a be Element of R;

      

      thus (1 * a) = (( Nat-mult-left R) . (( 0 + 1),a))

      .= (a + (( Nat-mult-left R) . ( 0 ,a))) by Def3

      .= (a + ( 0. R)) by Def3

      .= a by RLVECT_1:def 4;

    end;

    theorem :: BINOM:14

    

     Th14: for R be left_zeroed non empty addLoopStr, a be Element of R holds (a * 1) = a

    proof

      let R be left_zeroed non empty addLoopStr, a be Element of R;

      

      thus (a * 1) = (( Nat-mult-right R) . (a,( 0 + 1)))

      .= ((( Nat-mult-right R) . (a, 0 )) + a) by Def4

      .= (( 0. R) + a) by Def4

      .= a by ALGSTR_1:def 2;

    end;

    theorem :: BINOM:15

    

     Th15: for R be left_zeroed add-associative non empty addLoopStr, a be Element of R, n,m be Nat holds ((n + m) * a) = ((n * a) + (m * a))

    proof

      let R be left_zeroed add-associative non empty addLoopStr, a be Element of R, n,m be Nat;

      defpred P[ Nat] means (($1 + m) * a) = (($1 * a) + (m * a));

       A1:

      now

        let k be Nat;

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

        assume

         A2: P[k];

        (((k + 1) + m) * a) = (((k + m) + 1) * a)

        .= (a + ((k + m) * a)) by Def3

        .= (a + ((kk * a) + (m * a))) by A2

        .= ((a + (k * a)) + (m * a)) by RLVECT_1:def 3

        .= (((kk + 1) * a) + (m * a)) by Def3;

        hence P[(k + 1)];

      end;

      (( 0 + m) * a) = (( 0. R) + (m * a)) by ALGSTR_1:def 2

      .= (( 0 * a) + (m * a)) by Def3;

      then

       A3: P[ 0 ];

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

      hence thesis;

    end;

    theorem :: BINOM:16

    

     Th16: for R be right_zeroed add-associative non empty addLoopStr, a be Element of R, n,m be Element of NAT holds (a * (n + m)) = ((a * n) + (a * m))

    proof

      let R be right_zeroed add-associative non empty addLoopStr, a be Element of R, n,m be Element of NAT ;

      defpred P[ Nat] means (a * (n + $1)) = ((a * n) + (a * $1));

       A1:

      now

        let k be Nat;

        assume

         A2: P[k];

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

        (a * (n + (k + 1))) = (a * ((n + kk) + 1))

        .= (((a * n) + (a * kk)) + a) by A2, Def4

        .= ((a * n) + ((a * k) + a)) by RLVECT_1:def 3

        .= ((a * n) + (a * (kk + 1))) by Def4;

        hence P[(k + 1)];

      end;

      (a * (n + 0 )) = ((a * n) + ( 0. R)) by RLVECT_1:def 4

      .= ((a * n) + (a * 0 )) by Def4;

      then

       A3: P[ 0 ];

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

      hence thesis;

    end;

    theorem :: BINOM:17

    

     Th17: for R be left_zeroed right_zeroed add-associative non empty addLoopStr, a be Element of R, n be Element of NAT holds (n * a) = (a * n)

    proof

      let R be left_zeroed right_zeroed add-associative non empty addLoopStr, a be Element of R, n be Element of NAT ;

      defpred P[ Nat] means ($1 * a) = (a * $1);

       A1:

      now

        let k be Nat;

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

        assume

         A2: P[k];

        ((kk + 1) * a) = ((k * a) + (1 * a)) by Th15

        .= ((k * a) + a) by Th13

        .= ((a * k) + (a * 1)) by A2, Th14

        .= (a * (kk + 1)) by Th16;

        hence P[(k + 1)];

      end;

      ( 0 * a) = ( 0. R) by Def3

      .= (a * 0 ) by Def4;

      then

       A3: P[ 0 ];

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

      hence thesis;

    end;

    theorem :: BINOM:18

    for R be Abelian non empty addLoopStr, a be Element of R, n be Element of NAT holds (n * a) = (a * n)

    proof

      let R be Abelian non empty addLoopStr, a be Element of R, n be Element of NAT ;

      defpred P[ Nat] means ($1 * a) = (a * $1);

       A1:

      now

        let k be Nat;

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

        assume P[k];

        

        then ((kk + 1) * a) = (a + (a * k)) by Def3

        .= (a * (kk + 1)) by Def4;

        hence P[(k + 1)];

      end;

      ( 0 * a) = ( 0. R) by Def3

      .= (a * 0 ) by Def4;

      then

       A2: P[ 0 ];

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

      hence thesis;

    end;

    theorem :: BINOM:19

    

     Th19: for R be left_zeroed right_zeroed left_add-cancelable add-associative left-distributive non empty doubleLoopStr, a,b be Element of R, n be Element of NAT holds ((n * a) * b) = (n * (a * b))

    proof

      let R be left_zeroed right_zeroed left_add-cancelable add-associative left-distributive non empty doubleLoopStr, a,b be Element of R, n be Element of NAT ;

      defpred P[ Nat] means (($1 * a) * b) = ($1 * (a * b));

       A1:

      now

        let k be Nat;

        assume

         A2: P[k];

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

        (((kk + 1) * a) * b) = ((a + (k * a)) * b) by Def3

        .= ((a * b) + (k * (a * b))) by A2, VECTSP_1:def 3

        .= ((1 * (a * b)) + (k * (a * b))) by Th13

        .= ((kk + 1) * (a * b)) by Th15;

        hence P[(k + 1)];

      end;

      (( 0 * a) * b) = (( 0. R) * b) by Def3

      .= ( 0. R) by Th1

      .= ( 0 * (a * b)) by Def3;

      then

       A3: P[ 0 ];

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

      hence thesis;

    end;

    theorem :: BINOM:20

    

     Th20: for R be left_zeroed right_zeroed right_add-cancelable add-associative distributive non empty doubleLoopStr, a,b be Element of R, n be Element of NAT holds (b * (n * a)) = ((b * a) * n)

    proof

      let R be left_zeroed right_zeroed add-associative right_add-cancelable distributive non empty doubleLoopStr, a,b be Element of R, n be Element of NAT ;

      defpred P[ Nat] means (b * ($1 * a)) = ((b * a) * $1);

       A1:

      now

        let k be Nat;

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

        assume

         A2: P[k];

        (b * ((kk + 1) * a)) = (b * (a + (k * a))) by Def3

        .= ((b * a) + ((b * a) * k)) by A2, VECTSP_1:def 2

        .= (((b * a) * 1) + ((b * a) * k)) by Th14

        .= ((b * a) * (kk + 1)) by Th16;

        hence P[(k + 1)];

      end;

      (b * ( 0 * a)) = (b * ( 0. R)) by Def3

      .= ( 0. R) by Th2

      .= ((b * a) * 0 ) by Def4;

      then

       A3: P[ 0 ];

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

      hence thesis;

    end;

    theorem :: BINOM:21

    

     Th21: for R be left_zeroed right_zeroed add-associative add-cancelable distributive non empty doubleLoopStr, a,b be Element of R, n be Element of NAT holds ((a * n) * b) = (a * (n * b))

    proof

      let R be left_zeroed right_zeroed distributive add-cancelable add-associative non empty doubleLoopStr, a,b be Element of R, n be Element of NAT ;

      

      thus ((a * n) * b) = ((n * a) * b) by Th17

      .= (n * (a * b)) by Th19

      .= ((a * b) * n) by Th17

      .= (a * (n * b)) by Th20;

    end;

    begin

    definition

      let R be unital non empty doubleLoopStr, a,b be Element of R, n be Nat;

      :: BINOM:def7

      func (a,b) In_Power n -> FinSequence of the carrier of R means

      : Def7: ( len it ) = (n + 1) & for i,l,m be Nat st i in ( dom it ) & m = (i - 1) & l = (n - m) holds (it /. i) = (((n choose m) * (a |^ l)) * (b |^ m));

      existence

      proof

        defpred P[ Nat, Element of R] means for l,m be Nat st m = ($1 - 1) & l = (n - m) holds $2 = (((n choose m) * (a |^ l)) * (b |^ m));

        

         A1: for k be Nat st k in ( Seg (n + 1)) holds ex y be Element of R st P[k, y]

        proof

          let k be Nat;

          assume

           A2: k in ( Seg (n + 1));

          then k >= 1 by FINSEQ_1: 1;

          then

          reconsider m1 = (k - 1) as Element of NAT by INT_1: 5;

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

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

          then

          reconsider l1 = (n - m1) as Element of NAT by INT_1: 5;

          reconsider z = (((n choose m1) * (a |^ l1)) * (b |^ m1)) as Element of R;

          take z;

          thus thesis;

        end;

        consider p be FinSequence of the carrier of R such that

         A3: ( dom p) = ( Seg (n + 1)) & for k be Nat st k in ( Seg (n + 1)) holds P[k, (p /. k)] from RECDEF_1:sch 17( A1);

        take p;

        thus thesis by A3, FINSEQ_1:def 3;

      end;

      uniqueness

      proof

        let f,g be FinSequence of the carrier of R;

        assume that

         A4: ( len f) = (n + 1) and

         A5: for i,l,m be Nat st i in ( dom f) & m = (i - 1) & l = (n - m) holds (f /. i) = (((n choose m) * (a |^ l)) * (b |^ m));

        assume that

         A6: ( len g) = (n + 1) and

         A7: for i,l,m be Nat st i in ( dom g) & m = (i - 1) & l = (n - m) holds (g /. i) = (((n choose m) * (a |^ l)) * (b |^ m));

        for i be Nat st 1 <= i & i <= ( len f) holds (f . i) = (g . i)

        proof

          let i be Nat;

          assume that

           A8: 1 <= i and

           A9: i <= ( len f);

          reconsider m = (i - 1) as Element of NAT by A8, INT_1: 5;

          (i - 1) <= ((n + 1) - 1) by A4, A9, XREAL_1: 9;

          then

          reconsider l = (n - m) as Element of NAT by INT_1: 5;

          

           A10: i in ( Seg (n + 1)) by A4, A8, A9, FINSEQ_1: 1;

          then

           A11: i in ( dom f) by A4, FINSEQ_1:def 3;

          

           A12: i in ( dom g) by A6, A10, FINSEQ_1:def 3;

          

          hence (g . i) = (g /. i) by PARTFUN1:def 6

          .= (((n choose m) * (a |^ l)) * (b |^ m)) by A7, A12

          .= (f /. i) by A5, A11

          .= (f . i) by A11, PARTFUN1:def 6;

        end;

        hence f = g by A4, A6, FINSEQ_1: 14;

      end;

    end

    theorem :: BINOM:22

    

     Th22: for R be right_zeroed unital non empty doubleLoopStr, a,b be Element of R holds ((a,b) In_Power 0 ) = <*( 1_ R)*>

    proof

      let R be right_zeroed unital non empty doubleLoopStr, a,b be Element of R;

      set p = ((a,b) In_Power 0 );

      

       A1: ( len p) = ( 0 + 1) by Def7

      .= 1;

      then

       A2: ( dom p) = {1} by FINSEQ_1: 2, FINSEQ_1:def 3;

      then

       A3: 1 in ( dom p) by TARSKI:def 1;

      then

      consider i be Element of NAT such that

       A4: i in ( dom p);

      

       A5: i = 1 by A2, A4, TARSKI:def 1;

      then

      reconsider m = (i - 1) as Element of NAT by INT_1: 5;

      reconsider l = ( 0 - m) as Element of NAT by A5;

      (p . 1) = (p /. 1) by A3, PARTFUN1:def 6

      .= ((( 0 choose m) * (a |^ l)) * (b |^ m)) by A3, A5, Def7

      .= ((1 * (a |^ l)) * (b |^ m)) by A5, NEWTON: 19

      .= ((1 * (a |^ 0 )) * ( 1_ R)) by A5, Th8

      .= ((1 * ( 1_ R)) * ( 1_ R)) by Th8

      .= (( 1_ R) * ( 1_ R)) by Th13

      .= ( 1_ R) by GROUP_1:def 4;

      hence thesis by A1, FINSEQ_1: 40;

    end;

    theorem :: BINOM:23

    

     Th23: for R be right_zeroed unital non empty doubleLoopStr, a,b be Element of R, n be Nat holds (((a,b) In_Power n) . 1) = (a |^ n)

    proof

      reconsider m = (1 - 1) as Element of NAT by NEWTON: 19;

      let R be right_zeroed unital non empty doubleLoopStr, a,b be Element of R, n be Nat;

      reconsider l = (n - m) as Nat;

      ( len ((a,b) In_Power n)) = (n + 1) by Def7;

      then

       A1: ( dom ((a,b) In_Power n)) = ( Seg (n + 1)) by FINSEQ_1:def 3;

      ( 0 + 1) <= (n + 1) by XREAL_1: 6;

      then

       A2: 1 in ( dom ((a,b) In_Power n)) by A1, FINSEQ_1: 1;

      

      hence (((a,b) In_Power n) . 1) = (((a,b) In_Power n) /. 1) by PARTFUN1:def 6

      .= (((n choose 0 ) * (a |^ l)) * (b |^ m)) by A2, Def7

      .= ((1 * (a |^ n)) * (b |^ 0 )) by NEWTON: 19

      .= ((a |^ n) * (b |^ 0 )) by Th13

      .= ((a |^ n) * ( 1_ R)) by Th8

      .= (a |^ n) by GROUP_1:def 4;

    end;

    theorem :: BINOM:24

    

     Th24: for R be right_zeroed unital non empty doubleLoopStr, a,b be Element of R, n be Nat holds (((a,b) In_Power n) . (n + 1)) = (b |^ n)

    proof

      let R be right_zeroed unital non empty doubleLoopStr, a,b be Element of R, n be Nat;

      reconsider m = ((n + 1) - 1) as Nat;

      reconsider l = (n - m) as Element of NAT by INT_1: 5;

      ( len ((a,b) In_Power n)) = (n + 1) by Def7;

      then

       A1: ( dom ((a,b) In_Power n)) = ( Seg (n + 1)) by FINSEQ_1:def 3;

      then

       A2: l = 0 & (n + 1) in ( dom ((a,b) In_Power n)) by FINSEQ_1: 4;

      

      thus (((a,b) In_Power n) . (n + 1)) = (((a,b) In_Power n) /. (n + 1)) by A1, FINSEQ_1: 4, PARTFUN1:def 6

      .= (((n choose n) * (a |^ 0 )) * (b |^ n)) by A2, Def7

      .= ((1 * (a |^ 0 )) * (b |^ n)) by NEWTON: 21

      .= ((1 * ( 1_ R)) * (b |^ n)) by Th8

      .= (( 1_ R) * (b |^ n)) by Th13

      .= (b |^ n) by GROUP_1:def 4;

    end;

    ::$Notion-Name

    theorem :: BINOM:25

    for R be Abelian add-associative left_zeroed right_zeroed commutative associative add-cancelable distributive unital non empty doubleLoopStr, a,b be Element of R, n be Element of NAT holds ((a + b) |^ n) = ( Sum ((a,b) In_Power n))

    proof

      let R be add-associative left_zeroed right_zeroed distributive associative Abelian add-cancelable commutative unital non empty doubleLoopStr, a,b be Element of R, n be Element of NAT ;

      defpred P[ Nat] means ((a + b) |^ $1) = ( Sum ((a,b) In_Power $1));

      

       A1: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat;

        set G1 = ((((a,b) In_Power n) * a) ^ <*( 0. R)*>);

        set G2 = ( <*( 0. R)*> ^ (((a,b) In_Power n) * b));

        

         A2: ( Seg ( len (((a,b) In_Power n) * a))) = ( dom (((a,b) In_Power n) * a)) by FINSEQ_1:def 3

        .= ( dom ((a,b) In_Power n)) by POLYNOM1:def 2

        .= ( Seg ( len ((a,b) In_Power n))) by FINSEQ_1:def 3;

        ( len G1) = (( len (((a,b) In_Power n) * a)) + ( len <*( 0. R)*>)) by FINSEQ_1: 22

        .= (( len (((a,b) In_Power n) * a)) + 1) by FINSEQ_1: 40

        .= (( len ((a,b) In_Power n)) + 1) by A2, FINSEQ_1: 6

        .= ((n + 1) + 1) by Def7;

        then

        reconsider F1 = G1 as Element of (((n + 1) + 1) -tuples_on the carrier of R) by FINSEQ_2: 92;

        

         A3: ( Seg ( len (((a,b) In_Power n) * b))) = ( dom (((a,b) In_Power n) * b)) by FINSEQ_1:def 3

        .= ( dom ((a,b) In_Power n)) by POLYNOM1:def 2

        .= ( Seg ( len ((a,b) In_Power n))) by FINSEQ_1:def 3;

        ( len G2) = (( len (((a,b) In_Power n) * b)) + ( len <*( 0. R)*>)) by FINSEQ_1: 22

        .= (( len (((a,b) In_Power n) * b)) + 1) by FINSEQ_1: 40

        .= (( len ((a,b) In_Power n)) + 1) by A3, FINSEQ_1: 6

        .= ((n + 1) + 1) by Def7;

        then

        reconsider F2 = G2 as Element of (((n + 1) + 1) -tuples_on the carrier of R) by FINSEQ_2: 92;

        

         A4: ( len F1) = ((n + 1) + 1) by CARD_1:def 7;

        set F = (F1 + F2);

        

         A5: ( len F2) = ((n + 1) + 1) by CARD_1:def 7;

        

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

        .= ( dom F1) by Def1

        .= ( Seg ( len F1)) by FINSEQ_1:def 3;

        then

         A7: ( len F) = ((n + 1) + 1) by A4, FINSEQ_1: 6;

        

         A8: for i be Nat st 1 <= i & i <= ( len ((a,b) In_Power (n + 1))) holds (F . i) = (((a,b) In_Power (n + 1)) . i)

        proof

          let i be Nat;

          assume that

           A9: 1 <= i and

           A10: i <= ( len ((a,b) In_Power (n + 1)));

          

           A11: ( len ((a,b) In_Power (n + 1))) = ((n + 1) + 1) by Def7;

          then

           A12: ( dom ((a,b) In_Power (n + 1))) = ( Seg ((n + 1) + 1)) by FINSEQ_1:def 3;

          then

           A13: i in ( dom ((a,b) In_Power (n + 1))) by A9, A10, A11, FINSEQ_1: 1;

          reconsider j = (i - 1) as Element of NAT by A9, INT_1: 5;

          set x = (((a,b) In_Power n) /. j);

          set r1 = (F1 /. i);

          set r2 = (F2 /. i);

          set r = (((a,b) In_Power n) /. i);

          

           A14: i = (j + 1);

          

           A15: i in ( Seg ((n + 1) + 1)) by A9, A10, A11, FINSEQ_1: 1;

          then

           A16: i in ( dom F1) by A4, FINSEQ_1:def 3;

          

           A17: i in ( dom F2) by A5, A15, FINSEQ_1:def 3;

          

           A18: i <= ( len (F1 + F2)) by A7, A10, Def7;

          

           A19: i in {((n + 1) + 1)} implies (F . i) = (((a,b) In_Power (n + 1)) . i)

          proof

            assume

             A20: i in {((n + 1) + 1)};

            then

             A21: i = ((n + 1) + 1) by TARSKI:def 1;

            (n + 1) = ( len ((a,b) In_Power n)) by Def7

            .= ( len (((a,b) In_Power n) * a)) by A2, FINSEQ_1: 6;

            

            then

             A22: r1 = (((((a,b) In_Power n) * a) ^ <*( 0. R)*>) . (( len (((a,b) In_Power n) * a)) + 1)) by A16, A21, PARTFUN1:def 6

            .= ( 0. R) by FINSEQ_1: 42;

            

             A23: j = (((n + 1) + 1) - 1) by A20, TARSKI:def 1

            .= (n + 1);

            (n + 1) in ( Seg (n + 1)) by FINSEQ_1: 4;

            then

             A24: j in ( Seg ( len ((a,b) In_Power n))) by A23, Def7;

            then

             A25: j in ( dom (((a,b) In_Power n) * b)) by A3, FINSEQ_1:def 3;

            

             A26: j in ( dom ((a,b) In_Power n)) by A24, FINSEQ_1:def 3;

            

            then

             A27: x = (((a,b) In_Power n) . (n + 1)) by A23, PARTFUN1:def 6

            .= (b |^ n) by Th24;

            

             A28: r2 = (( <*( 0. R)*> ^ (((a,b) In_Power n) * b)) . (1 + (n + 1))) by A17, A21, PARTFUN1:def 6

            .= (( <*( 0. R)*> ^ (((a,b) In_Power n) * b)) . (( len <*( 0. R)*>) + j)) by A23, FINSEQ_1: 39

            .= ((((a,b) In_Power n) * b) . j) by A25, FINSEQ_1:def 7

            .= ((((a,b) In_Power n) * b) /. j) by A25, PARTFUN1:def 6

            .= ((b |^ n) * b) by A26, A27, POLYNOM1:def 2

            .= (b |^ (n + 1)) by GROUP_1:def 7;

            ( dom F) = ( Seg ((n + 1) + 1)) by A4, A6, FINSEQ_1:def 3;

            then i in ( dom F) by A9, A21, FINSEQ_1: 1;

            

            hence (F . i) = (F /. i) by PARTFUN1:def 6

            .= (( 0. R) + r2) by A9, A18, A22, Def1

            .= (b |^ (n + 1)) by A28, ALGSTR_1:def 2

            .= (((a,b) In_Power (n + 1)) . i) by A21, Th24;

          end;

          

           A29: i in ( dom F) by A4, A6, A15, FINSEQ_1:def 3;

          

           A30: i in { k where k be Element of NAT : k > 1 & k < ((n + 1) + 1) } implies (F . i) = (((a,b) In_Power (n + 1)) . i)

          proof

            assume i in { k where k be Element of NAT : 1 < k & k < ((n + 1) + 1) };

            then

             A31: ex k be Element of NAT st k = i & 1 < k & k < ((n + 1) + 1);

            then

            reconsider m1 = (i - 1) as Element of NAT by INT_1: 5;

            

             A32: i <= (n + 1) by A31, NAT_1: 13;

            then i in ( Seg (n + 1)) by A31, FINSEQ_1: 1;

            then

             A33: i in ( Seg ( len ((a,b) In_Power n))) by Def7;

            then

             A34: i in ( dom ((a,b) In_Power n)) by FINSEQ_1:def 3;

            1 <= j by A14, A31, NAT_1: 13;

            then

            reconsider m2 = (j - 1) as Element of NAT by INT_1: 5;

            

             A35: j <= (n + 1) by A14, A31, XREAL_1: 6;

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

            then

            reconsider l2 = (n - m2) as Element of NAT by INT_1: 5;

            1 <= j by A14, A31, NAT_1: 13;

            then j in ( Seg (n + 1)) by A35, FINSEQ_1: 1;

            then

             A36: j in ( Seg ( len ((a,b) In_Power n))) by Def7;

            then

             A37: j in ( dom ((a,b) In_Power n)) by FINSEQ_1:def 3;

            

             A38: j in ( dom (((a,b) In_Power n) * b)) by A3, A36, FINSEQ_1:def 3;

            

             A39: j in ( dom (((a,b) In_Power n) * b)) by A3, A36, FINSEQ_1:def 3;

            r2 = (( <*( 0. R)*> ^ (((a,b) In_Power n) * b)) . i) by A17, PARTFUN1:def 6;

            

            then

             A40: r2 = (( <*( 0. R)*> ^ (((a,b) In_Power n) * b)) . (( len <*( 0. R)*>) + j)) by A14, FINSEQ_1: 40

            .= ((((a,b) In_Power n) * b) . j) by A39, FINSEQ_1:def 7

            .= ((((a,b) In_Power n) * b) /. j) by A38, PARTFUN1:def 6

            .= (x * b) by A37, POLYNOM1:def 2;

            (i - 1) <= ((n + 1) - 1) by A32, XREAL_1: 9;

            then

            reconsider l1 = (n - m1) as Element of NAT by INT_1: 5;

            

             A41: (l1 + 1) = ((n + 1) - (m2 + 1));

            

             A42: i in ( dom (((a,b) In_Power n) * a)) by A2, A33, FINSEQ_1:def 3;

            r1 = (((((a,b) In_Power n) * a) ^ <*( 0. R)*>) . i) by A16, PARTFUN1:def 6;

            

            then

             A43: r1 = ((((a,b) In_Power n) * a) . i) by A42, FINSEQ_1:def 7

            .= ((((a,b) In_Power n) * a) /. i) by A42, PARTFUN1:def 6

            .= (r * a) by A34, POLYNOM1:def 2;

            

            thus (F . i) = (F /. i) by A29, PARTFUN1:def 6

            .= ((F1 /. i) + (x * b)) by A9, A18, A40, Def1

            .= (((((n choose m1) * (a |^ l1)) * (b |^ m1)) * a) + (x * b)) by A34, A43, Def7

            .= (((((a |^ l1) * (n choose m1)) * (b |^ m1)) * a) + (x * b)) by Th17

            .= ((a * ((a |^ l1) * ((n choose m1) * (b |^ m1)))) + (x * b)) by Th21

            .= (((a * (a |^ l1)) * ((n choose m1) * (b |^ m1))) + (x * b)) by GROUP_1:def 3

            .= (((a |^ (l1 + 1)) * ((n choose m1) * (b |^ m1))) + (x * b)) by GROUP_1:def 7

            .= (((a |^ (l1 + 1)) * ((n choose m1) * (b |^ m1))) + (((b |^ m2) * ((n choose m2) * (a |^ l2))) * b)) by A37, Def7

            .= (((a |^ (l1 + 1)) * ((n choose m1) * (b |^ m1))) + (((b |^ m2) * b) * ((n choose m2) * (a |^ l2)))) by GROUP_1:def 3

            .= (((a |^ (l1 + 1)) * ((n choose (m2 + 1)) * (b |^ (m2 + 1)))) + ((b |^ (m2 + 1)) * ((n choose m2) * (a |^ l2)))) by GROUP_1:def 7

            .= ((((b |^ (m2 + 1)) * (a |^ (l1 + 1))) * (n choose (m2 + 1))) + ((b |^ (m2 + 1)) * ((n choose m2) * (a |^ l2)))) by Th20

            .= (((b |^ (m2 + 1)) * ((n choose (m2 + 1)) * (a |^ (l1 + 1)))) + ((b |^ (m2 + 1)) * ((n choose m2) * (a |^ l2)))) by Th20

            .= (((b |^ (m2 + 1)) * ((a |^ (l1 + 1)) * (n choose (m2 + 1)))) + ((b |^ (m2 + 1)) * ((n choose m2) * (a |^ l2)))) by Th17

            .= ((((a |^ (l1 + 1)) * (n choose (m2 + 1))) + ((n choose m2) * (a |^ l2))) * (b |^ (m2 + 1))) by VECTSP_1:def 7

            .= ((((n choose (m2 + 1)) * (a |^ (l1 + 1))) + ((n choose m2) * (a |^ (l1 + 1)))) * (b |^ (m2 + 1))) by Th17

            .= ((((n choose (m2 + 1)) + (n choose m2)) * (a |^ (l1 + 1))) * (b |^ (m2 + 1))) by Th15

            .= ((((n + 1) choose (m2 + 1)) * (a |^ (l1 + 1))) * (b |^ (m2 + 1))) by NEWTON: 22

            .= (((a,b) In_Power (n + 1)) /. i) by A13, A41, Def7

            .= (((a,b) In_Power (n + 1)) . i) by A13, PARTFUN1:def 6;

          end;

          

           A44: i in {1} implies (F . i) = (((a,b) In_Power (n + 1)) . i)

          proof

            assume i in {1};

            then

             A45: i = 1 by TARSKI:def 1;

            

            then

             A46: r2 = (( <*( 0. R)*> ^ (((a,b) In_Power n) * b)) . 1) by A17, PARTFUN1:def 6

            .= ( 0. R) by FINSEQ_1: 41;

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

            then 1 in ( Seg (n + 1)) by FINSEQ_1: 1;

            then

             A47: 1 in ( Seg ( len ((a,b) In_Power n))) by Def7;

            then

             A48: 1 in ( dom ((a,b) In_Power n)) by FINSEQ_1:def 3;

            then

             A49: r = (((a,b) In_Power n) . i) by A45, PARTFUN1:def 6;

            

             A50: 1 in ( dom (((a,b) In_Power n) * a)) by A2, A47, FINSEQ_1:def 3;

            

             A51: r1 = (((((a,b) In_Power n) * a) ^ <*( 0. R)*>) . 1) by A16, A45, PARTFUN1:def 6

            .= ((((a,b) In_Power n) * a) . 1) by A50, FINSEQ_1:def 7

            .= ((((a,b) In_Power n) * a) /. 1) by A50, PARTFUN1:def 6

            .= ((((a,b) In_Power n) /. 1) * a) by A48, POLYNOM1:def 2

            .= ((a |^ n) * a) by A45, A49, Th23

            .= (a |^ (n + 1)) by GROUP_1:def 7;

            

            thus (F . i) = (F /. i) by A29, PARTFUN1:def 6

            .= (r1 + (F2 /. i)) by A9, A18, Def1

            .= (a |^ (n + 1)) by A51, A46, RLVECT_1:def 4

            .= (((a,b) In_Power (n + 1)) . i) by A45, Th23;

          end;

          now

            assume i in (( {1} \/ { k where k be Element of NAT : 1 < k & k < ((n + 1) + 1) }) \/ {((n + 1) + 1)});

            then i in ( {1} \/ { k where k be Element of NAT : 1 < k & k < ((n + 1) + 1) }) or i in {((n + 1) + 1)} by XBOOLE_0:def 3;

            hence thesis by A44, A19, A30, XBOOLE_0:def 3;

          end;

          hence thesis by A12, A13, NAT_1: 12, NEWTON: 1;

        end;

        assume P[n];

        

        then

         A52: ((a + b) |^ (n + 1)) = (( Sum ((a,b) In_Power n)) * (a + b)) by GROUP_1:def 7

        .= ((( Sum ((a,b) In_Power n)) * a) + (( Sum ((a,b) In_Power n)) * b)) by VECTSP_1:def 2

        .= (( Sum (((a,b) In_Power n) * a)) + (( Sum ((a,b) In_Power n)) * b)) by Th5

        .= (( Sum (((a,b) In_Power n) * a)) + ( Sum (((a,b) In_Power n) * b))) by Th5;

        

         A53: ( Sum F1) = (( Sum (((a,b) In_Power n) * a)) + ( Sum <*( 0. R)*>)) by RLVECT_1: 41

        .= (( Sum (((a,b) In_Power n) * a)) + ( 0. R)) by Th3

        .= ( Sum (((a,b) In_Power n) * a)) by RLVECT_1:def 4;

        

         A54: ( Sum F2) = (( Sum <*( 0. R)*>) + ( Sum (((a,b) In_Power n) * b))) by RLVECT_1: 41

        .= (( 0. R) + ( Sum (((a,b) In_Power n) * b))) by Th3

        .= ( Sum (((a,b) In_Power n) * b)) by ALGSTR_1:def 2;

        ( dom F1) = ( Seg ( len F1)) by FINSEQ_1:def 3

        .= ( dom F2) by A4, A5, FINSEQ_1:def 3;

        then

         A55: ( Sum (G1 + G2)) = (( Sum (((a,b) In_Power n) * a)) + ( Sum (((a,b) In_Power n) * b))) by A53, A54, Th7;

        ( len ((a,b) In_Power (n + 1))) = ( len F) by A7, Def7;

        hence thesis by A52, A55, A8, FINSEQ_1: 14;

      end;

      ((a + b) |^ 0 ) = ( 1_ R) by Th8

      .= ( Sum <*( 1_ R)*>) by Th3

      .= ( Sum ((a,b) In_Power 0 )) by Th22;

      then

       A56: P[ 0 ];

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

      hence thesis;

    end;

    theorem :: BINOM:26

    for C,D be non empty set, b be Element of D, F be Function of [:C, D:], D holds ex g be Function of [: NAT , C:], D st for a be Element of C holds (g . ( 0 ,a)) = b & for n be Nat holds (g . ((n + 1),a)) = (F . (a,(g . (n,a)))) by Lm1;

    theorem :: BINOM:27

    for C,D be non empty set, b be Element of D, F be Function of [:D, C:], D holds ex g be Function of [:C, NAT :], D st for a be Element of C holds (g . (a, 0 )) = b & for n be Element of NAT holds (g . (a,(n + 1))) = (F . ((g . (a,n)),a)) by Lm2;