finseqop.miz



    begin

    reserve x,y for set;

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

    reserve c for Element of C;

    reserve c9 for Element of C9;

    reserve d,d1,d2,d3,d4,e for Element of D;

    reserve d9 for Element of D9;

    theorem :: FINSEQOP:1

    

     Th1: for f be Function holds <: {} , f:> = {} & <:f, {} :> = {}

    proof

      let f be Function;

      ( dom <: {} , f:>) = (( dom {} ) /\ ( dom f)) & ( dom <:f, {} :>) = (( dom f) /\ ( dom {} )) by FUNCT_3:def 7;

      hence thesis;

    end;

    theorem :: FINSEQOP:2

    for f be Function holds [: {} , f:] = {} & [:f, {} :] = {}

    proof

      let f be Function;

      ( dom [: {} , f:]) = [:( dom {} ), ( dom f):] & ( dom [:f, {} :]) = [:( dom f), ( dom {} ):] by FUNCT_3:def 8;

      hence thesis by ZFMISC_1: 90;

    end;

    theorem :: FINSEQOP:3

    

     Th3: for F,f be Function holds (F .: ( {} ,f)) = {} & (F .: (f, {} )) = {}

    proof

      let F,f be Function;

      (F .: ( {} ,f)) = (F * {} ) by Th1;

      hence thesis by Th1;

    end;

    theorem :: FINSEQOP:4

    for F be Function holds (F [:] ( {} ,x)) = {}

    proof

      let F be Function;

      (F [:] ( {} ,x)) = (F .: ( {} ,(( dom {} ) --> x)));

      hence thesis by Th3;

    end;

    theorem :: FINSEQOP:5

    for F be Function holds (F [;] (x, {} )) = {}

    proof

      let F be Function;

      (F [;] (x, {} )) = (F .: ((( dom {} ) --> x), {} ));

      hence thesis by Th3;

    end;

    theorem :: FINSEQOP:6

    

     Th6: for X be set, x1,x2 be set holds <:(X --> x1), (X --> x2):> = (X --> [x1, x2])

    proof

      let X be set, x1,x2 be set;

      set f = (X --> x1), g = (X --> x2);

      set fg = <:f, g:>;

      now

        per cases ;

          suppose

           A1: X = {} ;

          thus thesis by A1;

        end;

          suppose

           A2: X <> {} ;

          ( rng fg) c= [: {x1}, {x2}:];

          then

           A3: ( rng fg) c= { [x1, x2]} by ZFMISC_1: 29;

          set x = the Element of X;

          

           A4: ( dom f) = X & ( dom g) = X;

          then

           A5: ( dom fg) = X by FUNCT_3: 50;

          (f . x) = x1 & (g . x) = x2 by A2, FUNCOP_1: 7;

          then (fg . x) = [x1, x2] by A2, A4, FUNCT_3: 49;

          then [x1, x2] in ( rng fg) by A2, A5, FUNCT_1:def 3;

          then { [x1, x2]} c= ( rng fg) by ZFMISC_1: 31;

          then ( rng fg) = { [x1, x2]} by A3, XBOOLE_0:def 10;

          hence thesis by A5, FUNCOP_1: 9;

        end;

      end;

      hence thesis;

    end;

    theorem :: FINSEQOP:7

    

     Th7: for F be Function, X be set, x1,x2 be set st [x1, x2] in ( dom F) holds (F .: ((X --> x1),(X --> x2))) = (X --> (F . (x1,x2)))

    proof

      let F be Function, X be set, x1,x2 be set such that

       A1: [x1, x2] in ( dom F);

      set f = (X --> x1), g = (X --> x2);

      

      thus (F .: (f,g)) = (F * (X --> [x1, x2])) by Th6

      .= (X --> (F . (x1,x2))) by A1, FUNCOP_1: 17;

    end;

    reserve i,j for natural Number;

    reserve F for Function of [:D, D9:], E;

    reserve p,q for FinSequence of D,

p9,q9 for FinSequence of D9;

    definition

      let D, D9, E, F, p, p9;

      :: original: .:

      redefine

      func F .: (p,p9) -> FinSequence of E ;

      coherence by FINSEQ_2: 70;

    end

    definition

      let D, D9, E, F, p, d9;

      :: original: [:]

      redefine

      func F [:] (p,d9) -> FinSequence of E ;

      coherence by FINSEQ_2: 83;

    end

    definition

      let D, D9, E, F, d, p9;

      :: original: [;]

      redefine

      func F [;] (d,p9) -> FinSequence of E ;

      coherence by FINSEQ_2: 77;

    end

    reserve f,f9 for Function of C, D,

