finseq_7.miz



    begin

    reserve D for non empty set,

f for FinSequence of D,

p,p1,p2,p3,q for Element of D,

i,j,k,l,n for Nat;

    theorem :: FINSEQ_7:1

    1 <= i & j <= ( len f) & i < j implies f = (((((f | (i -' 1)) ^ <*(f . i)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f . j)*>) ^ (f /^ j))

    proof

      assume that

       A1: 1 <= i and

       A2: j <= ( len f) and

       A3: i < j;

      

       A4: i <= ( len f) by A2, A3, XXREAL_0: 2;

      1 <= j by A1, A3, XXREAL_0: 2;

      then

       A5: j in ( dom f) by A2, FINSEQ_3: 25;

      set I = ((j -' i) -' 1);

      (i -' i) < (j -' i) by A3, NAT_D: 57;

      then

       A6: (I + 1) = (j -' i) by NAT_1: 14, XREAL_1: 235;

      (j -' i) <= (( len f) -' i) by A2, NAT_D: 42;

      then

       A7: (I + 1) <= ( len (f /^ i)) by A6, RFINSEQ: 29;

      reconsider i, j as Element of NAT by ORDINAL1:def 12;

      

       A8: i < ( len (f | j)) by A2, A3, FINSEQ_1: 59;

      1 <= (I + 1) by NAT_1: 14;

      then

       A9: (I + 1) in ( dom (f /^ i)) by A7, FINSEQ_3: 25;

      ((I + 1) + i) = j by A3, A6, XREAL_1: 235;

      then

       A10: ((f /^ i) /. (I + 1)) = (f /. j) by A9, FINSEQ_5: 27;

      

       A11: (f /^ i) = (((f | j) ^ (f /^ j)) /^ i) by RFINSEQ: 8

      .= (((f | j) /^ i) ^ (f /^ j)) by A8, GENEALG1: 1

      .= (((f /^ i) | (I + 1)) ^ (f /^ j)) by A6, FINSEQ_5: 80

      .= ((((f /^ i) | I) ^ <*((f /^ i) /. (I + 1))*>) ^ (f /^ j)) by A7, FINSEQ_5: 82

      .= ((((f /^ i) | I) ^ <*(f . j)*>) ^ (f /^ j)) by A5, A10, PARTFUN1:def 6;

      f = (((f | (i -' 1)) ^ <*(f . i)*>) ^ (f /^ i)) by A1, A4, FINSEQ_5: 84

      .= (((f | (i -' 1)) ^ <*(f . i)*>) ^ (((f /^ i) | I) ^ ( <*(f . j)*> ^ (f /^ j)))) by A11, FINSEQ_1: 32

      .= ((((f | (i -' 1)) ^ <*(f . i)*>) ^ ((f /^ i) | I)) ^ ( <*(f . j)*> ^ (f /^ j))) by FINSEQ_1: 32

      .= (((((f | (i -' 1)) ^ <*(f . i)*>) ^ ((f /^ i) | I)) ^ <*(f . j)*>) ^ (f /^ j)) by FINSEQ_1: 32;

      hence thesis;

    end;

    theorem :: FINSEQ_7:2

    for f,g,h be FinSequence holds ( len g) = ( len h) & ( len g) < i & i <= ( len (g ^ f)) implies ((g ^ f) . i) = ((h ^ f) . i)

    proof

      let f,g,h be FinSequence;

      assume that

       A1: ( len g) = ( len h) and

       A2: ( len g) < i and

       A3: i <= ( len (g ^ f));

      i <= (( len g) + ( len f)) by A3, FINSEQ_1: 22;

      then

       A4: (i - ( len g)) <= ((( len g) + ( len f)) - ( len g)) by XREAL_1: 9;

      set k = (i - ( len g));

      

       A5: (( len g) - ( len g)) < (i - ( len g)) by A2, XREAL_1: 9;

      then

      reconsider k as Element of NAT by INT_1: 3;

      ( 0 + 1) <= (i - ( len g)) by A5, INT_1: 7;

      then

       A6: k in ( dom f) by A4, FINSEQ_3: 25;

      ((g ^ f) . i) = ((g ^ f) . (k + ( len g)))

      .= (f . k) by A6, FINSEQ_1:def 7

      .= ((h ^ f) . (( len h) + k)) by A6, FINSEQ_1:def 7;

      hence thesis by A1;

    end;

    theorem :: FINSEQ_7:3

    for f,g be FinSequence st 1 <= i & i <= ( len f) holds (f . i) = ((g ^ f) . (( len g) + i))

    proof

      let f,g be FinSequence;

      assume 1 <= i & i <= ( len f);

      then i in ( dom f) by FINSEQ_3: 25;

      hence thesis by FINSEQ_1:def 7;

    end;

    theorem :: FINSEQ_7:4

    i in ( dom (f /^ n)) implies ((f /^ n) . i) = (f . (n + i)) by FINSEQ_5: 27;

    

     Lm1: ((j -' i) -' 1) = ((j -' 1) -' i)

    proof

      ((j -' i) -' 1) = (j -' (i + 1)) by NAT_2: 30;

      hence thesis by NAT_2: 30;

    end;

    begin

    notation

      let f be FinSequence;

      let i be Nat;

      let p be object;

      synonym Replace (f,i,p) for f +* (i,p);

    end

    definition

      let D be non empty set;

      let f be FinSequence of D;

      let i be Nat;

      let p be Element of D;

      :: original: Replace

      redefine

      :: FINSEQ_7:def1

      func Replace (f,i,p) -> FinSequence of D equals

      : Def1: (((f | (i -' 1)) ^ <*p*>) ^ (f /^ i)) if 1 <= i & i <= ( len f)

      otherwise f;

      compatibility

      proof

        

         A1: not (1 <= i & i <= ( len f)) implies (f +* (i,p)) = f

        proof

          assume not (1 <= i & i <= ( len f));

          then not i in ( dom f) by FINSEQ_3: 25;

          hence thesis by FUNCT_7:def 3;

        end;

        1 <= i & i <= ( len f) implies (f +* (i,p)) = (((f | (i -' 1)) ^ <*p*>) ^ (f /^ i))

        proof

          assume 1 <= i & i <= ( len f);

          then i in ( dom f) by FINSEQ_3: 25;

          hence thesis by FUNCT_7: 98;

        end;

        hence thesis by A1;

      end;

      correctness

      proof

        reconsider i as Element of NAT by ORDINAL1:def 12;

        (f +* (i,p)) is FinSequence of D;

        hence thesis;

      end;

    end

    theorem :: FINSEQ_7:5

    ( len ( Replace (f,i,p))) = ( len f) by FUNCT_7: 97;

    theorem :: FINSEQ_7:6

    for f be FinSequence, i be Nat, p be set holds ( rng ( Replace (f,i,p))) c= (( rng f) \/ {p}) by FUNCT_7: 100;

    theorem :: FINSEQ_7:7

    1 <= i & i <= ( len f) implies p in ( rng ( Replace (f,i,p)))

    proof

      assume 1 <= i & i <= ( len f);

      then i in ( dom f) by FINSEQ_3: 25;

      hence thesis by FUNCT_7: 102;

    end;

    

     Lm2: 1 <= i & i <= ( len f) implies (( Replace (f,i,p)) . i) = p

    proof

      assume 1 <= i & i <= ( len f);

      then i in ( dom f) by FINSEQ_3: 25;

      hence thesis by FUNCT_7: 31;

    end;

    theorem :: FINSEQ_7:8

    1 <= i & i <= ( len f) implies (( Replace (f,i,p)) /. i) = p

    proof

      assume 1 <= i & i <= ( len f);

      then i in ( dom f) by FINSEQ_3: 25;

      hence thesis by FUNCT_7: 36;

    end;

    theorem :: FINSEQ_7:9

    1 <= i & i <= ( len f) implies for k st 0 < k & k <= (( len f) - i) holds (( Replace (f,i,p)) . (i + k)) = ((f /^ i) . k)

    proof

      assume that

       A1: 1 <= i and

       A2: i <= ( len f);

      (i - 1) < i by XREAL_1: 146;

      then

       A3: (i -' 1) < i by A1, XREAL_1: 233;

      

       A4: ( len ((f | (i -' 1)) ^ <*p*>)) = (( len (f | (i -' 1))) + ( len <*p*>)) by FINSEQ_1: 22

      .= ((i -' 1) + ( len <*p*>)) by A2, A3, FINSEQ_1: 59, XXREAL_0: 2

      .= ((i -' 1) + 1) by FINSEQ_1: 39

      .= i by A1, XREAL_1: 235;

      let k;

      assume that

       A5: 0 < k and

       A6: k <= (( len f) - i);

      

       A7: ( 0 + 1) <= k by A5, INT_1: 7;

      ( len f) = ( len ( Replace (f,i,p))) by FUNCT_7: 97

      .= ( len (((f | (i -' 1)) ^ <*p*>) ^ (f /^ i))) by A1, A2, Def1

      .= (i + ( len (f /^ i))) by A4, FINSEQ_1: 22;

      then

       A8: k in ( dom (f /^ i)) by A6, A7, FINSEQ_3: 25;

      (( Replace (f,i,p)) . (i + k)) = ((((f | (i -' 1)) ^ <*p*>) ^ (f /^ i)) . (( len ((f | (i -' 1)) ^ <*p*>)) + k)) by A1, A2, A4, Def1;

      hence thesis by A8, FINSEQ_1:def 7;

    end;

    theorem :: FINSEQ_7:10

    

     Th10: 1 <= k & k <= ( len f) & k <> i implies (( Replace (f,i,p)) /. k) = (f /. k)

    proof

      assume

       A1: 1 <= k & k <= ( len f) & k <> i;

      reconsider i, k as Element of NAT by ORDINAL1:def 12;

      k <> i & k in ( dom f) by A1, FINSEQ_3: 25;

      hence thesis by FUNCT_7: 37;

    end;

    theorem :: FINSEQ_7:11

    

     Th11: 1 <= i & i < j & j <= ( len f) implies ( Replace (( Replace (f,j,q)),i,p)) = (((((f | (i -' 1)) ^ <*p*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*q*>) ^ (f /^ j))

    proof

      assume that

       A1: 1 <= i and

       A2: i < j and

       A3: j <= ( len f);

      set fp = (f | (j -' 1));

      

       A4: (j -' 1) <= j by NAT_D: 35;

      (1 + i) <= j by A2, INT_1: 7;

      then i <= (j -' 1) by NAT_D: 55;

      then

       A5: i <= ( len fp) by A3, A4, FINSEQ_1: 59, XXREAL_0: 2;

      set Q = (f /^ j);

      set F = ( Replace (f,j,q));

      

       A6: 1 <= j by A1, A2, XXREAL_0: 2;

      set fj = <*q*>;

      set P = (fp ^ fj);

      

       A7: ( len P) = (( len fp) + ( len fj)) by FINSEQ_1: 22

      .= (( len fp) + 1) by FINSEQ_1: 39

      .= ((j -' 1) + 1) by A3, A4, FINSEQ_1: 59, XXREAL_0: 2

      .= j by A1, A2, XREAL_1: 235, XXREAL_0: 2;

      

       A8: (i -' 1) < (j -' 1) by A1, A2, NAT_D: 56;

      then

       A9: (i -' 1) <= ( len fp) by A3, A4, FINSEQ_1: 59, XXREAL_0: 2;

      i <= ( len f) by A2, A3, XXREAL_0: 2;

      then i <= ( len F) by FUNCT_7: 97;

      

      then ( Replace (F,i,p)) = (((F | (i -' 1)) ^ <*p*>) ^ (F /^ i)) by A1, Def1

      .= (((F | (i -' 1)) ^ <*p*>) ^ ((P ^ Q) /^ i)) by A3, A6, Def1

      .= (((F | (i -' 1)) ^ <*p*>) ^ ((P /^ i) ^ Q)) by A2, A7, GENEALG1: 1

      .= (((F | (i -' 1)) ^ <*p*>) ^ (((fp /^ i) ^ fj) ^ Q)) by A5, GENEALG1: 1

      .= (((F | (i -' 1)) ^ <*p*>) ^ ((((f /^ i) | ((j -' 1) -' i)) ^ fj) ^ Q)) by FINSEQ_5: 80

      .= ((((F | (i -' 1)) ^ <*p*>) ^ (((f /^ i) | ((j -' 1) -' i)) ^ fj)) ^ Q) by FINSEQ_1: 32

      .= (((((F | (i -' 1)) ^ <*p*>) ^ ((f /^ i) | ((j -' 1) -' i))) ^ fj) ^ Q) by FINSEQ_1: 32

      .= ((((((P ^ Q) | (i -' 1)) ^ <*p*>) ^ ((f /^ i) | ((j -' 1) -' i))) ^ fj) ^ Q) by A3, A6, Def1

      .= (((((P | (i -' 1)) ^ <*p*>) ^ ((f /^ i) | ((j -' 1) -' i))) ^ fj) ^ Q) by A2, A7, FINSEQ_5: 22, NAT_D: 44

      .= (((((fp | (i -' 1)) ^ <*p*>) ^ ((f /^ i) | ((j -' 1) -' i))) ^ fj) ^ Q) by A9, FINSEQ_5: 22

      .= (((((f | (i -' 1)) ^ <*p*>) ^ ((f /^ i) | ((j -' 1) -' i))) ^ fj) ^ Q) by A8, FINSEQ_5: 77

      .= (((((f | (i -' 1)) ^ <*p*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*q*>) ^ Q) by Lm1;

      hence thesis;

    end;

    theorem :: FINSEQ_7:12

    ( Replace ( <*p*>,1,q)) = <*q*>

    proof

      

       A1: (1 - 1) = 0 ;

      set g = ( <*> D);

      reconsider P = ( <*p*> ^ g) as FinSequence of D;

      

       A2: (( <*p*> ^ g) /^ 1) = g by FINSEQ_6: 45;

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

      

      hence ( Replace ( <*p*>,1,q)) = ((( <*p*> | (1 -' 1)) ^ <*q*>) ^ ( <*p*> /^ 1)) by Def1

      .= ((( <*p*> | 0 ) ^ <*q*>) ^ ( <*p*> /^ 1)) by A1, XREAL_0:def 2

      .= ( <*q*> ^ ( <*p*> /^ 1)) by FINSEQ_1: 34

      .= ( <*q*> ^ (P /^ 1)) by FINSEQ_1: 34

      .= <*q*> by A2, FINSEQ_1: 34;

    end;

    theorem :: FINSEQ_7:13

    

     Th13: ( Replace ( <*p1, p2*>,1,q)) = <*q, p2*>

    proof

      set f = <*p1, p2*>;

      

       A1: ( len f) = 2 by FINSEQ_1: 44;

      (1 + 1) = ( len f) by FINSEQ_1: 44;

      then

       A3: (f /^ 1) = <*(f . 2)*> by FINSEQ_5: 30;

      ( Replace (f,1,q)) = (((f | (1 -' 1)) ^ <*q*>) ^ (f /^ 1)) by A1, Def1

      .= (((f | 0 ) ^ <*q*>) ^ (f /^ 1)) by XREAL_1: 232

      .= (( {} ^ <*q*>) ^ <*p2*>) by A3, FINSEQ_1: 44

      .= ( <*q*> ^ <*p2*>) by FINSEQ_1: 34;

      hence thesis;

    end;

    theorem :: FINSEQ_7:14

    

     Th14: ( Replace ( <*p1, p2*>,2,q)) = <*p1, q*>

    proof

      set f = <*p1, p2*>;

      

       A1: (2 -' 1) = ((1 + 1) -' 1)

      .= 1 by NAT_D: 34;

      2 <= ( len f) by FINSEQ_1: 44;

      

      then ( Replace (f,2,q)) = (((f | (2 -' 1)) ^ <*q*>) ^ (f /^ 2)) by Def1

      .= (((f | 1) ^ <*q*>) ^ (f /^ ( len f))) by A1, FINSEQ_1: 44

      .= (((f | 1) ^ <*q*>) ^ {} ) by RFINSEQ: 27

      .= (( <*(f . 1)*> ^ <*q*>) ^ {} ) by FINSEQ_5: 20

      .= ( <*(f . 1)*> ^ <*q*>) by FINSEQ_1: 34

      .= ( <*p1*> ^ <*q*>) by FINSEQ_1: 44;

      hence thesis;

    end;

    theorem :: FINSEQ_7:15

    

     Th15: ( Replace ( <*p1, p2, p3*>,1,q)) = <*q, p2, p3*>

    proof

      set f = <*p1, p2, p3*>;

      ( len f) = 3 by FINSEQ_1: 45;

      

      then ( Replace (f,1,q)) = (((f | (1 -' 1)) ^ <*q*>) ^ (f /^ 1)) by Def1

      .= (((f | 0 ) ^ <*q*>) ^ (f /^ 1)) by XREAL_1: 232

      .= ( <*q*> ^ (f /^ 1)) by FINSEQ_1: 34

      .= ( <*q*> ^ <*p2, p3*>) by FINSEQ_6: 47

      .= (( <*q*> ^ <*p2*>) ^ <*p3*>) by FINSEQ_1: 32;

      hence thesis;

    end;

    theorem :: FINSEQ_7:16

    

     Th16: ( Replace ( <*p1, p2, p3*>,2,q)) = <*p1, q, p3*>

    proof

      set f = <*p1, p2, p3*>;

      

       A1: (2 -' 1) = ((1 + 1) -' 1)

      .= 1 by NAT_D: 34;

      

       A2: ( len f) = (2 + 1) by FINSEQ_1: 45;

      ( len f) = 3 by FINSEQ_1: 45;

      

      then ( Replace (f,2,q)) = (((f | (2 -' 1)) ^ <*q*>) ^ (f /^ 2)) by Def1

      .= (((f | 1) ^ <*q*>) ^ <*(f . 3)*>) by A1, A2, FINSEQ_5: 30

      .= (((f | 1) ^ <*q*>) ^ <*p3*>) by FINSEQ_1: 45

      .= (( <*(f . 1)*> ^ <*q*>) ^ <*p3*>) by FINSEQ_5: 20

      .= (( <*p1*> ^ <*q*>) ^ <*p3*>) by FINSEQ_1: 45;

      hence thesis;

    end;

    theorem :: FINSEQ_7:17

    

     Th17: ( Replace ( <*p1, p2, p3*>,3,q)) = <*p1, p2, q*>

    proof

      set f = <*p1, p2, p3*>;

      

       A1: (3 -' 1) = ((2 + 1) -' 1)

      .= 2 by NAT_D: 34;

      

       A2: ( len f) = 3 by FINSEQ_1: 45;

      then

       A3: 1 in ( dom f) by FINSEQ_3: 25;

      

       A4: 2 in ( dom f) by A2, FINSEQ_3: 25;

      3 <= ( len f) by FINSEQ_1: 45;

      

      then ( Replace (f,3,q)) = (((f | (3 -' 1)) ^ <*q*>) ^ (f /^ 3)) by Def1

      .= (((f | 2) ^ <*q*>) ^ (f /^ ( len f))) by A1, FINSEQ_1: 45

      .= (((f | 2) ^ <*q*>) ^ {} ) by RFINSEQ: 27

      .= ((f | 2) ^ <*q*>) by FINSEQ_1: 34

      .= ( <*(f /. 1), (f /. 2)*> ^ <*q*>) by A2, FINSEQ_5: 81

      .= (( <*(f . 1)*> ^ <*(f /. 2)*>) ^ <*q*>) by A3, PARTFUN1:def 6

      .= (( <*(f . 1)*> ^ <*(f . 2)*>) ^ <*q*>) by A4, PARTFUN1:def 6

      .= (( <*p1*> ^ <*(f . 2)*>) ^ <*q*>) by FINSEQ_1: 45

      .= (( <*p1*> ^ <*p2*>) ^ <*q*>) by FINSEQ_1: 45;

      hence thesis;

    end;

    begin

    registration

      let f be FinSequence;

      let i,j be Nat;

      cluster ( Swap (f,i,j)) -> FinSequence-like;

      correctness

      proof

        ( dom ( Swap (f,i,j))) = ( dom f) by FUNCT_7: 99;

        hence ex n be Nat st ( dom ( Swap (f,i,j))) = ( Seg n) by FINSEQ_1:def 2;

      end;

    end

    definition

      let D be non empty set;

      let f be FinSequence of D;

      let i,j be Nat;

      :: original: Swap

      redefine

      :: FINSEQ_7:def2

      func Swap (f,i,j) -> FinSequence of D equals

      : Def2: ( Replace (( Replace (f,i,(f /. j))),j,(f /. i))) if 1 <= i & i <= ( len f) & 1 <= j & j <= ( len f)

      otherwise f;

      coherence

      proof

        ( rng ( Swap (f,i,j))) = ( rng f) by FUNCT_7: 103;

        hence ( rng ( Swap (f,i,j))) c= D by FINSEQ_1:def 4;

      end;

      compatibility

      proof

        let IT be FinSequence of D;

        thus 1 <= i & i <= ( len f) & 1 <= j & j <= ( len f) implies (IT = ( Swap (f,i,j)) iff IT = ( Replace (( Replace (f,i,(f /. j))),j,(f /. i))))

        proof

          assume that

           A1: 1 <= i & i <= ( len f) and

           A2: 1 <= j & j <= ( len f);

          

           A3: j in ( dom f) by A2, FINSEQ_3: 25;

          then

           A4: (f /. j) = (f . j) by PARTFUN1:def 6;

          

           A5: i in ( dom f) by A1, FINSEQ_3: 25;

          then (f /. i) = (f . i) by PARTFUN1:def 6;

          hence thesis by A5, A3, A4, FUNCT_7:def 12;

        end;

        assume not (1 <= i & i <= ( len f) & 1 <= j & j <= ( len f));

        then not (i in ( dom f) & j in ( dom f)) by FINSEQ_3: 25;

        hence thesis by FUNCT_7:def 12;

      end;

      correctness ;

    end

    theorem :: FINSEQ_7:18

    

     Th18: ( len ( Swap (f,i,j))) = ( len f)

    proof

      ( dom ( Swap (f,i,j))) = ( dom f) by FUNCT_7: 99;

      hence thesis by FINSEQ_3: 29;

    end;

    

     Lm3: 1 <= i & i <= ( len f) & 1 <= j & j <= ( len f) implies (( Swap (f,i,j)) . i) = (f . j) & (( Swap (f,i,j)) . j) = (f . i)

    proof

      assume that

       A1: 1 <= i and

       A2: i <= ( len f) and

       A3: 1 <= j and

       A4: j <= ( len f);

      

       A5: i in ( dom f) by A1, A2, FINSEQ_3: 25;

      set F = ( Replace (f,i,(f /. j)));

      

       A6: i <= ( len F) by A2, FUNCT_7: 97;

      

       A7: j <= ( len F) by A4, FUNCT_7: 97;

      

       A8: j in ( dom f) by A3, A4, FINSEQ_3: 25;

      per cases ;

        suppose

         A9: i = j;

        (( Swap (f,i,j)) . i) = (( Replace (F,j,(f /. i))) . i) by A1, A2, A3, A4, Def2

        .= (f /. i) by A1, A6, A9, Lm2

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

        hence thesis by A9;

      end;

        suppose

         A10: i <> j;

        

         A11: (( Swap (f,i,j)) . j) = (( Replace (F,j,(f /. i))) . j) by A1, A2, A3, A4, Def2

        .= (f /. i) by A3, A7, Lm2;

        (( Swap (f,i,j)) . i) = (( Replace (F,j,(f /. i))) . i) by A1, A2, A3, A4, Def2

        .= (F . i) by A10, FUNCT_7: 32

        .= (f /. j) by A1, A2, Lm2;

        hence thesis by A5, A8, A11, PARTFUN1:def 6;

      end;

    end;

    theorem :: FINSEQ_7:19

    

     Th19: ( Swap (f,i,i)) = f

    proof

      reconsider i as Element of NAT by ORDINAL1:def 12;

      per cases ;

        suppose 1 <= i & i <= ( len f);

        

        then ( Swap (f,i,i)) = ( Replace (( Replace (f,i,(f /. i))),i,(f /. i))) by Def2

        .= ( Replace (f,i,(f /. i))) by FUNCT_7: 38;

        hence thesis by FUNCT_7: 38;

      end;

        suppose not (1 <= i & i <= ( len f));

        hence thesis by Def2;

      end;

    end;

    theorem :: FINSEQ_7:20

    ( Swap (( Swap (f,i,j)),j,i)) = f

    proof

      per cases ;

        suppose

         A1: 1 <= i & i <= ( len f) & 1 <= j & j <= ( len f);

        

         A2: for k be Nat st 1 <= k & k <= ( len f) holds (f . k) = (( Swap (( Swap (f,i,j)),j,i)) . k)

        proof

          

           A3: i <= ( len ( Swap (f,i,j))) by A1, Th18;

          

           A4: j <= ( len ( Swap (f,i,j))) by A1, Th18;

          let k be Nat;

          assume that

           A5: 1 <= k and

           A6: k <= ( len f);

          

           A7: k <= ( len ( Swap (f,i,j))) by A6, Th18;

          now

            per cases ;

              suppose i = k;

              then (( Swap (( Swap (f,i,j)),j,i)) . k) = (( Swap (f,k,j)) . j) by A1, A7, A4, Lm3;

              hence thesis by A1, A5, A6, Lm3;

            end;

              suppose

               A8: i <> k;

              now

                per cases ;

                  suppose j = k;

                  then (( Swap (( Swap (f,i,j)),j,i)) . k) = (( Swap (f,i,k)) . i) by A1, A7, A3, Lm3;

                  hence thesis by A1, A5, A6, Lm3;

                end;

                  suppose

                   A9: j <> k;

                  set S = ( Swap (f,i,j));

                  (( Swap (S,j,i)) . k) = (( Replace (( Replace (S,j,(S /. i))),i,(S /. j))) . k) by A1, A4, A3, Def2

                  .= (( Replace (S,j,(S /. i))) . k) by A8, FUNCT_7: 32

                  .= (S . k) by A9, FUNCT_7: 32

                  .= (( Replace (( Replace (f,i,(f /. j))),j,(f /. i))) . k) by A1, Def2

                  .= (( Replace (f,i,(f /. j))) . k) by A9, FUNCT_7: 32;

                  hence thesis by A8, FUNCT_7: 32;

                end;

              end;

              hence thesis;

            end;

          end;

          hence thesis;

        end;

        ( len ( Swap (( Swap (f,i,j)),j,i))) = ( len ( Swap (f,i,j))) by Th18

        .= ( len f) by Th18;

        hence thesis by A2;

      end;

        suppose

         A10: not (1 <= i & i <= ( len f) & 1 <= j & j <= ( len f));

        then ( Swap (( Swap (f,i,j)),j,i)) = ( Swap (f,j,i)) by Def2;

        hence thesis by A10, Def2;

      end;

    end;

    theorem :: FINSEQ_7:21

    

     Th21: ( Swap (f,i,j)) = ( Swap (f,j,i))

    proof

      per cases ;

        suppose

         A1: 1 <= i & i <= ( len f) & 1 <= j & j <= ( len f);

        set FJ = ( Replace (f,j,(f /. i)));

        set FI = ( Replace (f,i,(f /. j)));

        

         A2: for k be Nat st 1 <= k & k <= ( len ( Swap (f,i,j))) holds (( Swap (f,i,j)) . k) = (( Swap (f,j,i)) . k)

        proof

          

           A3: ( len ( Swap (f,i,j))) = ( len f) by Th18

          .= ( len FJ) by FUNCT_7: 97;

          

           A4: ( len ( Swap (f,i,j))) = ( len f) by Th18

          .= ( len FI) by FUNCT_7: 97;

          let k be Nat;

          assume that

           A5: 1 <= k and

           A6: k <= ( len ( Swap (f,i,j)));

          

           A7: k <= ( len f) by A6, Th18;

          now

            per cases ;

              suppose

               A8: i = k;

              now

                per cases ;

                  suppose

                   A9: j = k;

                  

                  then (( Swap (f,i,k)) . k) = (( Replace (FI,k,(f /. i))) . k) by A1, Def2

                  .= (f /. i) by A5, A6, A4, Lm2

                  .= (( Replace (FJ,k,(f /. i))) . k) by A5, A6, A3, Lm2

                  .= (( Swap (f,k,i)) . k) by A1, A8, A9, Def2;

                  hence thesis by A9;

                end;

                  suppose

                   A10: j <> k;

                  (( Swap (f,i,j)) . k) = (( Replace (FI,j,(f /. i))) . k) by A1, Def2

                  .= (( Replace (f,k,(f /. j))) . k) by A8, A10, FUNCT_7: 32

                  .= (f /. j) by A5, A7, Lm2

                  .= (( Replace (FJ,k,(f /. j))) . k) by A5, A6, A3, Lm2;

                  hence thesis by A1, A8, Def2;

                end;

              end;

              hence thesis;

            end;

              suppose

               A11: i <> k;

              now

                per cases ;

                  suppose

                   A12: j = k;

                  

                  then (( Swap (f,i,j)) . k) = (( Replace (FI,k,(f /. i))) . k) by A1, Def2

                  .= (f /. i) by A5, A6, A4, Lm2

                  .= (FJ . k) by A5, A7, A12, Lm2

                  .= (( Replace (FJ,i,(f /. j))) . k) by A11, FUNCT_7: 32;

                  hence thesis by A1, Def2;

                end;

                  suppose

                   A13: j <> k;

                  (( Swap (f,i,j)) . k) = (( Replace (FI,j,(f /. i))) . k) by A1, Def2

                  .= (FI . k) by A13, FUNCT_7: 32

                  .= (f . k) by A11, FUNCT_7: 32

                  .= (( Replace (f,j,(f /. i))) . k) by A13, FUNCT_7: 32

                  .= (( Replace (FJ,i,(f /. j))) . k) by A11, FUNCT_7: 32;

                  hence thesis by A1, Def2;

                end;

              end;

              hence thesis;

            end;

          end;

          hence thesis;

        end;

        ( len ( Swap (f,i,j))) = ( len f) by Th18

        .= ( len ( Swap (f,j,i))) by Th18;

        hence thesis by A2;

      end;

        suppose

         A14: not (1 <= i & i <= ( len f) & 1 <= j & j <= ( len f));

        then ( Swap (f,i,j)) = f by Def2;

        hence thesis by A14, Def2;

      end;

    end;

    theorem :: FINSEQ_7:22

    ( rng ( Swap (f,i,j))) = ( rng f) by FUNCT_7: 103;

    theorem :: FINSEQ_7:23

    ( Swap ( <*p1, p2*>,1,2)) = <*p2, p1*>

    proof

      set f = <*p1, p2*>;

      

       A1: ( len f) = 2 by FINSEQ_1: 44;

      then 1 in ( dom f) by FINSEQ_3: 25;

      

      then

       A2: (f /. 1) = (f . 1) by PARTFUN1:def 6

      .= p1 by FINSEQ_1: 44;

      2 in ( dom f) by A1, FINSEQ_3: 25;

      

      then

       A3: (f /. 2) = (f . 2) by PARTFUN1:def 6

      .= p2 by FINSEQ_1: 44;

      ( Swap (f,1,2)) = ( Replace (( Replace (f,1,(f /. 2))),2,(f /. 1))) by A1, Def2

      .= ( Replace ( <*p2, p2*>,2,(f /. 1))) by A3, Th13;

      hence thesis by A2, Th14;

    end;

    theorem :: FINSEQ_7:24

    ( Swap ( <*p1, p2, p3*>,1,2)) = <*p2, p1, p3*>

    proof

      set f = <*p1, p2, p3*>;

      

       A1: ( len f) = 3 by FINSEQ_1: 45;

      then 1 in ( dom f) by FINSEQ_3: 25;

      

      then

       A2: (f /. 1) = (f . 1) by PARTFUN1:def 6

      .= p1 by FINSEQ_1: 45;

      2 in ( dom f) by A1, FINSEQ_3: 25;

      

      then

       A3: (f /. 2) = (f . 2) by PARTFUN1:def 6

      .= p2 by FINSEQ_1: 45;

      ( Swap (f,1,2)) = ( Replace (( Replace (f,1,(f /. 2))),2,(f /. 1))) by A1, Def2

      .= ( Replace ( <*p2, p2, p3*>,2,(f /. 1))) by A3, Th15;

      hence thesis by A2, Th16;

    end;

    theorem :: FINSEQ_7:25

    ( Swap ( <*p1, p2, p3*>,1,3)) = <*p3, p2, p1*>

    proof

      set f = <*p1, p2, p3*>;

      

       A1: ( len f) = 3 by FINSEQ_1: 45;

      then 1 in ( dom f) by FINSEQ_3: 25;

      

      then

       A2: (f /. 1) = (f . 1) by PARTFUN1:def 6

      .= p1 by FINSEQ_1: 45;

      3 in ( dom f) by A1, FINSEQ_3: 25;

      

      then

       A3: (f /. 3) = (f . 3) by PARTFUN1:def 6

      .= p3 by FINSEQ_1: 45;

      ( Swap (f,1,3)) = ( Replace (( Replace (f,1,(f /. 3))),3,(f /. 1))) by A1, Def2

      .= ( Replace ( <*p3, p2, p3*>,3,(f /. 1))) by A3, Th15;

      hence thesis by A2, Th17;

    end;

    theorem :: FINSEQ_7:26

    ( Swap ( <*p1, p2, p3*>,2,3)) = <*p1, p3, p2*>

    proof

      set f = <*p1, p2, p3*>;

      

       A1: ( len f) = 3 by FINSEQ_1: 45;

      then 2 in ( dom f) by FINSEQ_3: 25;

      

      then

       A2: (f /. 2) = (f . 2) by PARTFUN1:def 6

      .= p2 by FINSEQ_1: 45;

      3 in ( dom f) by A1, FINSEQ_3: 25;

      

      then

       A3: (f /. 3) = (f . 3) by PARTFUN1:def 6

      .= p3 by FINSEQ_1: 45;

      ( Swap (f,2,3)) = ( Replace (( Replace (f,2,(f /. 3))),3,(f /. 2))) by A1, Def2

      .= ( Replace ( <*p1, p3, p3*>,3,(f /. 2))) by A3, Th16;

      hence thesis by A2, Th17;

    end;

    theorem :: FINSEQ_7:27

    

     Th27: 1 <= i & i < j & j <= ( len f) implies ( Swap (f,i,j)) = (((((f | (i -' 1)) ^ <*(f /. j)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f /. i)*>) ^ (f /^ j))

    proof

      assume that

       A1: 1 <= i and

       A2: i < j and

       A3: j <= ( len f);

      

       A4: i <= ( len f) & 1 <= j by A1, A2, A3, XXREAL_0: 2;

      ( Swap (f,i,j)) = ( Swap (f,j,i)) by Th21

      .= ( Replace (( Replace (f,j,(f /. i))),i,(f /. j))) by A1, A3, A4, Def2;

      hence thesis by A1, A2, A3, Th11;

    end;

    theorem :: FINSEQ_7:28

    1 < i & i <= ( len f) implies ( Swap (f,1,i)) = ((( <*(f /. i)*> ^ ((f /^ 1) | (i -' 2))) ^ <*(f /. 1)*>) ^ (f /^ i))

    proof

      assume 1 < i & i <= ( len f);

      

      then ( Swap (f,1,i)) = (((((f | (1 -' 1)) ^ <*(f /. i)*>) ^ ((f /^ 1) | ((i -' 1) -' 1))) ^ <*(f /. 1)*>) ^ (f /^ i)) by Th27

      .= (((((f | 0 ) ^ <*(f /. i)*>) ^ ((f /^ 1) | ((i -' 1) -' 1))) ^ <*(f /. 1)*>) ^ (f /^ i)) by XREAL_1: 232

      .= ((( <*(f /. i)*> ^ ((f /^ 1) | ((i -' 1) -' 1))) ^ <*(f /. 1)*>) ^ (f /^ i)) by FINSEQ_1: 34;

      hence thesis by NAT_D: 45;

    end;

    theorem :: FINSEQ_7:29

    1 <= i & i < ( len f) implies ( Swap (f,i,( len f))) = ((((f | (i -' 1)) ^ <*(f /. ( len f))*>) ^ ((f /^ i) | ((( len f) -' i) -' 1))) ^ <*(f /. i)*>)

    proof

      assume 1 <= i & i < ( len f);

      

      then ( Swap (f,i,( len f))) = (((((f | (i -' 1)) ^ <*(f /. ( len f))*>) ^ ((f /^ i) | ((( len f) -' i) -' 1))) ^ <*(f /. i)*>) ^ (f /^ ( len f))) by Th27

      .= (((((f | (i -' 1)) ^ <*(f /. ( len f))*>) ^ ((f /^ i) | ((( len f) -' i) -' 1))) ^ <*(f /. i)*>) ^ {} ) by RFINSEQ: 27;

      hence thesis by FINSEQ_1: 34;

    end;

    

     Lm4: i <> k & j <> k implies (( Swap (f,i,j)) . k) = (f . k)

    proof

      per cases ;

        suppose

         A1: 1 <= i & i <= ( len f) & 1 <= j & j <= ( len f);

        assume that

         A2: i <> k and

         A3: j <> k;

        (( Replace (( Replace (f,i,(f /. j))),j,(f /. i))) . k) = (( Replace (f,i,(f /. j))) . k) by A3, FUNCT_7: 32

        .= (f . k) by A2, FUNCT_7: 32;

        hence thesis by A1, Def2;

      end;

        suppose not (1 <= i & i <= ( len f) & 1 <= j & j <= ( len f));

        hence thesis by Def2;

      end;

    end;

    theorem :: FINSEQ_7:30

    

     Th30: i <> k & j <> k & 1 <= k & k <= ( len f) implies (( Swap (f,i,j)) /. k) = (f /. k)

    proof

      assume that

       A1: i <> k & j <> k and

       A2: 1 <= k and

       A3: k <= ( len f);

      

       A4: k in ( dom f) by A2, A3, FINSEQ_3: 25;

      k <= ( len ( Swap (f,i,j))) by A3, Th18;

      then k in ( dom ( Swap (f,i,j))) by A2, FINSEQ_3: 25;

      

      hence (( Swap (f,i,j)) /. k) = (( Swap (f,i,j)) . k) by PARTFUN1:def 6

      .= (f . k) by A1, Lm4

      .= (f /. k) by A4, PARTFUN1:def 6;

    end;

    theorem :: FINSEQ_7:31

    

     Th31: 1 <= i & i <= ( len f) & 1 <= j & j <= ( len f) implies (( Swap (f,i,j)) /. i) = (f /. j) & (( Swap (f,i,j)) /. j) = (f /. i)

    proof

      assume that

       A1: 1 <= i and

       A2: i <= ( len f) and

       A3: 1 <= j and

       A4: j <= ( len f);

      

       A5: i in ( dom f) by A1, A2, FINSEQ_3: 25;

      set F = ( Swap (f,i,j));

      j <= ( len F) by A4, Th18;

      then j in ( dom F) by A3, FINSEQ_3: 25;

      

      then

       A6: (F /. j) = (F . j) by PARTFUN1:def 6

      .= (f . i) by A1, A2, A3, A4, Lm3

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

      

       A7: j in ( dom f) by A3, A4, FINSEQ_3: 25;

      i <= ( len F) by A2, Th18;

      then i in ( dom F) by A1, FINSEQ_3: 25;

      

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

      .= (f . j) by A1, A2, A3, A4, Lm3

      .= (f /. j) by A7, PARTFUN1:def 6;

      hence thesis by A6;

    end;

    begin

    theorem :: FINSEQ_7:32

    

     Th32: 1 <= i & i <= ( len f) & 1 <= j & j <= ( len f) implies ( Replace (( Swap (f,i,j)),i,p)) = ( Swap (( Replace (f,j,p)),i,j))

    proof

      assume that

       A1: 1 <= i and

       A2: i <= ( len f) and

       A3: 1 <= j and

       A4: j <= ( len f);

      

       A5: i in ( dom f) by A1, A2, FINSEQ_3: 25;

      per cases by XXREAL_0: 1;

        suppose

         A6: i = j;

        then ( Replace (( Swap (f,i,j)),i,p)) = ( Replace (f,i,p)) by Th19;

        hence thesis by A6, Th19;

      end;

        suppose

         A7: i < j;

        set N = <*(f /. j)*>;

        set M = (f | (i -' 1));

        set F = ( Swap (f,i,j));

        set P = (M ^ N);

        

         A8: F = (((P ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f /. i)*>) ^ (f /^ j)) by A1, A4, A7, Th27

        .= ((P ^ ((f /^ i) | ((j -' i) -' 1))) ^ ( <*(f /. i)*> ^ (f /^ j))) by FINSEQ_1: 32

        .= (P ^ (((f /^ i) | ((j -' i) -' 1)) ^ ( <*(f /. i)*> ^ (f /^ j)))) by FINSEQ_1: 32;

        set F1 = ( Replace (f,j,p));

        i <= ( len F1) by A2, FUNCT_7: 97;

        then

         A9: i in ( dom F1) by A1, FINSEQ_3: 25;

        

         A10: (f . i) = (F1 . i) by A7, FUNCT_7: 32

        .= (F1 /. i) by A9, PARTFUN1:def 6;

        

         A11: j <= ( len F1) by A4, FUNCT_7: 97;

        then

         A12: j in ( dom F1) by A3, FINSEQ_3: 25;

        set G1 = (f | (j -' 1));

        

         A13: (j -' 1) <= j by NAT_D: 35;

        

         A14: (i -' 1) < (j -' 1) by A1, A7, NAT_D: 56;

        then

         A15: (i -' 1) <= ( len G1) by A4, A13, FINSEQ_1: 59, XXREAL_0: 2;

        set H1 = <*p*>;

        set Q = (((f /^ i) | ((j -' i) -' 1)) ^ ( <*(f /. i)*> ^ (f /^ j)));

        

         A16: (i -' 1) <= i by NAT_D: 35;

        

         A17: i <= ( len F) by A2, Th18;

        ( len P) = (( len M) + ( len N)) by FINSEQ_1: 22

        .= (( len M) + 1) by FINSEQ_1: 39

        .= ((i -' 1) + 1) by A2, A16, FINSEQ_1: 59, XXREAL_0: 2

        .= i by A1, XREAL_1: 235;

        

        then

         A18: ( Replace (F,i,p)) = (((F | (i -' 1)) ^ <*p*>) ^ (F /^ ( len P))) by A1, A17, Def1

        .= (((F | (i -' 1)) ^ <*p*>) ^ Q) by A8, FINSEQ_5: 37

        .= ((((M ^ (N ^ Q)) | (i -' 1)) ^ <*p*>) ^ Q) by A8, FINSEQ_1: 32

        .= ((((M ^ (N ^ Q)) | ( len M)) ^ <*p*>) ^ Q) by A2, A16, FINSEQ_1: 59, XXREAL_0: 2

        .= ((M ^ <*p*>) ^ Q) by FINSEQ_5: 23;

        

         A19: ( len (G1 ^ H1)) = (( len G1) + ( len H1)) by FINSEQ_1: 22

        .= (( len G1) + 1) by FINSEQ_1: 39

        .= ((j -' 1) + 1) by A4, A13, FINSEQ_1: 59, XXREAL_0: 2

        .= j by A3, XREAL_1: 235;

        

         A20: ((F1 /^ i) | ((j -' i) -' 1)) = ((F1 /^ i) | (j -' (i + 1))) by NAT_2: 30

        .= ((F1 /^ i) | ((j -' 1) -' i)) by NAT_2: 30

        .= ((F1 | (j -' 1)) /^ i) by FINSEQ_5: 80

        .= ((((G1 ^ H1) ^ (f /^ j)) | (j -' 1)) /^ i) by A3, A4, Def1

        .= (((G1 ^ (H1 ^ (f /^ j))) | (j -' 1)) /^ i) by FINSEQ_1: 32

        .= (((G1 ^ (H1 ^ (f /^ j))) | ( len G1)) /^ i) by A4, A13, FINSEQ_1: 59, XXREAL_0: 2

        .= (G1 /^ i) by FINSEQ_5: 23

        .= ((f /^ i) | ((j -' 1) -' i)) by FINSEQ_5: 80

        .= ((f /^ i) | (j -' (1 + i))) by NAT_2: 30

        .= ((f /^ i) | ((j -' i) -' 1)) by NAT_2: 30;

        

         A21: p = (F1 . j) by A3, A4, Lm2

        .= (F1 /. j) by A12, PARTFUN1:def 6;

        

         A22: (F1 | (i -' 1)) = (((G1 ^ H1) ^ (f /^ j)) | (i -' 1)) by A3, A4, Def1

        .= ((G1 ^ (H1 ^ (f /^ j))) | (i -' 1)) by FINSEQ_1: 32

        .= (G1 | (i -' 1)) by A15, FINSEQ_5: 22

        .= (f | (i -' 1)) by A14, FINSEQ_5: 77;

        

         A23: (F1 /^ j) = (((G1 ^ H1) ^ (f /^ j)) /^ j) by A3, A4, Def1

        .= (f /^ j) by A19, FINSEQ_5: 37;

        ( Swap (F1,i,j)) = (((((F1 | (i -' 1)) ^ <*(F1 /. j)*>) ^ ((F1 /^ i) | ((j -' i) -' 1))) ^ <*(F1 /. i)*>) ^ (F1 /^ j)) by A1, A7, A11, Th27

        .= (((M ^ <*p*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ ( <*(f . i)*> ^ (f /^ j))) by A23, A22, A20, A10, A21, FINSEQ_1: 32

        .= (((M ^ <*p*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ ( <*(f /. i)*> ^ (f /^ j))) by A5, PARTFUN1:def 6

        .= ((M ^ <*p*>) ^ (((f /^ i) | ((j -' i) -' 1)) ^ ( <*(f /. i)*> ^ (f /^ j)))) by FINSEQ_1: 32;

        hence thesis by A18;

      end;

        suppose

         A24: i > j;

        then

        consider k be Nat such that

         A25: i = (j + k) by NAT_1: 10;

        reconsider i, j, k as Element of NAT by ORDINAL1:def 12;

        

         A26: (i - j) > (j - j) by A24, XREAL_1: 9;

        then

         A27: k = (i -' j) by A25, XREAL_0:def 2;

        set X = (f /^ i);

        set W = <*(f /. j)*>;

        set V = ((f /^ j) | ((i -' j) -' 1));

        set N = <*(f /. i)*>;

        set M = (f | (j -' 1));

        set F = ( Swap (f,j,i));

        set P = (M ^ N);

        

         A28: F = (((P ^ V) ^ W) ^ X) by A2, A3, A24, Th27

        .= ((P ^ V) ^ (W ^ X)) by FINSEQ_1: 32

        .= (P ^ (V ^ (W ^ X))) by FINSEQ_1: 32

        .= (P ^ ((V ^ W) ^ X)) by FINSEQ_1: 32;

        

         A29: (j - 1) >= (1 - 1) by A3, XREAL_1: 9;

        

         A30: ((k + j) -' 1) = ((k + j) - 1) by A25, A26, NAT_1: 14, NAT_D: 37

        .= (k + (j - 1))

        .= (k + (j -' 1)) by A29, XREAL_0:def 2;

        

         A31: k = (1 + (k -' 1)) by A25, A26, NAT_1: 14, XREAL_1: 235;

        set Q = ((V ^ W) ^ X);

        

         A32: (j -' 1) <= j by NAT_D: 35;

        set F1 = ( Replace (f,j,p));

        set G1 = (f | (j -' 1));

        

         A33: (j -' 1) <= j by NAT_D: 35;

        set H1 = <*p*>;

        j <= ( len F1) by A4, FUNCT_7: 97;

        then

         A34: j in ( dom F1) by A3, FINSEQ_3: 25;

        

         A35: ( len (G1 ^ H1)) = (( len G1) + ( len H1)) by FINSEQ_1: 22

        .= (( len G1) + 1) by FINSEQ_1: 39

        .= ((j -' 1) + 1) by A4, A33, FINSEQ_1: 59, XXREAL_0: 2

        .= j by A3, XREAL_1: 235;

        

        then

         A36: (F1 /^ i) = (((G1 ^ H1) ^ (f /^ j)) /^ (( len (G1 ^ H1)) + k)) by A3, A4, A25, Def1

        .= ((f /^ j) /^ k) by FINSEQ_5: 36

        .= (f /^ i) by A25, FINSEQ_6: 81;

        k >= 1 by A25, A26, NAT_1: 14;

        then

         A37: (k - 1) >= (1 - 1) by XREAL_1: 9;

        

         A38: ((j + k) -' 1) = ((j + k) - 1) by A3, NAT_D: 37

        .= (j + (k - 1))

        .= (j + (k -' 1)) by A37, XREAL_0:def 2;

        

         A39: i <= ( len F1) by A2, FUNCT_7: 97;

        then

         A40: i in ( dom F1) by A1, FINSEQ_3: 25;

        

         A41: ((F1 /^ j) | ((i -' j) -' 1)) = ((F1 /^ j) | (i -' (j + 1))) by NAT_2: 30

        .= ((F1 /^ j) | ((i -' 1) -' j)) by NAT_2: 30

        .= ((F1 | (i -' 1)) /^ j) by FINSEQ_5: 80

        .= ((((G1 ^ H1) ^ (f /^ j)) | (j + (k -' 1))) /^ j) by A3, A4, A25, A38, Def1

        .= (((G1 ^ H1) ^ ((f /^ j) | (k -' 1))) /^ ( len (G1 ^ H1))) by A35, GENEALG1: 2

        .= ((f /^ j) | ((i -' j) -' 1)) by A27, FINSEQ_5: 37;

        

         A42: (F1 | (j -' 1)) = (((G1 ^ H1) ^ (f /^ j)) | (j -' 1)) by A3, A4, Def1

        .= ((G1 ^ (H1 ^ (f /^ j))) | (j -' 1)) by FINSEQ_1: 32

        .= ((G1 ^ (H1 ^ (f /^ j))) | ( len G1)) by A4, A33, FINSEQ_1: 59, XXREAL_0: 2

        .= G1 by FINSEQ_5: 23;

        

         A43: p = (F1 . j) by A3, A4, Lm2

        .= (F1 /. j) by A34, PARTFUN1:def 6;

        

         A44: (f . i) = (F1 . i) by A24, FUNCT_7: 32

        .= (F1 /. i) by A40, PARTFUN1:def 6;

        

         A45: ( Swap (F1,i,j)) = ( Swap (F1,j,i)) by Th21

        .= (((((F1 | (j -' 1)) ^ <*(F1 /. i)*>) ^ ((F1 /^ j) | ((i -' j) -' 1))) ^ <*(F1 /. j)*>) ^ (F1 /^ i)) by A3, A24, A39, Th27

        .= (((((f | (j -' 1)) ^ <*(f /. i)*>) ^ ((f /^ j) | ((i -' j) -' 1))) ^ <*p*>) ^ (f /^ i)) by A5, A36, A42, A41, A44, A43, PARTFUN1:def 6;

        

         A46: (i -' j) <> 0 by A26, XREAL_0:def 2;

        (i -' 1) <= i by NAT_D: 35;

        then (i -' 1) <= ( len f) by A2, XXREAL_0: 2;

        then ((i -' 1) -' j) <= (( len f) -' j) by NAT_D: 42;

        then ((i -' 1) -' j) <= ( len (f /^ j)) by RFINSEQ: 29;

        then (i -' (1 + j)) <= ( len (f /^ j)) by NAT_2: 30;

        then

         A47: ((i -' j) -' 1) <= ( len (f /^ j)) by NAT_2: 30;

        then

         A48: ( len V) = (k -' 1) by A27, FINSEQ_1: 59;

        

         A49: ( len P) = (( len M) + ( len N)) by FINSEQ_1: 22

        .= (( len M) + 1) by FINSEQ_1: 39

        .= ((j -' 1) + 1) by A4, A32, FINSEQ_1: 59, XXREAL_0: 2

        .= j by A3, XREAL_1: 235;

        

         A50: i <= ( len F) by A2, Th18;

        

         A51: ( len (V ^ W)) = (( len V) + ( len W)) by FINSEQ_1: 22

        .= (( len V) + 1) by FINSEQ_1: 39

        .= (((i -' j) -' 1) + 1) by A47, FINSEQ_1: 59

        .= (i -' j) by A46, NAT_1: 14, XREAL_1: 235;

        ( Replace (( Swap (f,i,j)),i,p)) = ( Replace (F,i,p)) by Th21

        .= (((F | (i -' 1)) ^ <*p*>) ^ ((P ^ Q) /^ (j + k))) by A1, A25, A28, A50, Def1

        .= (((F | (i -' 1)) ^ <*p*>) ^ (((V ^ W) ^ X) /^ ( len (V ^ W)))) by A27, A49, A51, FINSEQ_5: 36

        .= (((F | (k + (j -' 1))) ^ <*p*>) ^ X) by A25, A30, FINSEQ_5: 37

        .= ((((M ^ (N ^ Q)) | ((j -' 1) + k)) ^ <*p*>) ^ X) by A28, FINSEQ_1: 32

        .= ((((M ^ (N ^ Q)) | (( len M) + k)) ^ <*p*>) ^ X) by A4, A32, FINSEQ_1: 59, XXREAL_0: 2

        .= (((M ^ ((N ^ Q) | k)) ^ <*p*>) ^ X) by GENEALG1: 2

        .= (((M ^ ((N ^ Q) | (( len N) + (k -' 1)))) ^ <*p*>) ^ X) by A31, FINSEQ_1: 39

        .= (((M ^ (N ^ (Q | (k -' 1)))) ^ <*p*>) ^ X) by GENEALG1: 2

        .= (((M ^ (N ^ ((V ^ (W ^ X)) | (k -' 1)))) ^ <*p*>) ^ X) by FINSEQ_1: 32

        .= (((M ^ (N ^ V)) ^ <*p*>) ^ X) by A48, FINSEQ_5: 23

        .= ((((M ^ N) ^ V) ^ <*p*>) ^ X) by FINSEQ_1: 32;

        hence thesis by A45;

      end;

    end;

    theorem :: FINSEQ_7:33

    

     Th33: i <> k & j <> k & 1 <= i & i <= ( len f) & 1 <= j & j <= ( len f) implies ( Swap (( Replace (f,k,p)),i,j)) = ( Replace (( Swap (f,i,j)),k,p))

    proof

      assume that

       A1: i <> k and

       A2: j <> k and

       A3: 1 <= i and

       A4: i <= ( len f) and

       A5: 1 <= j and

       A6: j <= ( len f);

      i <= ( len ( Replace (f,k,p))) & j <= ( len ( Replace (f,k,p))) by A4, A6, FUNCT_7: 97;

      

      hence ( Swap (( Replace (f,k,p)),i,j)) = ( Replace (( Replace (( Replace (f,k,p)),i,(( Replace (f,k,p)) /. j))),j,(( Replace (f,k,p)) /. i))) by A3, A5, Def2

      .= ( Replace (( Replace (( Replace (f,k,p)),i,(f /. j))),j,(( Replace (f,k,p)) /. i))) by A2, A5, A6, Th10

      .= ( Replace (( Replace (( Replace (f,k,p)),i,(f /. j))),j,(f /. i))) by A1, A3, A4, Th10

      .= ( Replace (( Replace (( Replace (f,i,(f /. j))),k,p)),j,(f /. i))) by A1, FUNCT_7: 33

      .= ( Replace (( Replace (( Replace (f,i,(f /. j))),j,(f /. i))),k,p)) by A2, FUNCT_7: 33

      .= ( Replace (( Swap (f,i,j)),k,p)) by A3, A4, A5, A6, Def2;

    end;

    theorem :: FINSEQ_7:34

    i <> k & j <> k & 1 <= i & i <= ( len f) & 1 <= j & j <= ( len f) & 1 <= k & k <= ( len f) implies ( Swap (( Swap (f,i,j)),j,k)) = ( Swap (( Swap (f,i,k)),i,j))

    proof

      assume that

       A1: i <> k & j <> k and

       A2: 1 <= i and

       A3: i <= ( len f) and

       A4: 1 <= j and

       A5: j <= ( len f) and

       A6: 1 <= k and

       A7: k <= ( len f);

      

       A8: i <= ( len ( Replace (f,i,(f /. k)))) & j <= ( len ( Replace (f,i,(f /. k)))) by A3, A5, FUNCT_7: 97;

      j <= ( len ( Swap (f,i,j))) & k <= ( len ( Swap (f,i,j))) by A5, A7, Th18;

      

      hence ( Swap (( Swap (f,i,j)),j,k)) = ( Replace (( Replace (( Swap (f,i,j)),j,(( Swap (f,i,j)) /. k))),k,(( Swap (f,i,j)) /. j))) by A4, A6, Def2

      .= ( Replace (( Replace (( Swap (f,i,j)),j,(( Swap (f,i,j)) /. k))),k,(f /. i))) by A2, A3, A4, A5, Th31

      .= ( Replace (( Replace (( Swap (f,i,j)),j,(f /. k))),k,(f /. i))) by A1, A6, A7, Th30

      .= ( Replace (( Replace (( Swap (f,j,i)),j,(f /. k))),k,(f /. i))) by Th21

      .= ( Replace (( Swap (( Replace (f,i,(f /. k))),j,i)),k,(f /. i))) by A2, A3, A4, A5, Th32

      .= ( Swap (( Replace (( Replace (f,i,(f /. k))),k,(f /. i))),j,i)) by A1, A2, A4, A8, Th33

      .= ( Swap (( Swap (f,i,k)),j,i)) by A2, A3, A6, A7, Def2

      .= ( Swap (( Swap (f,i,k)),i,j)) by Th21;

    end;

    theorem :: FINSEQ_7:35

    i <> k & j <> k & l <> i & l <> j & 1 <= i & i <= ( len f) & 1 <= j & j <= ( len f) & 1 <= k & k <= ( len f) & 1 <= l & l <= ( len f) implies ( Swap (( Swap (f,i,j)),k,l)) = ( Swap (( Swap (f,k,l)),i,j))

    proof

      assume that

       A1: i <> k & j <> k and

       A2: l <> i & l <> j and

       A3: 1 <= i and

       A4: i <= ( len f) and

       A5: 1 <= j and

       A6: j <= ( len f) and

       A7: 1 <= k and

       A8: k <= ( len f) and

       A9: 1 <= l and

       A10: l <= ( len f);

      

       A11: i <= ( len ( Replace (f,k,(f /. l)))) & j <= ( len ( Replace (f,k,(f /. l)))) by A4, A6, FUNCT_7: 97;

      set F = ( Swap (f,i,j));

      k <= ( len F) & l <= ( len F) by A8, A10, Th18;

      

      then ( Swap (F,k,l)) = ( Replace (( Replace (F,k,(F /. l))),l,(F /. k))) by A7, A9, Def2

      .= ( Replace (( Replace (F,k,(F /. l))),l,(f /. k))) by A1, A7, A8, Th30

      .= ( Replace (( Replace (F,k,(f /. l))),l,(f /. k))) by A2, A9, A10, Th30

      .= ( Replace (( Replace (( Swap (f,j,i)),k,(f /. l))),l,(f /. k))) by Th21

      .= ( Replace (( Swap (( Replace (f,k,(f /. l))),j,i)),l,(f /. k))) by A1, A3, A4, A5, A6, Th33

      .= ( Swap (( Replace (( Replace (f,k,(f /. l))),l,(f /. k))),j,i)) by A2, A3, A5, A11, Th33

      .= ( Swap (( Swap (f,k,l)),j,i)) by A7, A8, A9, A10, Def2

      .= ( Swap (( Swap (f,k,l)),i,j)) by Th21;

      hence thesis;

    end;