h for Function of D, E;

    definition

      let D,E be set, p be FinSequence of D, h be Function of D, E;

      :: original: *

      redefine

      func h * p -> FinSequence of E ;

      coherence by FINSEQ_2: 32;

    end

    theorem :: FINSEQOP:8

    

     Th8: (h * (p ^ <*d*>)) = ((h * p) ^ <*(h . d)*>)

    proof

      set q = (h * (p ^ <*d*>));

      set r = ((h * p) ^ <*(h . d)*>);

      set i = (( len p) + 1);

      

       A1: ( len q) = ( len (p ^ <*d*>)) by FINSEQ_2: 33;

      

       A2: ( len (h * p)) = ( len p) by FINSEQ_2: 33;

      ( len (p ^ <*d*>)) = i by FINSEQ_2: 16;

      then

       A3: ( dom q) = ( Seg i) by A1, FINSEQ_1:def 3;

       A4:

      now

        let j be Nat;

        

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

        

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

        assume

         A7: j in ( dom q);

        now

          per cases by A3, A7, A5, FINSEQ_2: 7;

            suppose

             A8: j in ( dom p);

            

            hence (h . ((p ^ <*d*>) . j)) = (h . (p . j)) by FINSEQ_1:def 7

            .= ((h * p) . j) by A2, A5, A6, A8, FUNCT_1: 12

            .= (r . j) by A2, A5, A6, A8, FINSEQ_1:def 7;

          end;

            suppose

             A9: j = i;

            

            hence (h . ((p ^ <*d*>) . j)) = (h . d) by FINSEQ_1: 42

            .= (r . j) by A2, A9, FINSEQ_1: 42;

          end;

        end;

        hence (q . j) = (r . j) by A7, FUNCT_1: 12;

      end;

      ( len r) = (( len (h * p)) + 1) by FINSEQ_2: 16;

      hence thesis by A1, A2, A4, FINSEQ_2: 9, FINSEQ_2: 16;

    end;

    theorem :: FINSEQOP:9

    (h * (p ^ q)) = ((h * p) ^ (h * q))

    proof

      defpred P[ FinSequence of D] means (h * (p ^ $1)) = ((h * p) ^ (h * $1));

      

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

      proof

        let q, d such that

         A2: (h * (p ^ q)) = ((h * p) ^ (h * q));

        

        thus (h * (p ^ (q ^ <*d*>))) = (h * ((p ^ q) ^ <*d*>)) by FINSEQ_1: 32

        .= ((h * (p ^ q)) ^ <*(h . d)*>) by Th8

        .= ((h * p) ^ ((h * q) ^ <*(h . d)*>)) by A2, FINSEQ_1: 32

        .= ((h * p) ^ (h * (q ^ <*d*>))) by Th8;

      end;

      (h * (p ^ ( <*> D))) = (h * p) by FINSEQ_1: 34

      .= ((h * p) ^ (h * ( <*> D))) by FINSEQ_1: 34;

      then

       A3: P[( <*> D)];

      for q holds P[q] from FINSEQ_2:sch 2( A3, A1);

      hence thesis;

    end;

    reserve T,T1,T2,T3 for Tuple of i, D;

    reserve T9 for Tuple of i, D9;

    reserve S for Tuple of j, D;

    reserve S9 for Tuple of j, D9;

    

     Lm1: for T be Tuple of 0 , D holds (F .: (T,T9)) = ( <*> E)

    proof

      let T be Tuple of 0 , D;

      T = ( <*> D);

      hence thesis by FINSEQ_2: 73;

    end;

    

     Lm2: for T9 be Tuple of 0 , D9 holds (F [;] (d,T9)) = ( <*> E)

    proof

      let T9 be Tuple of 0 , D9;

      T9 = ( <*> D9);

      hence thesis by FINSEQ_2: 79;

    end;

    

     Lm3: for T be Tuple of 0 , D holds (F [:] (T,d9)) = ( <*> E)

    proof

      let T be Tuple of 0 , D;

      T = ( <*> D);

      hence thesis by FINSEQ_2: 85;

    end;

    theorem :: FINSEQOP:10

    

     Th10: (F .: ((T ^ <*d*>),(T9 ^ <*d9*>))) = ((F .: (T,T9)) ^ <*(F . (d,d9))*>)

    proof

      set p = (T ^ <*d*>), q = (T9 ^ <*d9*>), pq = (F .: (T,T9));

      set r = (F .: (p,q)), s = (pq ^ <*(F . (d,d9))*>);

      

       A1: ( len T9) = i by CARD_1:def 7;

      then

       A2: ( len q) = (i + 1) by FINSEQ_2: 16;

      

       A3: ( len T) = i by CARD_1:def 7;

      then

       A4: ( len pq) = i by A1, FINSEQ_2: 72;

      ( len p) = (i + 1) by A3, FINSEQ_2: 16;

      then

       A5: ( len r) = (i + 1) by A2, FINSEQ_2: 72;

      then

       A6: ( dom r) = ( Seg (i + 1)) by FINSEQ_1:def 3;

       A7:

      now

        let j be Nat;

        assume

         A8: j in ( dom r);

        now

          per cases by A6, A8, FINSEQ_2: 7;

            suppose

             A9: j in ( Seg i);

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

            then

             A10: (p . j) = (T . j) by A3, A9, FINSEQ_1:def 7;

            

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

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

            then

             A12: (q . j) = (T9 . j) by A1, A9, FINSEQ_1:def 7;

            j in ( dom pq) by A4, A9, FINSEQ_1:def 3;

            

            hence (F . ((p . j),(q . j))) = (pq . j) by A10, A12, FUNCOP_1: 22

            .= (s . j) by A4, A9, A11, FINSEQ_1:def 7;

          end;

            suppose

             A13: j = (i + 1);

            then (p . j) = d & (q . j) = d9 by A3, A1, FINSEQ_1: 42;

            hence (F . ((p . j),(q . j))) = (s . j) by A4, A13, FINSEQ_1: 42;

          end;

        end;

        hence (r . j) = (s . j) by A8, FUNCOP_1: 22;

      end;

      ( len s) = (( len pq) + 1) by FINSEQ_2: 16;

      hence thesis by A5, A4, A7, FINSEQ_2: 9;

    end;

    theorem :: FINSEQOP:11

    (F .: ((T ^ S),(T9 ^ S9))) = ((F .: (T,T9)) ^ (F .: (S,S9)))

    proof

      

       A0: i is Nat & j is Nat by TARSKI: 1;

      defpred P[ Nat] means for S be Tuple of $1, D, S9 be Tuple of $1, D9 holds (F .: ((T ^ S),(T9 ^ S9))) = ((F .: (T,T9)) ^ (F .: (S,S9)));

      now

        let j such that

         A1: for S, S9 holds (F .: ((T ^ S),(T9 ^ S9))) = ((F .: (T,T9)) ^ (F .: (S,S9)));

        let S be Tuple of (j + 1), D;

        let S9 be Tuple of (j + 1), D9;

        consider S1 be Element of (j -tuples_on D), d such that

         A2: S = (S1 ^ <*d*>) by FINSEQ_2: 117;

        

         A3: (T ^ S) = ((T ^ S1) ^ <*d*>) by A2, FINSEQ_1: 32;

        reconsider S1 as Tuple of j, D;

        consider S19 be Element of (j -tuples_on D9), d9 such that

         A4: S9 = (S19 ^ <*d9*>) by FINSEQ_2: 117;

        

         A5: (T9 ^ S9) = ((T9 ^ S19) ^ <*d9*>) by A4, FINSEQ_1: 32;

        reconsider S19 as Tuple of j, D9;

        

        thus (F .: ((T ^ S),(T9 ^ S9))) = ((F .: ((T ^ S1),(T9 ^ S19))) ^ <*(F . (d,d9))*>) by A3, A5, Th10

        .= (((F .: (T,T9)) ^ (F .: (S1,S19))) ^ <*(F . (d,d9))*>) by A1

        .= ((F .: (T,T9)) ^ ((F .: (S1,S19)) ^ <*(F . (d,d9))*>)) by FINSEQ_1: 32

        .= ((F .: (T,T9)) ^ (F .: (S,S9))) by A2, A4, Th10;

      end;

      then

       A6: for j be Nat st P[j] holds P[(j + 1)];

      now

        let S be Tuple of 0 , D;

        let S9 be Tuple of 0 , D9;

        S = ( <*> D);

        then

         A7: (F .: (S,S9)) = ( <*> E) by FINSEQ_2: 73;

        (T ^ S) = T & (T9 ^ S9) = T9 by FINSEQ_2: 95;

        hence (F .: ((T ^ S),(T9 ^ S9))) = ((F .: (T,T9)) ^ (F .: (S,S9))) by A7, FINSEQ_1: 34;

      end;

      then

       A8: P[ 0 ];

      for j be Nat holds P[j] from NAT_1:sch 2( A8, A6);

      hence thesis by A0;

    end;

    theorem :: FINSEQOP:12

    

     Th12: (F [;] (d,(p9 ^ <*d9*>))) = ((F [;] (d,p9)) ^ <*(F . (d,d9))*>)

    proof

      set pd = (p9 ^ <*d9*>), q = (F [;] (d,p9));

      set r = (F [;] (d,pd)), s = (q ^ <*(F . (d,d9))*>);

      set i = ( len p9);

      

       A1: ( len q) = i by FINSEQ_2: 78;

      ( len pd) = (i + 1) by FINSEQ_2: 16;

      then

       A2: ( len r) = (i + 1) by FINSEQ_2: 78;

      then

       A3: ( dom r) = ( Seg (i + 1)) by FINSEQ_1:def 3;

       A4:

      now

        let j be Nat;

        assume

         A5: j in ( dom r);

        now

          per cases by A3, A5, FINSEQ_2: 7;

            suppose

             A6: j in ( Seg i);

            then

             A7: j in ( dom q) by A1, FINSEQ_1:def 3;

            

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

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

            

            hence (F . (d,(pd . j))) = (F . (d,(p9 . j))) by A6, FINSEQ_1:def 7

            .= (q . j) by A7, FUNCOP_1: 32

            .= (s . j) by A1, A6, A8, FINSEQ_1:def 7;

          end;

            suppose

             A9: j = (i + 1);

            

            hence (F . (d,(pd . j))) = (F . (d,d9)) by FINSEQ_1: 42

            .= (s . j) by A1, A9, FINSEQ_1: 42;

          end;

        end;

        hence (r . j) = (s . j) by A5, FUNCOP_1: 32;

      end;

      ( len s) = (( len q) + 1) by FINSEQ_2: 16;

      hence thesis by A1, A2, A4, FINSEQ_2: 9;

    end;

    theorem :: FINSEQOP:13

    (F [;] (d,(p9 ^ q9))) = ((F [;] (d,p9)) ^ (F [;] (d,q9)))

    proof

      defpred P[ FinSequence of D9] means (F [;] (d,(p9 ^ $1))) = ((F [;] (d,p9)) ^ (F [;] (d,$1)));

      

       A1: for q9, d9 st P[q9] holds P[(q9 ^ <*d9*>)]

      proof

        let q9, d9 such that

         A2: (F [;] (d,(p9 ^ q9))) = ((F [;] (d,p9)) ^ (F [;] (d,q9)));

        

        thus (F [;] (d,(p9 ^ (q9 ^ <*d9*>)))) = (F [;] (d,((p9 ^ q9) ^ <*d9*>))) by FINSEQ_1: 32

        .= ((F [;] (d,(p9 ^ q9))) ^ <*(F . (d,d9))*>) by Th12

        .= ((F [;] (d,p9)) ^ ((F [;] (d,q9)) ^ <*(F . (d,d9))*>)) by A2, FINSEQ_1: 32

        .= ((F [;] (d,p9)) ^ (F [;] (d,(q9 ^ <*d9*>)))) by Th12;

      end;

      (F [;] (d,(p9 ^ ( <*> D9)))) = (F [;] (d,p9)) by FINSEQ_1: 34

      .= ((F [;] (d,p9)) ^ ( <*> E)) by FINSEQ_1: 34

      .= ((F [;] (d,p9)) ^ (F [;] (d,( <*> D9)))) by FINSEQ_2: 79;

      then

       A3: P[( <*> D9)];

      for q9 holds P[q9] from FINSEQ_2:sch 2( A3, A1);

      hence thesis;

    end;

    theorem :: FINSEQOP:14

    

     Th14: (F [:] ((p ^ <*d*>),d9)) = ((F [:] (p,d9)) ^ <*(F . (d,d9))*>)

    proof

      set pd = (p ^ <*d*>), q = (F [:] (p,d9));

      set r = (F [:] (pd,d9)), s = (q ^ <*(F . (d,d9))*>);

      set i = ( len p);

      

       A1: ( len q) = i by FINSEQ_2: 84;

      ( len pd) = (i + 1) by FINSEQ_2: 16;

      then

       A2: ( len r) = (i + 1) by FINSEQ_2: 84;

      then

       A3: ( dom r) = ( Seg (i + 1)) by FINSEQ_1:def 3;

       A4:

      now

        let j be Nat;

        assume

         A5: j in ( dom r);

        now

          per cases by A3, A5, FINSEQ_2: 7;

            suppose

             A6: j in ( Seg i);

            then

             A7: j in ( dom q) by A1, FINSEQ_1:def 3;

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

            

            hence (F . ((pd . j),d9)) = (F . ((p . j),d9)) by A6, FINSEQ_1:def 7

            .= (q . j) by A7, FUNCOP_1: 27

            .= (s . j) by A7, FINSEQ_1:def 7;

          end;

            suppose

             A8: j = (i + 1);

            

            hence (F . ((pd . j),d9)) = (F . (d,d9)) by FINSEQ_1: 42

            .= (s . j) by A1, A8, FINSEQ_1: 42;

          end;

        end;

        hence (r . j) = (s . j) by A5, FUNCOP_1: 27;

      end;

      ( len s) = (( len q) + 1) by FINSEQ_2: 16;

      hence thesis by A1, A2, A4, FINSEQ_2: 9;

    end;

    theorem :: FINSEQOP:15

    (F [:] ((p ^ q),d9)) = ((F [:] (p,d9)) ^ (F [:] (q,d9)))

    proof

      defpred P[ FinSequence of D] means (F [:] ((p ^ $1),d9)) = ((F [:] (p,d9)) ^ (F [:] ($1,d9)));

      

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

      proof

        let q, d such that

         A2: (F [:] ((p ^ q),d9)) = ((F [:] (p,d9)) ^ (F [:] (q,d9)));

        

        thus (F [:] ((p ^ (q ^ <*d*>)),d9)) = (F [:] (((p ^ q) ^ <*d*>),d9)) by FINSEQ_1: 32

        .= ((F [:] ((p ^ q),d9)) ^ <*(F . (d,d9))*>) by Th14

        .= ((F [:] (p,d9)) ^ ((F [:] (q,d9)) ^ <*(F . (d,d9))*>)) by A2, FINSEQ_1: 32

        .= ((F [:] (p,d9)) ^ (F [:] ((q ^ <*d*>),d9))) by Th14;

      end;

      (F [:] ((p ^ ( <*> D)),d9)) = (F [:] (p,d9)) by FINSEQ_1: 34

      .= ((F [:] (p,d9)) ^ ( <*> E)) by FINSEQ_1: 34

      .= ((F [:] (p,d9)) ^ (F [:] (( <*> D),d9))) by FINSEQ_2: 85;

      then

       A3: P[( <*> D)];

      for q holds P[q] from FINSEQ_2:sch 2( A3, A1);

      hence thesis;

    end;

    theorem :: FINSEQOP:16

    for h be Function of D, E holds (h * (i |-> d)) = (i |-> (h . d))

    proof

      let h be Function of D, E;

      d in D;

      then d in ( dom h) by FUNCT_2:def 1;

      hence thesis by FUNCOP_1: 17;

    end;

    theorem :: FINSEQOP:17

    

     Th17: (F .: ((i |-> d),(i |-> d9))) = (i |-> (F . (d,d9)))

    proof

       [d, d9] in [:D, D9:] by ZFMISC_1:def 2;

      then [d, d9] in ( dom F) by FUNCT_2:def 1;

      hence thesis by Th7;

    end;

    theorem :: FINSEQOP:18

    (F [;] (d,(i |-> d9))) = (i |-> (F . (d,d9)))

    proof

      

      thus (F [;] (d,(i |-> d9))) = (F .: ((i |-> d),(i |-> d9)))

      .= (i |-> (F . (d,d9))) by Th17;

    end;

    theorem :: FINSEQOP:19

    (F [:] ((i |-> d),d9)) = (i |-> (F . (d,d9)))

    proof

      

      thus (F [:] ((i |-> d),d9)) = (F .: ((i |-> d),(i |-> d9)))

      .= (i |-> (F . (d,d9))) by Th17;

    end;

    theorem :: FINSEQOP:20

    (F .: ((i |-> d),T9)) = (F [;] (d,T9))

    proof

      ( dom T9) = ( Seg ( len T9)) by FINSEQ_1:def 3

      .= ( Seg i) by CARD_1:def 7;

      hence thesis;

    end;

    theorem :: FINSEQOP:21

    (F .: (T,(i |-> d))) = (F [:] (T,d))

    proof

      ( dom T) = ( Seg ( len T)) by FINSEQ_1:def 3

      .= ( Seg i) by CARD_1:def 7;

      hence thesis;

    end;

    theorem :: FINSEQOP:22

    (F [;] (d,T9)) = ((F [;] (d,( id D9))) * T9)

    proof

      ( rng T9) c= D9;

      

      hence (F [;] (d,T9)) = (F [;] (d,(( id D9) * T9))) by RELAT_1: 53

      .= ((F [;] (d,( id D9))) * T9) by FUNCOP_1: 34;

    end;

    theorem :: FINSEQOP:23

    (F [:] (T,d)) = ((F [:] (( id D),d)) * T)

    proof

      ( rng T) c= D;

      

      hence (F [:] (T,d)) = (F [:] ((( id D) * T),d)) by RELAT_1: 53

      .= ((F [:] (( id D),d)) * T) by FUNCOP_1: 29;

    end;

    reserve F,G for BinOp of D;

    reserve u for UnOp of D;

    reserve H for BinOp of E;

    

     Lm4: T is Function of ( Seg i), D

    proof

      ( len T) = i by CARD_1:def 7;

      then ( Seg i) = ( dom T) by FINSEQ_1:def 3;

      hence thesis by FINSEQ_2: 26;

    end;

    theorem :: FINSEQOP:24

    

     Th24: F is associative implies ((F [;] (d,( id D))) * (F .: (f,f9))) = (F .: (((F [;] (d,( id D))) * f),f9))

    proof

      assume

       A1: F is associative;

      now

        let c;

        

        thus (((F [;] (d,( id D))) * (F .: (f,f9))) . c) = ((F [;] (d,( id D))) . ((F .: (f,f9)) . c)) by FUNCT_2: 15

        .= ((F [;] (d,( id D))) . (F . ((f . c),(f9 . c)))) by FUNCOP_1: 37

        .= (F . (d,(( id D) . (F . ((f . c),(f9 . c)))))) by FUNCOP_1: 53

        .= (F . (d,(F . ((f . c),(f9 . c)))))

        .= (F . ((F . (d,(f . c))),(f9 . c))) by A1

        .= (F . (((F [;] (d,f)) . c),(f9 . c))) by FUNCOP_1: 53

        .= (F . ((((F [;] (d,( id D))) * f) . c),(f9 . c))) by FUNCOP_1: 55

        .= ((F .: (((F [;] (d,( id D))) * f),f9)) . c) by FUNCOP_1: 37;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: FINSEQOP:25

    

     Th25: F is associative implies ((F [:] (( id D),d)) * (F .: (f,f9))) = (F .: (f,((F [:] (( id D),d)) * f9)))

    proof

      assume

       A1: F is associative;

      now

        let c;

        

        thus (((F [:] (( id D),d)) * (F .: (f,f9))) . c) = ((F [:] (( id D),d)) . ((F .: (f,f9)) . c)) by FUNCT_2: 15

        .= ((F [:] (( id D),d)) . (F . ((f . c),(f9 . c)))) by FUNCOP_1: 37

        .= (F . ((( id D) . (F . ((f . c),(f9 . c)))),d)) by FUNCOP_1: 48

        .= (F . ((F . ((f . c),(f9 . c))),d))

        .= (F . ((f . c),(F . ((f9 . c),d)))) by A1

        .= (F . ((f . c),((F [:] (f9,d)) . c))) by FUNCOP_1: 48

        .= (F . ((f . c),(((F [:] (( id D),d)) * f9) . c))) by FUNCOP_1: 50

        .= ((F .: (f,((F [:] (( id D),d)) * f9))) . c) by FUNCOP_1: 37;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: FINSEQOP:26

    F is associative implies ((F [;] (d,( id D))) * (F .: (T1,T2))) = (F .: (((F [;] (d,( id D))) * T1),T2))

    proof

      assume

       A1: F is associative;

      per cases ;

        suppose

         A2: i = 0 ;

        then (F .: (T1,T2)) = ( <*> D) by Lm1;

        then

         A3: ((F [;] (d,( id D))) * (F .: (T1,T2))) = ( <*> D);

        T2 = ( <*> D) by A2;

        hence thesis by A3, FINSEQ_2: 73;

      end;

        suppose i <> 0 ;

        then

        reconsider C = ( Seg i) as non empty set;

        T1 is Function of C, D & T2 is Function of C, D by Lm4;

        hence thesis by A1, Th24;

      end;

    end;

    theorem :: FINSEQOP:27

    F is associative implies ((F [:] (( id D),d)) * (F .: (T1,T2))) = (F .: (T1,((F [:] (( id D),d)) * T2)))

    proof

      assume

       A1: F is associative;

      per cases ;

        suppose

         A2: i = 0 ;

        then (F .: (T1,T2)) = ( <*> D) by Lm1;

        then

         A3: ((F [:] (( id D),d)) * (F .: (T1,T2))) = ( <*> D);

        T1 = ( <*> D) by A2;

        hence thesis by A3, FINSEQ_2: 73;

      end;

        suppose i <> 0 ;

        then

        reconsider C = ( Seg i) as non empty set;

        T1 is Function of C, D & T2 is Function of C, D by Lm4;

        hence thesis by A1, Th25;

      end;

    end;

    theorem :: FINSEQOP:28

    F is associative implies (F .: ((F .: (T1,T2)),T3)) = (F .: (T1,(F .: (T2,T3))))

    proof

      assume

       A1: F is associative;

      per cases ;

        suppose

         A2: i = 0 ;

        then (F .: (T1,T2)) = ( <*> D) by Lm1;

        then

         A3: (F .: ((F .: (T1,T2)),T3)) = ( <*> D) by FINSEQ_2: 73;

        (F .: (T2,T3)) = ( <*> D) by A2, Lm1;

        hence thesis by A3, FINSEQ_2: 73;

      end;

        suppose i <> 0 ;

        then

        reconsider C = ( Seg i) as non empty set;

        

         A4: T3 is Function of C, D by Lm4;

        T1 is Function of C, D & T2 is Function of C, D by Lm4;

        hence thesis by A1, A4, FUNCOP_1: 61;

      end;

    end;

    theorem :: FINSEQOP:29

    F is associative implies (F [:] ((F [;] (d1,T)),d2)) = (F [;] (d1,(F [:] (T,d2))))

    proof

      assume

       A1: F is associative;

      per cases ;

        suppose

         A2: i = 0 ;

        then (F [;] (d1,T)) = ( <*> D) by Lm2;

        then

         A3: (F [:] ((F [;] (d1,T)),d2)) = ( <*> D) by FINSEQ_2: 85;

        (F [:] (T,d2)) = ( <*> D) by A2, Lm3;

        hence thesis by A3, FINSEQ_2: 79;

      end;

        suppose i <> 0 ;

        then

        reconsider C = ( Seg i) as non empty set;

        T is Function of C, D by Lm4;

        hence thesis by A1, FUNCOP_1: 59;

      end;

    end;

    theorem :: FINSEQOP:30

    F is associative implies (F .: ((F [:] (T1,d)),T2)) = (F .: (T1,(F [;] (d,T2))))

    proof

      assume

       A1: F is associative;

      per cases ;

        suppose

         A2: i = 0 ;

        then (F [:] (T1,d)) = ( <*> D) by Lm3;

        then

         A3: (F .: ((F [:] (T1,d)),T2)) = ( <*> D) by FINSEQ_2: 73;

        (F [;] (d,T2)) = ( <*> D) by A2, Lm2;

        hence thesis by A3, FINSEQ_2: 73;

      end;

        suppose i <> 0 ;

        then

        reconsider C = ( Seg i) as non empty set;

        T1 is Function of C, D & T2 is Function of C, D by Lm4;

        hence thesis by A1, FUNCOP_1: 60;

      end;

    end;

    theorem :: FINSEQOP:31

    F is associative implies (F [;] ((F . (d1,d2)),T)) = (F [;] (d1,(F [;] (d2,T))))

    proof

      assume

       A1: F is associative;

      per cases ;

        suppose i = 0 ;

        then T = ( <*> D) & (F [;] (d2,T)) = ( <*> D) by Lm2;

        hence thesis;

      end;

        suppose i <> 0 ;

        then

        reconsider C = ( Seg i) as non empty set;

        T is Function of C, D by Lm4;

        hence thesis by A1, FUNCOP_1: 62;

      end;

    end;

    theorem :: FINSEQOP:32

    F is associative implies (F [:] (T,(F . (d1,d2)))) = (F [:] ((F [:] (T,d1)),d2))

    proof

      assume

       A1: F is associative;

      per cases ;

        suppose i = 0 ;

        then T = ( <*> D) & (F [:] (T,d1)) = ( <*> D) by Lm3;

        hence thesis;

      end;

        suppose i <> 0 ;

        then

        reconsider C = ( Seg i) as non empty set;

        T is Function of C, D by Lm4;

        hence thesis by A1, FUNCOP_1: 63;

      end;

    end;

    theorem :: FINSEQOP:33

    F is commutative implies (F .: (T1,T2)) = (F .: (T2,T1))

    proof

      assume

       A1: F is commutative;

      per cases ;

        suppose

         A2: i = 0 ;

        then (F .: (T1,T2)) = ( <*> D) by Lm1;

        hence thesis by A2, Lm1;

      end;

        suppose i <> 0 ;

        then

        reconsider C = ( Seg i) as non empty set;

        T1 is Function of C, D & T2 is Function of C, D by Lm4;

        hence thesis by A1, FUNCOP_1: 65;

      end;

    end;

    theorem :: FINSEQOP:34

    F is commutative implies (F [;] (d,T)) = (F [:] (T,d))

    proof

      assume

       A1: F is commutative;

      per cases ;

        suppose

         A2: i = 0 ;

        then (F [;] (d,T)) = ( <*> D) by Lm2;

        hence thesis by A2, Lm3;

      end;

        suppose i <> 0 ;

        then

        reconsider C = ( Seg i) as non empty set;

        T is Function of C, D by Lm4;

        hence thesis by A1, FUNCOP_1: 64;

      end;

    end;

    theorem :: FINSEQOP:35

    

     Th35: F is_distributive_wrt G implies (F [;] ((G . (d1,d2)),f)) = (G .: ((F [;] (d1,f)),(F [;] (d2,f))))

    proof

      assume

       A1: F is_distributive_wrt G;

      now

        let c;

        

        thus ((F [;] ((G . (d1,d2)),f)) . c) = (F . ((G . (d1,d2)),(f . c))) by FUNCOP_1: 53

        .= (G . ((F . (d1,(f . c))),(F . (d2,(f . c))))) by A1, BINOP_1: 11

        .= (G . (((F [;] (d1,f)) . c),(F . (d2,(f . c))))) by FUNCOP_1: 53

        .= (G . (((F [;] (d1,f)) . c),((F [;] (d2,f)) . c))) by FUNCOP_1: 53

        .= ((G .: ((F [;] (d1,f)),(F [;] (d2,f)))) . c) by FUNCOP_1: 37;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: FINSEQOP:36

    

     Th36: F is_distributive_wrt G implies (F [:] (f,(G . (d1,d2)))) = (G .: ((F [:] (f,d1)),(F [:] (f,d2))))

    proof

      assume

       A1: F is_distributive_wrt G;

      now

        let c;

        

        thus ((F [:] (f,(G . (d1,d2)))) . c) = (F . ((f . c),(G . (d1,d2)))) by FUNCOP_1: 48

        .= (G . ((F . ((f . c),d1)),(F . ((f . c),d2)))) by A1, BINOP_1: 11

        .= (G . (((F [:] (f,d1)) . c),(F . ((f . c),d2)))) by FUNCOP_1: 48

        .= (G . (((F [:] (f,d1)) . c),((F [:] (f,d2)) . c))) by FUNCOP_1: 48

        .= ((G .: ((F [:] (f,d1)),(F [:] (f,d2)))) . c) by FUNCOP_1: 37;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: FINSEQOP:37

    

     Th37: (for d1, d2 holds (h . (F . (d1,d2))) = (H . ((h . d1),(h . d2)))) implies (h * (F .: (f,f9))) = (H .: ((h * f),(h * f9)))

    proof

      assume

       A1: for d1, d2 holds (h . (F . (d1,d2))) = (H . ((h . d1),(h . d2)));

      now

        let c;

        

        thus ((h * (F .: (f,f9))) . c) = (h . ((F .: (f,f9)) . c)) by FUNCT_2: 15

        .= (h . (F . ((f . c),(f9 . c)))) by FUNCOP_1: 37

        .= (H . ((h . (f . c)),(h . (f9 . c)))) by A1

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

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

        .= ((H .: ((h * f),(h * f9))) . c) by FUNCOP_1: 37;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: FINSEQOP:38

    

     Th38: (for d1, d2 holds (h . (F . (d1,d2))) = (H . ((h . d1),(h . d2)))) implies (h * (F [;] (d,f))) = (H [;] ((h . d),(h * f)))

    proof

      assume

       A1: for d1, d2 holds (h . (F . (d1,d2))) = (H . ((h . d1),(h . d2)));

      reconsider g = (C --> d) as Function of C, D;

      

       A2: ( dom h) = D & ( dom (h * f)) = C by FUNCT_2:def 1;

      

      thus (h * (F [;] (d,f))) = (h * (F .: (g,f))) by FUNCT_2:def 1

      .= (H .: ((h * g),(h * f))) by A1, Th37

      .= (H [;] ((h . d),(h * f))) by A2, FUNCOP_1: 17;

    end;

    theorem :: FINSEQOP:39

    

     Th39: (for d1, d2 holds (h . (F . (d1,d2))) = (H . ((h . d1),(h . d2)))) implies (h * (F [:] (f,d))) = (H [:] ((h * f),(h . d)))

    proof

      assume

       A1: for d1, d2 holds (h . (F . (d1,d2))) = (H . ((h . d1),(h . d2)));

      reconsider g = (C --> d) as Function of C, D;

      

       A2: ( dom h) = D & ( dom (h * f)) = C by FUNCT_2:def 1;

      

      thus (h * (F [:] (f,d))) = (h * (F .: (f,g))) by FUNCT_2:def 1

      .= (H .: ((h * f),(h * g))) by A1, Th37

      .= (H [:] ((h * f),(h . d))) by A2, FUNCOP_1: 17;

    end;

    theorem :: FINSEQOP:40

    u is_distributive_wrt F implies (u * (F .: (f,f9))) = (F .: ((u * f),(u * f9))) by Th37;

    theorem :: FINSEQOP:41

    u is_distributive_wrt F implies (u * (F [;] (d,f))) = (F [;] ((u . d),(u * f))) by Th38;

    theorem :: FINSEQOP:42

    u is_distributive_wrt F implies (u * (F [:] (f,d))) = (F [:] ((u * f),(u . d))) by Th39;

    theorem :: FINSEQOP:43

    

     Th43: F is having_a_unity implies (F .: ((C --> ( the_unity_wrt F)),f)) = f & (F .: (f,(C --> ( the_unity_wrt F)))) = f

    proof

      set e = ( the_unity_wrt F);

      reconsider g = (C --> e) as Function of C, D;

      assume

       A1: F is having_a_unity;

      now

        let c;

        

        thus ((F .: (g,f)) . c) = (F . ((g . c),(f . c))) by FUNCOP_1: 37

        .= (F . (e,(f . c)))

        .= (f . c) by A1, SETWISEO: 15;

      end;

      hence (F .: ((C --> e),f)) = f by FUNCT_2: 63;

      now

        let c;

        

        thus ((F .: (f,g)) . c) = (F . ((f . c),(g . c))) by FUNCOP_1: 37

        .= (F . ((f . c),e))

        .= (f . c) by A1, SETWISEO: 15;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: FINSEQOP:44

    

     Th44: F is having_a_unity implies (F [;] (( the_unity_wrt F),f)) = f

    proof

      set e = ( the_unity_wrt F);

      assume

       A1: F is having_a_unity;

      now

        let c;

        

        thus ((F [;] (e,f)) . c) = (F . (e,(f . c))) by FUNCOP_1: 53

        .= (f . c) by A1, SETWISEO: 15;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: FINSEQOP:45

    

     Th45: F is having_a_unity implies (F [:] (f,( the_unity_wrt F))) = f

    proof

      set e = ( the_unity_wrt F);

      assume

       A1: F is having_a_unity;

      now

        let c;

        

        thus ((F [:] (f,e)) . c) = (F . ((f . c),e)) by FUNCOP_1: 48

        .= (f . c) by A1, SETWISEO: 15;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: FINSEQOP:46

    F is_distributive_wrt G implies (F [;] ((G . (d1,d2)),T)) = (G .: ((F [;] (d1,T)),(F [;] (d2,T))))

    proof

      assume

       A1: F is_distributive_wrt G;

      per cases ;

        suppose i = 0 ;

        then (F [;] (d1,T)) = ( <*> D) & (F [;] ((G . (d1,d2)),T)) = ( <*> D) by Lm2;

        hence thesis by FINSEQ_2: 73;

      end;

        suppose i <> 0 ;

        then

        reconsider C = ( Seg i) as non empty set;

        T is Function of C, D by Lm4;

        hence thesis by A1, Th35;

      end;

    end;

    theorem :: FINSEQOP:47

    F is_distributive_wrt G implies (F [:] (T,(G . (d1,d2)))) = (G .: ((F [:] (T,d1)),(F [:] (T,d2))))

    proof

      assume

       A1: F is_distributive_wrt G;

      per cases ;

        suppose i = 0 ;

        then (F [:] (T,d1)) = ( <*> D) & (F [:] (T,(G . (d1,d2)))) = ( <*> D) by Lm3;

        hence thesis by FINSEQ_2: 73;

      end;

        suppose i <> 0 ;

        then

        reconsider C = ( Seg i) as non empty set;

        T is Function of C, D by Lm4;

        hence thesis by A1, Th36;

      end;

    end;

    theorem :: FINSEQOP:48

    

     Th48: (for d1, d2 holds (h . (F . (d1,d2))) = (H . ((h . d1),(h . d2)))) implies (h * (F .: (T1,T2))) = (H .: ((h * T1),(h * T2)))

    proof

      assume

       A1: for d1, d2 holds (h . (F . (d1,d2))) = (H . ((h . d1),(h . d2)));

      per cases ;

        suppose

         A2: i = 0 ;

        then (F .: (T1,T2)) = ( <*> D) by Lm1;

        then

         A3: (h * (F .: (T1,T2))) = ( <*> E);

        (h * T1) = ( <*> E) by A2;

        hence thesis by A3, FINSEQ_2: 73;

      end;

        suppose i <> 0 ;

        then

        reconsider C = ( Seg i) as non empty set;

        T1 is Function of C, D & T2 is Function of C, D by Lm4;

        hence thesis by A1, Th37;

      end;

    end;

    theorem :: FINSEQOP:49

    

     Th49: (for d1, d2 holds (h . (F . (d1,d2))) = (H . ((h . d1),(h . d2)))) implies (h * (F [;] (d,T))) = (H [;] ((h . d),(h * T)))

    proof

      assume

       A1: for d1, d2 holds (h . (F . (d1,d2))) = (H . ((h . d1),(h . d2)));

      per cases ;

        suppose

         A2: i = 0 ;

        then (F [;] (d,T)) = ( <*> D) by Lm2;

        then

         A3: (h * (F [;] (d,T))) = ( <*> E);

        (h * T) = ( <*> E) by A2;

        hence thesis by A3, FINSEQ_2: 79;

      end;

        suppose i <> 0 ;

        then

        reconsider C = ( Seg i) as non empty set;

        T is Function of C, D by Lm4;

        hence thesis by A1, Th38;

      end;

    end;

    theorem :: FINSEQOP:50

    

     Th50: (for d1, d2 holds (h . (F . (d1,d2))) = (H . ((h . d1),(h . d2)))) implies (h * (F [:] (T,d))) = (H [:] ((h * T),(h . d)))

    proof

      assume

       A1: for d1, d2 holds (h . (F . (d1,d2))) = (H . ((h . d1),(h . d2)));

      per cases ;

        suppose

         A2: i = 0 ;

        then (F [:] (T,d)) = ( <*> D) by Lm3;

        then

         A3: (h * (F [:] (T,d))) = ( <*> E);

        (h * T) = ( <*> E) by A2;

        hence thesis by A3, FINSEQ_2: 85;

      end;

        suppose i <> 0 ;

        then

        reconsider C = ( Seg i) as non empty set;

        T is Function of C, D by Lm4;

        hence thesis by A1, Th39;

      end;

    end;

    theorem :: FINSEQOP:51

    u is_distributive_wrt F implies (u * (F .: (T1,T2))) = (F .: ((u * T1),(u * T2))) by Th48;

    theorem :: FINSEQOP:52

    u is_distributive_wrt F implies (u * (F [;] (d,T))) = (F [;] ((u . d),(u * T))) by Th49;

    theorem :: FINSEQOP:53

    u is_distributive_wrt F implies (u * (F [:] (T,d))) = (F [:] ((u * T),(u . d))) by Th50;

    theorem :: FINSEQOP:54

    G is_distributive_wrt F & u = (G [;] (d,( id D))) implies u is_distributive_wrt F

    proof

      assume that

       A1: G is_distributive_wrt F and

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

      let d1, d2;

      

      thus (u . (F . (d1,d2))) = (G . (d,(( id D) . (F . (d1,d2))))) by A2, FUNCOP_1: 53

      .= (G . (d,(F . (d1,d2))))

      .= (F . ((G . (d,d1)),(G . (d,d2)))) by A1, BINOP_1: 11

      .= (F . ((G . (d,(( id D) . d1))),(G . (d,d2))))

      .= (F . ((G . (d,(( id D) . d1))),(G . (d,(( id D) . d2)))))

      .= (F . ((u . d1),(G . (d,(( id D) . d2))))) by A2, FUNCOP_1: 53

      .= (F . ((u . d1),(u . d2))) by A2, FUNCOP_1: 53;

    end;

    theorem :: FINSEQOP:55

    G is_distributive_wrt F & u = (G [:] (( id D),d)) implies u is_distributive_wrt F

    proof

      assume that

       A1: G is_distributive_wrt F and

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

      let d1, d2;

      

      thus (u . (F . (d1,d2))) = (G . ((( id D) . (F . (d1,d2))),d)) by A2, FUNCOP_1: 48

      .= (G . ((F . (d1,d2)),d))

      .= (F . ((G . (d1,d)),(G . (d2,d)))) by A1, BINOP_1: 11

      .= (F . ((G . ((( id D) . d1),d)),(G . (d2,d))))

      .= (F . ((G . ((( id D) . d1),d)),(G . ((( id D) . d2),d))))

      .= (F . ((u . d1),(G . ((( id D) . d2),d)))) by A2, FUNCOP_1: 48

      .= (F . ((u . d1),(u . d2))) by A2, FUNCOP_1: 48;

    end;

    theorem :: FINSEQOP:56

    F is having_a_unity implies (F .: ((i |-> ( the_unity_wrt F)),T)) = T & (F .: (T,(i |-> ( the_unity_wrt F)))) = T

    proof

      assume

       A1: F is having_a_unity;

      per cases ;

        suppose

         A2: i = 0 ;

        then T = ( <*> D);

        hence thesis by A2, Lm1;

      end;

        suppose i <> 0 ;

        then

        reconsider C = ( Seg i) as non empty set;

        T is Function of C, D by Lm4;

        hence thesis by A1, Th43;

      end;

    end;

    theorem :: FINSEQOP:57

    F is having_a_unity implies (F [;] (( the_unity_wrt F),T)) = T

    proof

      assume

       A1: F is having_a_unity;

      per cases ;

        suppose i = 0 ;

        then T = ( <*> D);

        hence thesis by Lm2;

      end;

        suppose i <> 0 ;

        then

        reconsider C = ( Seg i) as non empty set;

        T is Function of C, D by Lm4;

        hence thesis by A1, Th44;

      end;

    end;

    theorem :: FINSEQOP:58

    F is having_a_unity implies (F [:] (T,( the_unity_wrt F))) = T

    proof

      assume

       A1: F is having_a_unity;

      per cases ;

        suppose i = 0 ;

        then T = ( <*> D);

        hence thesis by Lm3;

      end;

        suppose i <> 0 ;

        then

        reconsider C = ( Seg i) as non empty set;

        T is Function of C, D by Lm4;

        hence thesis by A1, Th45;

      end;

    end;

    definition

      let D, u, F;

      :: FINSEQOP:def1

      pred u is_an_inverseOp_wrt F means for d holds (F . (d,(u . d))) = ( the_unity_wrt F) & (F . ((u . d),d)) = ( the_unity_wrt F);

    end

    definition

      let D, F;

      :: FINSEQOP:def2

      attr F is having_an_inverseOp means ex u st u is_an_inverseOp_wrt F;

    end

    definition

      let D, F;

      assume that

       A1: F is having_a_unity and

       A2: F is associative and

       A3: F is having_an_inverseOp;

      :: FINSEQOP:def3

      func the_inverseOp_wrt F -> UnOp of D means

      : Def3: it is_an_inverseOp_wrt F;

      existence by A3;

      uniqueness

      proof

        set e = ( the_unity_wrt F);

        let u1,u2 be UnOp of D such that

         A4: for d holds (F . (d,(u1 . d))) = e & (F . ((u1 . d),d)) = e and

         A5: for d holds (F . (d,(u2 . d))) = e & (F . ((u2 . d),d)) = e;

        now

          let d;

          set d1 = (u1 . d), d2 = (u2 . d);

          

          thus (u1 . d) = (F . (d1,e)) by A1, SETWISEO: 15

          .= (F . (d1,(F . (d,d2)))) by A5

          .= (F . ((F . (d1,d)),d2)) by A2

          .= (F . (e,d2)) by A4

          .= (u2 . d) by A1, SETWISEO: 15;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    theorem :: FINSEQOP:59

    

     Th59: F is having_a_unity & F is associative & F is having_an_inverseOp implies (F . ((( the_inverseOp_wrt F) . d),d)) = ( the_unity_wrt F) & (F . (d,(( the_inverseOp_wrt F) . d))) = ( the_unity_wrt F)

    proof

      assume F is having_a_unity & F is associative & F is having_an_inverseOp;

      then ( the_inverseOp_wrt F) is_an_inverseOp_wrt F by Def3;

      hence thesis;

    end;

    theorem :: FINSEQOP:60

    

     Th60: F is having_a_unity & F is associative & F is having_an_inverseOp & (F . (d1,d2)) = ( the_unity_wrt F) implies d1 = (( the_inverseOp_wrt F) . d2) & (( the_inverseOp_wrt F) . d1) = d2

    proof

      assume that

       A1: F is having_a_unity and

       A2: F is associative and

       A3: F is having_an_inverseOp and

       A4: (F . (d1,d2)) = ( the_unity_wrt F);

      set e = ( the_unity_wrt F), d3 = (( the_inverseOp_wrt F) . d2);

      (F . ((F . (d1,d2)),d3)) = d3 by A1, A4, SETWISEO: 15;

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

      then (F . (d1,e)) = d3 by A1, A2, A3, Th59;

      hence d1 = d3 by A1, SETWISEO: 15;

      set d3 = (( the_inverseOp_wrt F) . d1);

      (F . (d3,(F . (d1,d2)))) = d3 by A1, A4, SETWISEO: 15;

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

      then (F . (e,d2)) = d3 by A1, A2, A3, Th59;

      hence thesis by A1, SETWISEO: 15;

    end;

    theorem :: FINSEQOP:61

    

     Th61: F is having_a_unity & F is associative & F is having_an_inverseOp implies (( the_inverseOp_wrt F) . ( the_unity_wrt F)) = ( the_unity_wrt F)

    proof

      assume that

       A1: F is having_a_unity and

       A2: F is associative & F is having_an_inverseOp;

      set e = ( the_unity_wrt F);

      (F . (e,e)) = e by A1, SETWISEO: 15;

      hence thesis by A1, A2, Th60;

    end;

    theorem :: FINSEQOP:62

    

     Th62: F is having_a_unity & F is associative & F is having_an_inverseOp implies (( the_inverseOp_wrt F) . (( the_inverseOp_wrt F) . d)) = d

    proof

      assume

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

      then (F . (d,(( the_inverseOp_wrt F) . d))) = ( the_unity_wrt F) by Th59;

      hence thesis by A1, Th60;

    end;

    theorem :: FINSEQOP:63

    

     Th63: F is having_a_unity & F is associative & F is commutative & F is having_an_inverseOp implies ( the_inverseOp_wrt F) is_distributive_wrt F

    proof

      assume that

       A1: F is having_a_unity and

       A2: F is associative and

       A3: F is commutative and

       A4: F is having_an_inverseOp;

      let d1, d2;

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

      (F . ((F . ((u . d1),(u . d2))),(F . (d1,d2)))) = (F . ((u . d1),(F . ((u . d2),(F . (d1,d2)))))) by A2

      .= (F . ((u . d1),(F . ((F . ((u . d2),d1)),d2)))) by A2

      .= (F . ((u . d1),(F . ((F . (d1,(u . d2))),d2)))) by A3

      .= (F . ((u . d1),(F . (d1,(F . ((u . d2),d2)))))) by A2

      .= (F . ((u . d1),(F . (d1,e)))) by A1, A2, A4, Th59

      .= (F . ((F . ((u . d1),d1)),e)) by A2

      .= (F . (e,e)) by A1, A2, A4, Th59

      .= e by A1, SETWISEO: 15;

      hence (u . (F . (d1,d2))) = (F . ((u . d1),(u . d2))) by A1, A2, A4, Th60;

    end;

    theorem :: FINSEQOP:64

    

     Th64: F is having_a_unity & F is associative & F is having_an_inverseOp & ((F . (d,d1)) = (F . (d,d2)) or (F . (d1,d)) = (F . (d2,d))) implies d1 = d2

    proof

      assume that

       A1: F is having_a_unity and

       A2: F is associative and

       A3: F is having_an_inverseOp and

       A4: (F . (d,d1)) = (F . (d,d2)) or (F . (d1,d)) = (F . (d2,d));

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

      per cases by A4;

        suppose

         A5: (F . (d,d1)) = (F . (d,d2));

        

        thus d1 = (F . (e,d1)) by A1, SETWISEO: 15

        .= (F . ((F . ((u . d),d)),d1)) by A1, A2, A3, Th59

        .= (F . ((u . d),(F . (d,d2)))) by A2, A5

        .= (F . ((F . ((u . d),d)),d2)) by A2

        .= (F . (e,d2)) by A1, A2, A3, Th59

        .= d2 by A1, SETWISEO: 15;

      end;

        suppose

         A6: (F . (d1,d)) = (F . (d2,d));

        

        thus d1 = (F . (d1,e)) by A1, SETWISEO: 15

        .= (F . (d1,(F . (d,(u . d))))) by A1, A2, A3, Th59

        .= (F . ((F . (d2,d)),(u . d))) by A2, A6

        .= (F . (d2,(F . (d,(u . d))))) by A2

        .= (F . (d2,e)) by A1, A2, A3, Th59

        .= d2 by A1, SETWISEO: 15;

      end;

    end;

    theorem :: FINSEQOP:65

    

     Th65: F is having_a_unity & F is associative & F is having_an_inverseOp & ((F . (d1,d2)) = d2 or (F . (d2,d1)) = d2) implies d1 = ( the_unity_wrt F)

    proof

      assume that

       A1: F is having_a_unity and

       A2: F is associative & F is having_an_inverseOp;

      set e = ( the_unity_wrt F);

      assume (F . (d1,d2)) = d2 or (F . (d2,d1)) = d2;

      then (F . (d1,d2)) = (F . (e,d2)) or (F . (d2,d1)) = (F . (d2,e)) by A1, SETWISEO: 15;

      hence thesis by A1, A2, Th64;

    end;

    theorem :: FINSEQOP:66

    

     Th66: F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F & e = ( the_unity_wrt F) implies for d holds (G . (e,d)) = e & (G . (d,e)) = e

    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 and

       A5: e = ( the_unity_wrt F);

      let d;

      set ed = (G . (e,d));

      (F . (ed,ed)) = (G . ((F . (e,e)),d)) by A4, BINOP_1: 11

      .= ed by A2, A5, SETWISEO: 15;

      hence ed = e by A1, A2, A3, A5, Th65;

      set de = (G . (d,e));

      (F . (de,de)) = (G . (d,(F . (e,e)))) by A4, BINOP_1: 11

      .= de by A2, A5, SETWISEO: 15;

      hence thesis by A1, A2, A3, A5, Th65;

    end;

    theorem :: FINSEQOP:67

    

     Th67: F is having_a_unity & F is associative & F is having_an_inverseOp & u = ( the_inverseOp_wrt F) & G is_distributive_wrt F implies (u . (G . (d1,d2))) = (G . ((u . d1),d2)) & (u . (G . (d1,d2))) = (G . (d1,(u . d2)))

    proof

      assume that

       A1: F is having_a_unity & F is associative & F is having_an_inverseOp and

       A2: u = ( the_inverseOp_wrt F) and

       A3: G is_distributive_wrt F;

      set e = ( the_unity_wrt F);

      (F . ((G . (d1,d2)),(G . ((u . d1),d2)))) = (G . ((F . (d1,(u . d1))),d2)) by A3, BINOP_1: 11

      .= (G . (e,d2)) by A1, A2, Th59

      .= e by A1, A3, Th66;

      hence (u . (G . (d1,d2))) = (G . ((u . d1),d2)) by A1, A2, Th60;

      (F . ((G . (d1,d2)),(G . (d1,(u . d2))))) = (G . (d1,(F . (d2,(u . d2))))) by A3, BINOP_1: 11

      .= (G . (d1,e)) by A1, A2, Th59

      .= e by A1, A3, Th66;

      hence thesis by A1, A2, Th60;

    end;

    theorem :: FINSEQOP:68

    F is having_a_unity & F is associative & F is having_an_inverseOp & u = ( the_inverseOp_wrt F) & G is_distributive_wrt F & G is having_a_unity implies (G [;] ((u . ( the_unity_wrt G)),( id D))) = u

    proof

      assume that

       A1: F is having_a_unity & F is associative & F is having_an_inverseOp & u = ( the_inverseOp_wrt F) & G is_distributive_wrt F and

       A2: G is having_a_unity;

      set o = ( the_unity_wrt G);

      for d holds ((G [;] ((u . o),( id D))) . d) = (u . d)

      proof

        let d;

        

        thus ((G [;] ((u . o),( id D))) . d) = (G . ((u . o),(( id D) . d))) by FUNCOP_1: 53

        .= (G . ((u . o),d))

        .= (u . (G . (o,d))) by A1, Th67

        .= (u . d) by A2, SETWISEO: 15;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: FINSEQOP:69

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

    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), i = ( the_inverseOp_wrt F);

      (G . (d,e)) = (G . (d,(F . (e,e)))) by A2, SETWISEO: 15

      .= (F . ((G . (d,e)),(G . (d,e)))) by A4, BINOP_1: 11;

      then e = (F . ((F . ((G . (d,e)),(G . (d,e)))),(i . (G . (d,e))))) by A1, A2, A3, Th59;

      then e = (F . ((G . (d,e)),(F . ((G . (d,e)),(i . (G . (d,e))))))) by A1;

      then e = (F . ((G . (d,e)),e)) by A1, A2, A3, Th59;

      then e = (G . (d,e)) by A2, SETWISEO: 15;

      then (G . (d,(( id D) . e))) = e;

      hence thesis by FUNCOP_1: 53;

    end;

    theorem :: FINSEQOP:70

    F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F implies ((G [:] (( id D),d)) . ( the_unity_wrt F)) = ( the_unity_wrt F)

    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), i = ( the_inverseOp_wrt F);

      (G . (e,d)) = (G . ((F . (e,e)),d)) by A2, SETWISEO: 15

      .= (F . ((G . (e,d)),(G . (e,d)))) by A4, BINOP_1: 11;

      then e = (F . ((F . ((G . (e,d)),(G . (e,d)))),(i . (G . (e,d))))) by A1, A2, A3, Th59;

      then e = (F . ((G . (e,d)),(F . ((G . (e,d)),(i . (G . (e,d))))))) by A1;

      then e = (F . ((G . (e,d)),e)) by A1, A2, A3, Th59;

      then e = (G . (e,d)) by A2, SETWISEO: 15;

      then (G . ((( id D) . e),d)) = e;

      hence thesis by FUNCOP_1: 48;

    end;

    theorem :: FINSEQOP:71

    

     Th71: F is having_a_unity & F is associative & F is having_an_inverseOp implies (F .: (f,(( the_inverseOp_wrt F) * f))) = (C --> ( the_unity_wrt F)) & (F .: ((( the_inverseOp_wrt F) * f),f)) = (C --> ( the_unity_wrt F))

    proof

      set u = ( the_inverseOp_wrt F);

      reconsider g = (C --> ( the_unity_wrt F)) as Function of C, D;

      assume

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

      now

        let c;

        

        thus ((F .: (f,(u * f))) . c) = (F . ((f . c),((u * f) . c))) by FUNCOP_1: 37

        .= (F . ((f . c),(u . (f . c)))) by FUNCT_2: 15

        .= ( the_unity_wrt F) by A1, Th59

        .= (g . c);

      end;

      hence (F .: (f,(( the_inverseOp_wrt F) * f))) = (C --> ( the_unity_wrt F)) by FUNCT_2: 63;

      now

        let c;

        

        thus ((F .: ((u * f),f)) . c) = (F . (((u * f) . c),(f . c))) by FUNCOP_1: 37

        .= (F . ((u . (f . c)),(f . c))) by FUNCT_2: 15

        .= ( the_unity_wrt F) by A1, Th59

        .= (g . c);

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: FINSEQOP:72

    

     Th72: F is associative & F is having_an_inverseOp & F is having_a_unity & (F .: (f,f9)) = (C --> ( the_unity_wrt F)) implies f = (( the_inverseOp_wrt F) * f9) & (( the_inverseOp_wrt F) * f) = f9

    proof

      assume that

       A1: F is associative & F is having_an_inverseOp & F is having_a_unity and

       A2: (F .: (f,f9)) = (C --> ( the_unity_wrt F));

      set u = ( the_inverseOp_wrt F);

      set e = ( the_unity_wrt F);

      reconsider g = (C --> e) as Function of C, D;

      now

        let c;

        (F . ((f . c),(f9 . c))) = (g . c) by A2, FUNCOP_1: 37

        .= e;

        

        hence (f . c) = (u . (f9 . c)) by A1, Th60

        .= ((u * f9) . c) by FUNCT_2: 15;

      end;

      hence f = (( the_inverseOp_wrt F) * f9) by FUNCT_2: 63;

      now

        let c;

        (F . ((f . c),(f9 . c))) = (g . c) by A2, FUNCOP_1: 37

        .= e;

        then (f9 . c) = (u . (f . c)) by A1, Th60;

        hence ((u * f) . c) = (f9 . c) by FUNCT_2: 15;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: FINSEQOP:73

    F is having_a_unity & F is associative & F is having_an_inverseOp implies (F .: (T,(( the_inverseOp_wrt F) * T))) = (i |-> ( the_unity_wrt F)) & (F .: ((( the_inverseOp_wrt F) * T),T)) = (i |-> ( the_unity_wrt F))

    proof

      assume

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

      reconsider uT = (( the_inverseOp_wrt F) * T) as Element of (i -tuples_on D) by FINSEQ_2: 113;

      per cases ;

        suppose

         A2: i = 0 ;

        then (F .: (T,uT)) = ( <*> D) & (F .: (uT,T)) = ( <*> D) by Lm1;

        hence thesis by A2;

      end;

        suppose i <> 0 ;

        then

        reconsider C = ( Seg i) as non empty set;

        T is Function of C, D by Lm4;

        hence thesis by A1, Th71;

      end;

    end;

    theorem :: FINSEQOP:74

    F is associative & F is having_an_inverseOp & F is having_a_unity & (F .: (T1,T2)) = (i |-> ( the_unity_wrt F)) implies T1 = (( the_inverseOp_wrt F) * T2) & (( the_inverseOp_wrt F) * T1) = T2

    proof

      assume

       A1: F is associative & F is having_an_inverseOp & F is having_a_unity & (F .: (T1,T2)) = (i |-> ( the_unity_wrt F));

      per cases ;

        suppose i = 0 ;

        then T1 = ( <*> D) & T2 = ( <*> D);

        hence thesis;

      end;

        suppose i <> 0 ;

        then

        reconsider C = ( Seg i) as non empty set;

        T1 is Function of C, D & T2 is Function of C, D by Lm4;

        hence thesis by A1, Th72;

      end;

    end;

    theorem :: FINSEQOP:75

    

     Th75: F is associative & F is having_a_unity & e = ( the_unity_wrt F) & F is having_an_inverseOp & G is_distributive_wrt F implies (G [;] (e,f)) = (C --> e)

    proof

      reconsider g = (C --> e) as Function of C, D;

      assume

       A1: F is associative & F is having_a_unity & e = ( the_unity_wrt F) & F is having_an_inverseOp & G is_distributive_wrt F;

      now

        let c;

        

        thus ((G [;] (e,f)) . c) = (G . (e,(f . c))) by FUNCOP_1: 53

        .= e by A1, Th66

        .= (g . c);

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: FINSEQOP:76

    F is associative & F is having_a_unity & e = ( the_unity_wrt F) & F is having_an_inverseOp & G is_distributive_wrt F implies (G [;] (e,T)) = (i |-> e)

    proof

      assume

       A1: F is associative & F is having_a_unity & e = ( the_unity_wrt F) & F is having_an_inverseOp & G is_distributive_wrt F;

      per cases ;

        suppose

         A2: i = 0 ;

        then (G [;] (e,T)) = ( <*> D) by Lm2;

        hence thesis by A2;

      end;

        suppose i <> 0 ;

        then

        reconsider C = ( Seg i) as non empty set;

        T is Function of C, D by Lm4;

        hence thesis by A1, Th75;

      end;

    end;

    definition

      let F,f,g be Function;

      :: FINSEQOP:def4

      func F * (f,g) -> Function equals (F * [:f, g:]);

      correctness ;

    end

    theorem :: FINSEQOP:77

    

     Th77: for F,f,g be Function st [x, y] in ( dom (F * (f,g))) holds ((F * (f,g)) . (x,y)) = (F . ((f . x),(g . y)))

    proof

      let F,f,g be Function such that

       A1: [x, y] in ( dom (F * (f,g)));

       [x, y] in ( dom [:f, g:]) by A1, FUNCT_1: 11;

      then [x, y] in [:( dom f), ( dom g):] by FUNCT_3:def 8;

      then ( [:f, g:] . (x,y)) = [(f . x), (g . y)] by FUNCT_3: 65;

      hence thesis by A1, FUNCT_1: 12;

    end;

    ::$Canceled

    theorem :: FINSEQOP:79

    

     Th78: for F be Function of [:D, D9:], E, f be Function of C, D, g be Function of C9, D9 holds (F * (f,g)) is Function of [:C, C9:], E

    proof

      let F be Function of [:D, D9:], E, f be Function of C, D, g be Function of C9, D9;

      (F * (f,g)) = (F * [:f, g:]);

      hence thesis;

    end;

    theorem :: FINSEQOP:80

    for u,u9 be Function of D, D holds (F * (u,u9)) is BinOp of D by Th78;

    definition

      let D, F;

      let f,f9 be Function of D, D;

      :: original: *

      redefine

      func F * (f,f9) -> BinOp of D ;

      coherence by Th78;

    end

    theorem :: FINSEQOP:81

    

     Th80: for F be Function of [:D, D9:], E, f be Function of C, D, g be Function of C9, D9 holds ((F * (f,g)) . (c,c9)) = (F . ((f . c),(g . c9)))

    proof

      let F be Function of [:D, D9:], E, f be Function of C, D, g be Function of C9, D9;

      set H = (F * (f,g));

      H is Function of [:C, C9:], E by Th78;

      then ( dom H) = [:C, C9:] by FUNCT_2:def 1;

      then [c, c9] in ( dom H) by ZFMISC_1:def 2;

      hence thesis by Th77;

    end;

    theorem :: FINSEQOP:82

    

     Th81: for u be Function of D, D holds ((F * (( id D),u)) . (d1,d2)) = (F . (d1,(u . d2))) & ((F * (u,( id D))) . (d1,d2)) = (F . ((u . d1),d2))

    proof

      let u be Function of D, D;

      (( id D) . d1) = d1 & (( id D) . d2) = d2;

      hence thesis by Th80;

    end;

    theorem :: FINSEQOP:83

    

     Th82: ((F * (( id D),u)) .: (f,f9)) = (F .: (f,(u * f9)))

    proof

      now

        let c;

        

        thus (((F * (( id D),u)) .: (f,f9)) . c) = ((F * (( id D),u)) . ((f . c),(f9 . c))) by FUNCOP_1: 37

        .= (F . ((f . c),(u . (f9 . c)))) by Th81

        .= (F . ((f . c),((u * f9) . c))) by FUNCT_2: 15

        .= ((F .: (f,(u * f9))) . c) by FUNCOP_1: 37;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: FINSEQOP:84

    ((F * (( id D),u)) .: (T1,T2)) = (F .: (T1,(u * T2)))

    proof

      now

        per cases ;

          suppose i = 0 ;

          then ((F * (( id D),u)) .: (T1,T2)) = ( <*> D) & (u * T2) = ( <*> D) by Lm1;

          hence thesis by FINSEQ_2: 73;

        end;

          suppose i <> 0 ;

          then

          reconsider C = ( Seg i) as non empty set;

          T1 is Function of C, D & T2 is Function of C, D by Lm4;

          hence thesis by Th82;

        end;

      end;

      hence thesis;

    end;

    theorem :: FINSEQOP:85

    F is associative & F is having_a_unity & F is commutative & F is having_an_inverseOp & u = ( the_inverseOp_wrt F) implies (u . ((F * (( id D),u)) . (d1,d2))) = ((F * (u,( id D))) . (d1,d2)) & ((F * (( id D),u)) . (d1,d2)) = (u . ((F * (u,( id D))) . (d1,d2)))

    proof

      assume that

       A1: F is associative & F is having_a_unity and

       A2: F is commutative and

       A3: F is having_an_inverseOp & u = ( the_inverseOp_wrt F);

      

       A4: u is_distributive_wrt F by A1, A2, A3, Th63;

      

      thus (u . ((F * (( id D),u)) . (d1,d2))) = (u . (F . (d1,(u . d2)))) by Th81

      .= (F . ((u . d1),(u . (u . d2)))) by A4

      .= (F . ((u . d1),d2)) by A1, A3, Th62

      .= ((F * (u,( id D))) . (d1,d2)) by Th81;

      hence thesis by A1, A3, Th62;

    end;

    theorem :: FINSEQOP:86

    F is associative & F is having_a_unity & F is having_an_inverseOp implies ((F * (( id D),( the_inverseOp_wrt F))) . (d,d)) = ( the_unity_wrt F)

    proof

      assume

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

      set u = ( the_inverseOp_wrt F);

      

      thus ((F * (( id D),u)) . (d,d)) = (F . (d,(u . d))) by Th81

      .= ( the_unity_wrt F) by A1, Th59;

    end;

    theorem :: FINSEQOP:87

    F is associative & F is having_a_unity & F is having_an_inverseOp implies ((F * (( id D),( the_inverseOp_wrt F))) . (d,( the_unity_wrt F))) = d

    proof

      assume that

       A1: F is associative and

       A2: F is having_a_unity and

       A3: F is having_an_inverseOp;

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

      

      thus ((F * (( id D),u)) . (d,e)) = (F . (d,(u . e))) by Th81

      .= (F . (d,e)) by A1, A2, A3, Th61

      .= d by A2, SETWISEO: 15;

    end;

    theorem :: FINSEQOP:88

    F is having_a_unity implies ((F * (( id D),u)) . (( the_unity_wrt F),d)) = (u . d)

    proof

      assume

       A1: F is having_a_unity;

      set e = ( the_unity_wrt F);

      

      thus ((F * (( id D),u)) . (e,d)) = (F . (e,(u . d))) by Th81

      .= (u . d) by A1, SETWISEO: 15;

    end;

    theorem :: FINSEQOP:89

    F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G = (F * (( id D),( the_inverseOp_wrt F))) implies for d1, d2, d3, d4 holds (F . ((G . (d1,d2)),(G . (d3,d4)))) = (G . ((F . (d1,d3)),(F . (d2,d4))))

    proof

      assume that

       A1: F is commutative and

       A2: F is associative and

       A3: F is having_a_unity & F is having_an_inverseOp and

       A4: G = (F * (( id D),( the_inverseOp_wrt F)));

      set u = ( the_inverseOp_wrt F);

      

       A5: u is_distributive_wrt F by A1, A2, A3, Th63;

      let d1, d2, d3, d4;

      

      thus (F . ((G . (d1,d2)),(G . (d3,d4)))) = (F . ((F . (d1,(u . d2))),(G . (d3,d4)))) by A4, Th81

      .= (F . ((F . (d1,(u . d2))),(F . (d3,(u . d4))))) by A4, Th81

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

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

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

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

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

      .= (F . ((F . (d1,d3)),(u . (F . (d2,d4))))) by A5

      .= (G . ((F . (d1,d3)),(F . (d2,d4)))) by A4, Th81;

    end;