gobrd10.miz



    begin

    reserve i,j,k,k1,k2,n,m,i1,i2,j1,j2 for Element of NAT ,

x for set;

    definition

      let i1,i2 be Nat;

      :: GOBRD10:def1

      pred i1,i2 are_adjacent means i2 = (i1 + 1) or i1 = (i2 + 1);

      symmetry ;

      irreflexivity ;

    end

    notation

      let i,j be Nat;

      antonym i,j aren't_adjacent for i,j are_adjacent ;

    end

    theorem :: GOBRD10:1

    for i1,i2 be Nat st (i1,i2) are_adjacent holds ((i1 + 1),(i2 + 1)) are_adjacent ;

    theorem :: GOBRD10:2

    

     Th2: for i1,i2 be Nat st (i1,i2) are_adjacent & 1 <= i1 & 1 <= i2 holds ((i1 -' 1),(i2 -' 1)) are_adjacent

    proof

      let i1,i2 be Nat;

      assume that

       A1: (i1,i2) are_adjacent and

       A2: 1 <= i1 and

       A3: 1 <= i2;

       0 <= (i1 - 1) by A2, XREAL_1: 48;

      then

       A4: (i1 -' 1) = (i1 - 1) by XREAL_0:def 2;

       0 <= (i2 - 1) by A3, XREAL_1: 48;

      then

       A5: (i2 -' 1) = (i2 - 1) by XREAL_0:def 2;

      i2 = (i1 + 1) or i1 = (i2 + 1) by A1;

      then (i2 - 1) = ((i1 - 1) + 1) or (i1 - 1) = ((i2 - 1) + 1);

      hence thesis by A4, A5;

    end;

    definition

      let i1,j1,i2,j2 be Nat;

      :: GOBRD10:def2

      pred i1,j1,i2,j2 are_adjacent means (i1,i2) are_adjacent & j1 = j2 or i1 = i2 & (j1,j2) are_adjacent ;

    end

    theorem :: GOBRD10:3

    

     Th3: for i1,i2,j1,j2 be Nat st (i1,j1,i2,j2) are_adjacent holds ((i1 + 1),(j1 + 1),(i2 + 1),(j2 + 1)) are_adjacent

    proof

      let i1,i2,j1,j2 be Nat;

      assume (i1,j1,i2,j2) are_adjacent ;

      then (i1,i2) are_adjacent & j1 = j2 or i1 = i2 & (j1,j2) are_adjacent ;

      then ((i1 + 1),(i2 + 1)) are_adjacent & (j1 + 1) = (j2 + 1) or (i1 + 1) = (i2 + 1) & ((j1 + 1),(j2 + 1)) are_adjacent ;

      hence thesis;

    end;

    theorem :: GOBRD10:4

    for i1,i2,j1,j2 be Nat st (i1,j1,i2,j2) are_adjacent & 1 <= i1 & 1 <= i2 & 1 <= j1 & 1 <= j2 holds ((i1 -' 1),(j1 -' 1),(i2 -' 1),(j2 -' 1)) are_adjacent by Th2;

    

     Lm1: for n, i, j st 1 <= j & j <= n holds ((n |-> i) . j) = i by FINSEQ_1: 1, FINSEQ_2: 57;

    theorem :: GOBRD10:5

    

     Th5: for n, i, j st i <= n & j <= n holds ex fs1 be FinSequence of NAT st (fs1 . 1) = i & (fs1 . ( len fs1)) = j & ( len fs1) = (((i -' j) + (j -' i)) + 1) & (for k, k1 st 1 <= k & k <= ( len fs1) & k1 = (fs1 . k) holds k1 <= n) & for i1 st 1 <= i1 & i1 < ( len fs1) holds (fs1 . (i1 + 1)) = ((fs1 /. i1) + 1) or (fs1 . i1) = ((fs1 /. (i1 + 1)) + 1)

    proof

      let n, i, j;

      assume that

       A1: i <= n and

       A2: j <= n;

      now

        per cases by XXREAL_0: 1;

          case

           A3: i < j;

          then (i - j) < (j - j) by XREAL_1: 9;

          then

           A4: (i -' j) = 0 by XREAL_0:def 2;

          (j - i) > 0 by A3, XREAL_1: 50;

          then

           A5: ((j - i) + 1) > ( 0 + 1) by XREAL_1: 6;

          then ((j + 1) - i) >= 0 ;

          then

           A6: ((j + 1) -' i) = ((j - i) + 1) by XREAL_0:def 2;

          then

           A7: ((i + ((j + 1) -' i)) -' 1) = ((i + ((j + 1) -' i)) - 1) by XREAL_0:def 2;

          deffunc F( Nat) = ((i + $1) -' 1);

          ex p be FinSequence st ( len p) = ((j + 1) -' i) & for k be Nat st k in ( dom p) holds (p . k) = F(k) from FINSEQ_1:sch 2;

          then

          consider p be FinSequence such that

           A8: ( len p) = ((j + 1) -' i) and

           A9: for k be Nat st k in ( dom p) holds (p . k) = ((i + k) -' 1);

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

          then

           A10: ( len p) = (((i -' j) + (j -' i)) + 1) by A8, A6, A4, XREAL_0:def 2;

          

           A11: ((j + 1) -' i) = ((j + 1) - i) by A5, XREAL_0:def 2;

          then 1 in ( dom p) by A5, A8, FINSEQ_3: 25;

          then (p . 1) = ((i + 1) -' 1) by A9;

          then

           A12: (p . 1) = i by NAT_D: 34;

          ( rng p) c= NAT

          proof

            let x be object;

            assume x in ( rng p);

            then

            consider y be object such that

             A13: y in ( dom p) and

             A14: (p . y) = x by FUNCT_1:def 3;

            y in ( Seg ( len p)) by A13, FINSEQ_1:def 3;

            then y in { k where k be Nat : 1 <= k & k <= ( len p) } by FINSEQ_1:def 1;

            then

            consider k be Nat such that

             A15: k = y and 1 <= k and k <= ( len p);

            (p . k) = ((i + k) -' 1) by A9, A13, A15;

            hence thesis by A14, A15;

          end;

          then

          reconsider fs2 = p as FinSequence of NAT by FINSEQ_1:def 4;

          

           A16: for i1 st 1 <= i1 & i1 < ( len fs2) holds (fs2 . (i1 + 1)) = ((fs2 /. i1) + 1) or (fs2 . i1) = ((fs2 /. (i1 + 1)) + 1)

          proof

            let i1;

            assume that

             A17: 1 <= i1 and

             A18: i1 < ( len fs2);

            

             A19: 1 <= (1 + i1) by NAT_1: 11;

            (i1 + 1) <= ( len fs2) by A18, NAT_1: 13;

            then (i1 + 1) in ( dom p) by A19, FINSEQ_3: 25;

            then

             A20: (fs2 . (i1 + 1)) = ((i + (i1 + 1)) -' 1) by A9;

            (1 + (i + i1)) >= 1 by NAT_1: 11;

            then ((1 + (i + i1)) - 1) >= (1 - 1) by XREAL_1: 9;

            then

             A21: ((1 + (i + i1)) -' 1) = (i + i1) by XREAL_0:def 2;

            (i + i1) >= (1 + 0 ) by A17, XREAL_1: 7;

            then ((i + i1) - 1) >= (1 - 1) by XREAL_1: 9;

            

            then

             A22: (1 + ((i + i1) -' 1)) = (1 + ((i + i1) - 1)) by XREAL_0:def 2

            .= (i + i1);

            i1 in ( dom fs2) & (fs2 /. i1) = (fs2 . i1) by A17, A18, FINSEQ_3: 25, FINSEQ_4: 15;

            hence thesis by A9, A20, A22, A21;

          end;

          

           A23: for k, k1 st 1 <= k & k <= ( len p) & k1 = (p . k) holds k1 <= n

          proof

            let k, k1;

            assume that

             A24: 1 <= k and

             A25: k <= ( len p) and

             A26: k1 = (p . k);

            k in ( dom p) by A24, A25, FINSEQ_3: 25;

            then

             A27: k1 = ((k + i) -' 1) by A9, A26;

            ((k + i) - 1) = (k + (i - 1));

            then (1 + (i - 1)) <= ((k + i) - 1) by A24, XREAL_1: 6;

            then

             A28: k1 = ((k + i) - 1) by A27, XREAL_0:def 2;

            (k + i) <= (((j + 1) -' i) + i) by A8, A25, XREAL_1: 6;

            then (k + i) <= (((j + 1) - i) + i) by A5, XREAL_0:def 2;

            then k1 <= ((j + 1) - 1) by A28, XREAL_1: 9;

            hence thesis by A2, XXREAL_0: 2;

          end;

          ( len p) in ( dom p) by A5, A8, A11, FINSEQ_3: 25;

          then (p . ( len p)) = j by A8, A9, A11, A7;

          hence thesis by A23, A12, A10, A16;

        end;

          case

           A29: i = j;

          then (i - j) = 0 ;

          then

           A30: (i -' j) = 0 by XREAL_0:def 2;

          consider f be Function such that

           A31: ( dom f) = ( Seg 1) and

           A32: ( rng f) = {i} by FUNCT_1: 5;

          ( rng f) c= NAT & f is FinSequence-like by A31, A32, FINSEQ_1:def 2, ZFMISC_1: 31;

          then

          reconsider fs1 = f as FinSequence of NAT by FINSEQ_1:def 4;

          

           A33: for i1 st 1 <= i1 & i1 < ( len fs1) holds (fs1 . (i1 + 1)) = ((fs1 /. i1) + 1) or (fs1 . i1) = ((fs1 /. (i1 + 1)) + 1) by A31, FINSEQ_1:def 3;

          1 in ( dom f) by A31, FINSEQ_1: 1;

          then (fs1 . 1) in ( rng f) by FUNCT_1:def 3;

          then

           A34: (fs1 . 1) = i by A32, TARSKI:def 1;

          

           A35: ( len fs1) = 1 by A31, FINSEQ_1:def 3;

          then for k, k1 st 1 <= k & k <= ( len fs1) & k1 = (fs1 . k) holds k1 <= n by A1, A34, XXREAL_0: 1;

          hence thesis by A29, A34, A35, A30, A33;

        end;

          case

           A36: j < i;

          then

           A37: (i - j) >= (j - j) by XREAL_1: 9;

           A38:

          now

            per cases by A37;

              case (i - j) = 0 ;

              hence (j -' i) = 0 by XREAL_0:def 2;

            end;

              case (i - j) > 0 ;

              then ( - ( - (i - j))) > 0 ;

              then (j - i) < 0 ;

              hence (j -' i) = 0 by XREAL_0:def 2;

            end;

          end;

          (j - i) < (i - i) by A36, XREAL_1: 9;

          then (j -' i) = 0 by XREAL_0:def 2;

          

          then

           A39: (((i -' j) + (j -' i)) + 1) = (((i - j) + 1) + (j -' i)) by A37, XREAL_0:def 2

          .= ((i + 1) - j) by A38;

          deffunc F( Nat) = ((i + 1) -' $1);

          

           A40: ((i + 1) - 1) >= 0 ;

          (i - j) > 0 by A36, XREAL_1: 50;

          then

           A41: ((i - j) + 1) > ( 0 + 1) by XREAL_1: 6;

          

          then

           A42: ((i + 1) - ((i + 1) -' j)) = ((i + 1) - ((i + 1) - j)) by XREAL_0:def 2

          .= j;

          ex p be FinSequence st ( len p) = ((i + 1) -' j) & for k be Nat st k in ( dom p) holds (p . k) = F(k) from FINSEQ_1:sch 2;

          then

          consider p be FinSequence such that

           A43: ( len p) = ((i + 1) -' j) and

           A44: for k be Nat st k in ( dom p) holds (p . k) = ((i + 1) -' k);

          

           A45: ((i + 1) -' j) = ((i + 1) - j) by A41, XREAL_0:def 2;

          then 1 in ( dom p) by A41, A43, FINSEQ_3: 25;

          then (p . 1) = ((i + 1) -' 1) by A44;

          then

           A46: (p . 1) = i by A40, XREAL_0:def 2;

          ( rng p) c= NAT

          proof

            let x be object;

            assume x in ( rng p);

            then

            consider y be object such that

             A47: y in ( dom p) and

             A48: (p . y) = x by FUNCT_1:def 3;

            y in ( Seg ( len p)) by A47, FINSEQ_1:def 3;

            then y in { k where k be Nat : 1 <= k & k <= ( len p) } by FINSEQ_1:def 1;

            then

            consider k be Nat such that

             A49: k = y and

             A50: 1 <= k & k <= ( len p);

            k in ( dom p) by A50, FINSEQ_3: 25;

            then (p . k) = ((i + 1) -' k) by A44;

            hence thesis by A48, A49;

          end;

          then

          reconsider fs2 = p as FinSequence of NAT by FINSEQ_1:def 4;

          ((i - j) + 1) >= ( 0 + 1) by A37, XREAL_1: 6;

          then

           A51: ((i + 1) - j) >= 0 ;

          

           A52: for i1 st 1 <= i1 & i1 < ( len fs2) holds (fs2 . (i1 + 1)) = ((fs2 /. i1) + 1) or (fs2 . i1) = ((fs2 /. (i1 + 1)) + 1)

          proof

            let i1;

            assume that

             A53: 1 <= i1 and

             A54: i1 < ( len fs2);

            

             A55: (i1 + 1) <= ( len fs2) by A54, NAT_1: 13;

            then (i1 + 1) <= ((i - j) + 1) by A43, A51, XREAL_0:def 2;

            then i1 <= (i - j) by XREAL_1: 6;

            then (i1 + j) <= i by XREAL_1: 19;

            then j <= (i - i1) by XREAL_1: 19;

            

            then

             A56: (1 + ((i + 1) -' (i1 + 1))) = (1 + ((i + 1) - (i1 + 1))) by XREAL_0:def 2

            .= ((i + 1) - i1);

            

             A57: 1 <= (i1 + 1) by A53, NAT_1: 13;

            then (i1 + 1) in ( dom fs2) by A55, FINSEQ_3: 25;

            then (fs2 . (i1 + 1)) = ((i + 1) -' (i1 + 1)) by A44;

            then

             A58: ((fs2 /. (i1 + 1)) + 1) = (1 + ((i + 1) -' (i1 + 1))) by A57, A55, FINSEQ_4: 15;

            i1 in ( dom fs2) by A53, A54, FINSEQ_3: 25;

            then (fs2 . i1) = ((i + 1) -' i1) by A44;

            hence thesis by A58, A56, XREAL_0:def 2;

          end;

          

           A59: for k, k1 st 1 <= k & k <= ( len p) & k1 = (p . k) holds k1 <= n

          proof

            let k, k1;

            assume that

             A60: 1 <= k and

             A61: k <= ( len p) and

             A62: k1 = (p . k);

            k <= ((i + 1) - j) by A43, A60, A61, XREAL_0:def 2;

            then (k + j) <= (((i + 1) - j) + j) by XREAL_1: 6;

            then

             A63: ((k + j) - k) <= ((i + 1) - k) by XREAL_1: 9;

            ( - k) <= ( - 1) by A60, XREAL_1: 24;

            then

             A64: (( - k) + (i + 1)) <= (( - 1) + (i + 1)) by XREAL_1: 6;

            k in ( dom p) by A60, A61, FINSEQ_3: 25;

            then k1 = ((i + 1) -' k) by A44, A62;

            then k1 = ((i + 1) - k) by A63, XREAL_0:def 2;

            hence thesis by A1, A64, XXREAL_0: 2;

          end;

          ( len p) in ( dom p) by A41, A43, A45, FINSEQ_3: 25;

          

          then (p . ( len p)) = ((i + 1) -' ((i + 1) -' j)) by A43, A44

          .= j by A42, XREAL_0:def 2;

          hence thesis by A43, A59, A45, A46, A39, A52;

        end;

      end;

      hence thesis;

    end;

    theorem :: GOBRD10:6

    

     Th6: for n, i, j st i <= n & j <= n holds ex fs1 be FinSequence of NAT st (fs1 . 1) = i & (fs1 . ( len fs1)) = j & ( len fs1) = (((i -' j) + (j -' i)) + 1) & (for k, k1 st 1 <= k & k <= ( len fs1) & k1 = (fs1 . k) holds k1 <= n) & for i1 st 1 <= i1 & i1 < ( len fs1) holds ((fs1 /. i1),(fs1 /. (i1 + 1))) are_adjacent

    proof

      let n, i, j;

      assume i <= n & j <= n;

      then

      consider fs1 be FinSequence of NAT such that

       A1: (fs1 . 1) = i & (fs1 . ( len fs1)) = j & (( len fs1) = (((i -' j) + (j -' i)) + 1) & for k, k1 st 1 <= k & k <= ( len fs1) & k1 = (fs1 . k) holds k1 <= n) and

       A2: for i1 st 1 <= i1 & i1 < ( len fs1) holds (fs1 . (i1 + 1)) = ((fs1 /. i1) + 1) or (fs1 . i1) = ((fs1 /. (i1 + 1)) + 1) by Th5;

      for i1 st 1 <= i1 & i1 < ( len fs1) holds ((fs1 /. i1),(fs1 /. (i1 + 1))) are_adjacent

      proof

        let i1;

        assume

         A3: 1 <= i1 & i1 < ( len fs1);

        then

         A4: (fs1 . i1) = (fs1 /. i1) by FINSEQ_4: 15;

        1 <= (i1 + 1) & (i1 + 1) <= ( len fs1) by A3, NAT_1: 13;

        then

         A5: (fs1 . (i1 + 1)) = (fs1 /. (i1 + 1)) by FINSEQ_4: 15;

        (fs1 . (i1 + 1)) = ((fs1 /. i1) + 1) or (fs1 . i1) = ((fs1 /. (i1 + 1)) + 1) by A2, A3;

        hence thesis by A5, A4;

      end;

      hence thesis by A1;

    end;

    theorem :: GOBRD10:7

    

     Th7: for n, m, i1, j1, i2, j2 st i1 <= n & j1 <= m & i2 <= n & j2 <= m holds ex fs1,fs2 be FinSequence of NAT st (for i, k1, k2 st i in ( dom fs1) & k1 = (fs1 . i) & k2 = (fs2 . i) holds k1 <= n & k2 <= m) & (fs1 . 1) = i1 & (fs1 . ( len fs1)) = i2 & (fs2 . 1) = j1 & (fs2 . ( len fs2)) = j2 & ( len fs1) = ( len fs2) & ( len fs1) = (((((i1 -' i2) + (i2 -' i1)) + (j1 -' j2)) + (j2 -' j1)) + 1) & for i st 1 <= i & i < ( len fs1) holds ((fs1 /. i),(fs2 /. i),(fs1 /. (i + 1)),(fs2 /. (i + 1))) are_adjacent

    proof

      let n, m, i1, j1, i2, j2;

      assume that

       A1: i1 <= n and

       A2: j1 <= m and

       A3: i2 <= n and

       A4: j2 <= m;

      consider gs1 be FinSequence of NAT such that

       A5: (gs1 . 1) = i1 and

       A6: (gs1 . ( len gs1)) = i2 and

       A7: ( len gs1) = (((i1 -' i2) + (i2 -' i1)) + 1) and

       A8: for k, k1 st 1 <= k & k <= ( len gs1) & k1 = (gs1 . k) holds k1 <= n and

       A9: for k st 1 <= k & k < ( len gs1) holds ((gs1 /. k),(gs1 /. (k + 1))) are_adjacent by A1, A3, Th6;

      consider gs2 be FinSequence of NAT such that

       A10: (gs2 . 1) = j1 and

       A11: (gs2 . ( len gs2)) = j2 and

       A12: ( len gs2) = (((j1 -' j2) + (j2 -' j1)) + 1) and

       A13: for k, k1 st 1 <= k & k <= ( len gs2) & k1 = (gs2 . k) holds k1 <= m and

       A14: for k st 1 <= k & k < ( len gs2) holds ((gs2 /. k),(gs2 /. (k + 1))) are_adjacent by A2, A4, Th6;

      

       A15: 1 <= ( len gs2) by A12, NAT_1: 11;

      then

       A16: (( len gs2) - 1) >= (1 - 1) by XREAL_1: 9;

      set hs1 = (gs1 ^ ((( len gs2) -' 1) |-> i2)), hs2 = (((( len gs1) -' 1) |-> j1) ^ gs2);

      

       A17: ( len hs1) = (( len gs1) + ( len ((( len gs2) -' 1) |-> i2))) by FINSEQ_1: 22

      .= (( len gs1) + (( len gs2) -' 1)) by CARD_1:def 7

      .= (( len gs1) + (( len gs2) - 1)) by A16, XREAL_0:def 2

      .= ((( len gs1) - 1) + ( len gs2));

      

       A18: 1 <= ( len gs1) by A7, NAT_1: 11;

      then

       A19: (( len gs1) - 1) >= (1 - 1) by XREAL_1: 9;

      

      then

       A20: ((( len gs1) - 1) + ( len gs2)) = ((( len gs1) -' 1) + ( len gs2)) by XREAL_0:def 2

      .= (( len ((( len gs1) -' 1) |-> j1)) + ( len gs2)) by CARD_1:def 7

      .= ( len hs2) by FINSEQ_1: 22;

      

       A21: for i, k1, k2 st i in ( dom hs1) & k1 = (hs1 . i) & k2 = (hs2 . i) holds k1 <= n & k2 <= m

      proof

        ( dom hs2) = ( Seg (( len ((( len gs1) -' 1) |-> j1)) + ( len gs2))) by FINSEQ_1:def 7;

        then ( len hs2) = (( len ((( len gs1) -' 1) |-> j1)) + ( len gs2)) by FINSEQ_1:def 3;

        then

         A22: ( len hs2) = ((( len gs1) -' 1) + ( len gs2)) by CARD_1:def 7;

        let i, k1, k2;

        assume that

         A23: i in ( dom hs1) and

         A24: k1 = (hs1 . i) and

         A25: k2 = (hs2 . i);

        i in ( Seg ( len hs1)) by A23, FINSEQ_1:def 3;

        then 1 <= i & i <= (( len gs1) -' 1) or ((( len gs1) -' 1) + 1) <= i & i <= ( len hs2) by A17, A20, FINSEQ_1: 1, NAT_1: 13;

        then 1 <= i & i <= (( len gs1) -' 1) or ((( len gs1) - 1) + 1) <= i & i <= ( len hs2) by A19, XREAL_0:def 2;

        then 1 <= i & i <= (( len gs1) - 1) or (( len gs1) - (( len gs1) - 1)) <= (i - (( len gs1) - 1)) & i <= ( len hs2) by XREAL_0:def 2, XREAL_1: 9;

        then 1 <= i & i <= (( len gs1) - 1) or 1 <= (i - (( len gs1) - 1)) & (i - (( len gs1) - 1)) <= (( len hs2) - (( len gs1) - 1)) by XREAL_1: 9;

        then

         A26: 1 <= i & i <= (( len gs1) - 1) or 1 <= ((i - ( len gs1)) + 1) & ((i - ( len gs1)) + 1) <= ((( len hs2) - ( len gs1)) + 1);

         A27:

        now

          per cases by A26, XREAL_1: 6;

            case

             A28: 1 <= ((i - ( len gs1)) + 1) & (i - ( len gs1)) <= (( len hs2) - ( len gs1));

            then

             A29: ((i + 1) - ( len gs1)) <= ((( len hs2) - ( len gs1)) + 1) by XREAL_1: 6;

            

             A30: ( len ((( len gs1) -' 1) |-> j1)) = (( len gs1) -' 1) by CARD_1:def 7;

            

             A31: ((( len hs2) + 1) - ( len gs1)) = ((((( len gs1) - 1) + ( len gs2)) + 1) - ( len gs1)) by A19, A22, XREAL_0:def 2

            .= ( len gs2);

            

             A32: ((i + 1) - ( len gs1)) = ((i + 1) -' ( len gs1)) by A28, XREAL_0:def 2;

            ((i - ( len gs1)) + 1) <= ((( len hs2) - ( len gs1)) + 1) by A28, XREAL_1: 6;

            then ((i + 1) -' ( len gs1)) in ( Seg ( len gs2)) by A28, A31, A32, FINSEQ_1: 1;

            then

             A33: ((i + 1) -' ( len gs1)) in ( dom gs2) by FINSEQ_1:def 3;

            i = ((( len gs1) - 1) + ((i + 1) - ( len gs1)))

            .= (( len ((( len gs1) -' 1) |-> j1)) + ((i + 1) -' ( len gs1))) by A19, A32, A30, XREAL_0:def 2;

            then (hs2 . i) = (gs2 . ((i + 1) -' ( len gs1))) by A33, FINSEQ_1:def 7;

            hence k2 <= m by A13, A25, A28, A29, A31, A32;

          end;

            case

             A34: 1 <= i & i <= (( len gs1) - 1);

            then

             A35: i <= (( len gs1) -' 1) by XREAL_0:def 2;

            then i in ( Seg (( len gs1) -' 1)) by A34, FINSEQ_1: 1;

            then i in ( Seg ( len ((( len gs1) -' 1) |-> j1))) by CARD_1:def 7;

            then i in ( dom ((( len gs1) -' 1) |-> j1)) by FINSEQ_1:def 3;

            

            then (hs2 . i) = (((( len gs1) -' 1) |-> j1) . i) by FINSEQ_1:def 7

            .= j1 by A34, A35, Lm1;

            hence k2 <= m by A2, A25;

          end;

        end;

        ( dom hs1) = ( Seg (( len gs1) + ( len ((( len gs2) -' 1) |-> i2)))) by FINSEQ_1:def 7;

        then

         A36: ( len hs1) = (( len gs1) + ( len ((( len gs2) -' 1) |-> i2))) by FINSEQ_1:def 3;

        then

         A37: (( len hs1) -' ( len gs1)) = (( len hs1) - ( len gs1)) by XREAL_0:def 2;

        

         A38: ( len hs1) = (( len gs1) + (( len gs2) -' 1)) by A36, CARD_1:def 7;

        

         A39: 1 <= i & i <= ( len gs1) or (( len gs1) - ( len gs1)) < (i - ( len gs1)) & i <= ( len hs1) by A23, FINSEQ_3: 25, XREAL_1: 9;

        now

          per cases by A37, A39, XREAL_1: 9;

            case

             A40: 1 <= i & i <= ( len gs1);

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

            then (hs1 . i) = (gs1 . i) by FINSEQ_1:def 7;

            hence k1 <= n by A8, A24, A40;

          end;

            case

             A41: 0 < (i - ( len gs1)) & (i - ( len gs1)) <= (( len hs1) -' ( len gs1));

            then

             A42: (i - ( len gs1)) = (i -' ( len gs1)) by XREAL_0:def 2;

            then

             A43: ( 0 + 1) <= (i -' ( len gs1)) by A41, NAT_1: 13;

            then (i -' ( len gs1)) in ( Seg (( len hs1) -' ( len gs1))) by A41, A42, FINSEQ_1: 1;

            then

             A44: (i -' ( len gs1)) in ( Seg (( len gs2) -' 1)) by A38, NAT_D: 34;

            then

             A45: (i -' ( len gs1)) <= (( len gs2) -' 1) by FINSEQ_1: 1;

            

             A46: i = (( len gs1) + (i - ( len gs1)));

            (i -' ( len gs1)) in ( Seg ( len ((( len gs2) -' 1) |-> i2))) by A44, CARD_1:def 7;

            then

             A47: (i -' ( len gs1)) in ( dom ((( len gs2) -' 1) |-> i2)) by FINSEQ_1:def 3;

            (i -' ( len gs1)) = (i - ( len gs1)) by A41, XREAL_0:def 2;

            

            then (hs1 . i) = (((( len gs2) -' 1) |-> i2) . (i -' ( len gs1))) by A47, A46, FINSEQ_1:def 7

            .= i2 by A43, A45, Lm1;

            hence k1 <= n by A3, A24;

          end;

        end;

        hence thesis by A27;

      end;

      

       A48: for i st 1 <= i & i < ( len hs1) holds ((hs1 /. i),(hs2 /. i),(hs1 /. (i + 1)),(hs2 /. (i + 1))) are_adjacent

      proof

        let i;

        assume that

         A49: 1 <= i and

         A50: i < ( len hs1);

        now

          per cases ;

            case

             A51: i < ( len gs1);

            then

             A52: (i + 1) <= ( len gs1) by NAT_1: 13;

             A53:

            now

              per cases ;

                case (i + 1) <= (( len gs1) -' 1);

                then (i + 1) <= (( len gs1) - 1) by XREAL_0:def 2;

                then ((i + 1) + 1) <= ((( len gs1) - 1) + 1) by XREAL_1: 6;

                then

                 A54: (i + 1) < ( len gs1) by NAT_1: 13;

                then

                 A55: i < ( len gs1) by NAT_1: 13;

                then

                 A56: i in ( dom gs1) by A49, FINSEQ_3: 25;

                1 < (i + 1) by A49, NAT_1: 13;

                then

                 A57: (i + 1) in ( dom gs1) by A54, FINSEQ_3: 25;

                

                 A58: ( dom gs1) c= ( dom hs1) by FINSEQ_1: 26;

                

                then

                 A59: (hs1 /. (i + 1)) = (hs1 . (i + 1)) by A57, PARTFUN1:def 6

                .= (gs1 . (i + 1)) by A57, FINSEQ_1:def 7

                .= (gs1 /. (i + 1)) by A57, PARTFUN1:def 6;

                (hs1 /. i) = (hs1 . i) by A58, A56, PARTFUN1:def 6

                .= (gs1 . i) by A56, FINSEQ_1:def 7

                .= (gs1 /. i) by A56, PARTFUN1:def 6;

                hence ((hs1 /. i),(hs1 /. (i + 1))) are_adjacent by A9, A49, A55, A59;

              end;

                case (i + 1) > (( len gs1) -' 1);

                ( 0 + 1) <= (i + 1) by NAT_1: 13;

                then

                 A60: (i + 1) in ( dom gs1) by A52, FINSEQ_3: 25;

                

                 A61: ( dom gs1) c= ( dom hs1) by FINSEQ_1: 26;

                

                then

                 A62: (hs1 /. (i + 1)) = (hs1 . (i + 1)) by A60, PARTFUN1:def 6

                .= (gs1 . (i + 1)) by A60, FINSEQ_1:def 7

                .= (gs1 /. (i + 1)) by A60, PARTFUN1:def 6;

                

                 A63: i in ( dom gs1) by A49, A51, FINSEQ_3: 25;

                

                then (hs1 /. i) = (hs1 . i) by A61, PARTFUN1:def 6

                .= (gs1 . i) by A63, FINSEQ_1:def 7

                .= (gs1 /. i) by A63, PARTFUN1:def 6;

                hence ((hs1 /. i),(hs1 /. (i + 1))) are_adjacent by A9, A49, A51, A62;

              end;

            end;

            

             A64: 1 <= (i + 1) by A49, NAT_1: 13;

             A65:

            now

              per cases ;

                case

                 A66: (i + 1) <= (( len gs1) -' 1);

                

                 A67: ( len ((( len gs1) -' 1) |-> j1)) = (( len gs1) -' 1) by CARD_1:def 7;

                

                 A68: ( dom ((( len gs1) -' 1) |-> j1)) c= ( dom hs2) by FINSEQ_1: 26;

                (i + 1) in ( Seg (( len gs1) -' 1)) by A64, A66, FINSEQ_1: 1;

                then

                 A69: (i + 1) in ( dom ((( len gs1) -' 1) |-> j1)) by A67, FINSEQ_1:def 3;

                

                then (hs2 . (i + 1)) = (((( len gs1) -' 1) |-> j1) . (i + 1)) by FINSEQ_1:def 7

                .= j1 by A64, A66, Lm1;

                hence (hs2 /. (i + 1)) = j1 by A69, A68, PARTFUN1:def 6;

              end;

                case

                 A70: (i + 1) > (( len gs1) -' 1);

                

                 A71: ((( len gs1) -' 1) + 1) = ((( len gs1) - 1) + 1) by A7, XREAL_0:def 2

                .= ( len gs1);

                ((( len gs1) -' 1) + 1) <= (i + 1) by A70, NAT_1: 13;

                then

                 A72: ( len gs1) = (i + 1) by A52, A71, XXREAL_0: 1;

                ( dom hs2) = ( Seg (( len ((( len gs1) -' 1) |-> j1)) + ( len gs2))) by FINSEQ_1:def 7;

                

                then ( len hs2) = (( len ((( len gs1) -' 1) |-> j1)) + ( len gs2)) by FINSEQ_1:def 3

                .= ((( len gs1) -' 1) + ( len gs2)) by CARD_1:def 7

                .= ((( len gs1) - 1) + ( len gs2)) by A7, XREAL_0:def 2

                .= (( len gs1) + (( len gs2) - 1))

                .= (( len gs1) + (( len gs2) -' 1)) by A12, XREAL_0:def 2;

                then ( len gs1) <= ( len hs2) by NAT_1: 11;

                then ( len gs1) in ( Seg ( len hs2)) by A18, FINSEQ_1: 1;

                then

                 A73: (i + 1) in ( dom hs2) by A72, FINSEQ_1:def 3;

                1 in ( Seg ( len gs2)) by A15, FINSEQ_1: 1;

                then

                 A74: 1 in ( dom gs2) by FINSEQ_1:def 3;

                (( len ((( len gs1) -' 1) |-> j1)) + 1) = (i + 1) by A71, A72, CARD_1:def 7;

                then (hs2 . (i + 1)) = j1 by A10, A74, FINSEQ_1:def 7;

                hence (hs2 /. (i + 1)) = j1 by A73, PARTFUN1:def 6;

              end;

            end;

            

             A75: ( len ((( len gs1) -' 1) |-> j1)) = (( len gs1) -' 1) by CARD_1:def 7;

            

             A76: ( dom ((( len gs1) -' 1) |-> j1)) c= ( dom hs2) by FINSEQ_1: 26;

            ((i + 1) - 1) <= (( len gs1) - 1) by A52, XREAL_1: 9;

            then

             A77: i <= (( len gs1) -' 1) by XREAL_0:def 2;

            then i in ( Seg (( len gs1) -' 1)) by A49, FINSEQ_1: 1;

            then

             A78: i in ( dom ((( len gs1) -' 1) |-> j1)) by A75, FINSEQ_1:def 3;

            

            then (hs2 . i) = (((( len gs1) -' 1) |-> j1) . i) by FINSEQ_1:def 7

            .= j1 by A49, A77, Lm1;

            hence ((hs1 /. i),(hs1 /. (i + 1))) are_adjacent & (hs2 /. i) = (hs2 /. (i + 1)) or (hs1 /. i) = (hs1 /. (i + 1)) & ((hs2 /. i),(hs2 /. (i + 1))) are_adjacent by A78, A76, A65, A53, PARTFUN1:def 6;

          end;

            case

             A79: i >= ( len gs1);

            then

             A80: 0 <= ((i + 1) - ( len gs1)) by NAT_1: 12, XREAL_1: 48;

            

             A81: (( len ((( len gs1) -' 1) |-> j1)) + (((i + 1) -' ( len gs1)) + 1)) = ((( len gs1) -' 1) + (((i + 1) -' ( len gs1)) + 1)) by CARD_1:def 7

            .= ((( len gs1) - 1) + (((i + 1) -' ( len gs1)) + 1)) by A19, XREAL_0:def 2

            .= ((( len gs1) - 1) + (((i + 1) - ( len gs1)) + 1)) by A80, XREAL_0:def 2

            .= (i + 1);

            

             A82: (i + 1) = (( len gs1) + ((i + 1) - ( len gs1)))

            .= (( len gs1) + ((i + 1) -' ( len gs1))) by A80, XREAL_0:def 2;

            

             A83: (i - ( len gs1)) >= 0 by A79, XREAL_1: 48;

            then ( 0 + 1) <= ((i - ( len gs1)) + 1) by XREAL_1: 6;

            then

             A84: 1 <= ((i + 1) -' ( len gs1)) by A80, XREAL_0:def 2;

            

             A85: (i - ( len gs1)) = (i -' ( len gs1)) by A83, XREAL_0:def 2;

             A86:

            now

              assume not 1 <= (i -' ( len gs1));

              then (i -' ( len gs1)) < ( 0 + 1);

              then

               A87: (i -' ( len gs1)) = 0 by NAT_1: 13;

              ( len gs1) in ( Seg ( len gs1)) by A7, FINSEQ_1: 3;

              then i in ( dom gs1) by A85, A87, FINSEQ_1:def 3;

              hence (hs1 . i) = i2 by A6, A85, A87, FINSEQ_1:def 7;

            end;

            

             A88: (((i + 1) - ( len gs1)) + ( len gs1)) <= ((( len gs2) - 1) + ( len gs1)) by A17, A50, NAT_1: 13;

            then ((i + 1) - ( len gs1)) <= (( len gs2) - 1) by XREAL_1: 6;

            then ((i + 1) - ( len gs1)) <= (( len gs2) -' 1) by XREAL_0:def 2;

            then

             A89: ((i + 1) -' ( len gs1)) <= (( len gs2) -' 1) by XREAL_0:def 2;

            ((i - ( len gs1)) + 1) >= ( 0 + 1) by A83, XREAL_1: 6;

            then

             A90: 1 <= ((i + 1) -' ( len gs1)) by A88, XREAL_0:def 2;

            ( len ((( len gs2) -' 1) |-> i2)) = (( len gs2) -' 1) by CARD_1:def 7;

            then ((i + 1) -' ( len gs1)) in ( Seg ( len ((( len gs2) -' 1) |-> i2))) by A90, A89, FINSEQ_1: 1;

            then ((i + 1) -' ( len gs1)) in ( dom ((( len gs2) -' 1) |-> i2)) by FINSEQ_1:def 3;

            

            then

             A91: (hs1 . (i + 1)) = (((( len gs2) -' 1) |-> i2) . ((i + 1) -' ( len gs1))) by A82, FINSEQ_1:def 7

            .= i2 by A90, A89, Lm1;

            

             A92: (( len ((( len gs1) -' 1) |-> j1)) + ((i + 1) -' ( len gs1))) = ((( len gs1) -' 1) + ((i + 1) -' ( len gs1))) by CARD_1:def 7

            .= ((( len gs1) - 1) + ((i + 1) -' ( len gs1))) by A19, XREAL_0:def 2

            .= ((( len gs1) - 1) + ((i - ( len gs1)) + 1)) by A80, XREAL_0:def 2

            .= i;

            ( len hs1) = (( len gs1) + ( len ((( len gs2) -' 1) |-> i2))) by FINSEQ_1: 22

            .= (( len gs1) + (( len gs2) -' 1)) by CARD_1:def 7;

            then (i - ( len gs1)) < ((( len gs1) + (( len gs2) -' 1)) - ( len gs1)) by A50, XREAL_1: 9;

            then

             A93: (i -' ( len gs1)) <= (( len gs2) -' 1) by XREAL_0:def 2;

            (i - (( len gs1) - 1)) < (((( len gs1) - 1) + ( len gs2)) - (( len gs1) - 1)) by A17, A50, XREAL_1: 9;

            then

             A94: ((i + 1) -' ( len gs1)) < ( len gs2) by A80, XREAL_0:def 2;

            then 1 <= (((i + 1) -' ( len gs1)) + 1) & ( len gs2) >= (((i + 1) -' ( len gs1)) + 1) by NAT_1: 11, NAT_1: 13;

            then (((i + 1) -' ( len gs1)) + 1) in ( Seg ( len gs2)) by FINSEQ_1: 1;

            then

             A95: (((i + 1) -' ( len gs1)) + 1) in ( dom gs2) by FINSEQ_1:def 3;

            (( len gs2) -' 1) <= ((( len gs2) -' 1) + 1) by NAT_1: 11;

            then ((i + 1) -' ( len gs1)) <= ((( len gs2) -' 1) + 1) by A89, XXREAL_0: 2;

            then ((i + 1) -' ( len gs1)) <= ((( len gs2) - 1) + 1) by A16, XREAL_0:def 2;

            then

             A96: ((i + 1) -' ( len gs1)) in ( dom gs2) by A90, FINSEQ_3: 25;

            

             A97: ( len ((( len gs2) -' 1) |-> i2)) = (( len gs2) -' 1) by CARD_1:def 7;

             A98:

            now

              

               A99: i = (( len gs1) + (i - ( len gs1)))

              .= (( len gs1) + (i -' ( len gs1))) by A83, XREAL_0:def 2;

              assume

               A100: 1 <= (i -' ( len gs1));

              then (i -' ( len gs1)) in ( Seg ( len ((( len gs2) -' 1) |-> i2))) by A93, A97, FINSEQ_1: 1;

              then (i -' ( len gs1)) in ( dom ((( len gs2) -' 1) |-> i2)) by FINSEQ_1:def 3;

              

              then (hs1 . i) = (((( len gs2) -' 1) |-> i2) . (i -' ( len gs1))) by A99, FINSEQ_1:def 7

              .= i2 by A93, A100, Lm1;

              hence (hs1 . i) = i2;

            end;

            i in ( dom hs2) by A17, A20, A49, A50, FINSEQ_3: 25;

            

            then

             A101: (hs2 /. i) = (hs2 . (( len ((( len gs1) -' 1) |-> j1)) + ((i + 1) -' ( len gs1)))) by A92, PARTFUN1:def 6

            .= (gs2 . ((i + 1) -' ( len gs1))) by A96, FINSEQ_1:def 7

            .= (gs2 /. ((i + 1) -' ( len gs1))) by A96, PARTFUN1:def 6;

            i in ( dom hs1) by A49, A50, FINSEQ_3: 25;

            then

             A102: (hs1 /. i) = i2 by A86, A98, PARTFUN1:def 6;

            (i + 1) <= ( len hs1) & ( 0 + 1) <= (i + 1) by A50, NAT_1: 13;

            then

             A103: (i + 1) in ( Seg ( len hs1)) by FINSEQ_1: 1;

            then (i + 1) in ( dom hs2) by A17, A20, FINSEQ_1:def 3;

            

            then

             A104: (hs2 /. (i + 1)) = (hs2 . (( len ((( len gs1) -' 1) |-> j1)) + (((i + 1) -' ( len gs1)) + 1))) by A81, PARTFUN1:def 6

            .= (gs2 . (((i + 1) -' ( len gs1)) + 1)) by A95, FINSEQ_1:def 7

            .= (gs2 /. (((i + 1) -' ( len gs1)) + 1)) by A95, PARTFUN1:def 6;

            (i + 1) in ( dom hs1) by A103, FINSEQ_1:def 3;

            hence ((hs1 /. i),(hs1 /. (i + 1))) are_adjacent & (hs2 /. i) = (hs2 /. (i + 1)) or (hs1 /. i) = (hs1 /. (i + 1)) & ((hs2 /. i),(hs2 /. (i + 1))) are_adjacent by A14, A102, A91, A84, A94, A104, A101, PARTFUN1:def 6;

          end;

        end;

        hence thesis;

      end;

       A105:

      now

        per cases ;

          case (( len gs1) -' 1) = 0 ;

          

          then (((( len gs1) -' 1) |-> j1) ^ gs2) = (( <*> NAT ) ^ gs2)

          .= gs2 by FINSEQ_1: 34;

          hence (hs2 . 1) = j1 & (hs2 . ( len hs2)) = j2 by A10, A11;

        end;

          case

           A106: (( len gs1) -' 1) <> 0 ;

          ( len ((( len gs1) -' 1) |-> j1)) = (( len gs1) -' 1) by CARD_1:def 7;

          then

           A107: ( 0 + 1) <= ( len ((( len gs1) -' 1) |-> j1)) by A106, NAT_1: 13;

          then 1 in ( dom ((( len gs1) -' 1) |-> j1)) by FINSEQ_3: 25;

          then

           A108: (hs2 . 1) = (((( len gs1) -' 1) |-> j1) . 1) by FINSEQ_1:def 7;

          1 <= ( len gs2) by A12, NAT_1: 11;

          then

           A109: ( len gs2) in ( dom gs2) by FINSEQ_3: 25;

          ( len ((( len gs1) -' 1) |-> j1)) = (( len gs1) -' 1) & ( len hs2) = (( len ((( len gs1) -' 1) |-> j1)) + ( len gs2)) by CARD_1:def 7, FINSEQ_1: 22;

          hence (hs2 . 1) = j1 & (hs2 . ( len hs2)) = j2 by A11, A107, A108, A109, Lm1, FINSEQ_1:def 7;

        end;

      end;

      

       A110: 1 in ( dom gs1) by A18, FINSEQ_3: 25;

      now

        per cases ;

          case (( len gs2) -' 1) = 0 ;

          

          then (gs1 ^ ((( len gs2) -' 1) |-> i2)) = (gs1 ^ ( <*> NAT ))

          .= gs1 by FINSEQ_1: 34;

          hence (hs1 . 1) = i1 & (hs1 . ( len hs1)) = i2 by A5, A6;

        end;

          case (( len gs2) -' 1) <> 0 ;

          then

           A111: ( 0 + 1) <= (( len gs2) -' 1) by NAT_1: 13;

          

           A112: ( len hs1) = (( len gs1) + ( len ((( len gs2) -' 1) |-> i2))) by FINSEQ_1: 22;

          ( len ((( len gs2) -' 1) |-> i2)) = (( len gs2) -' 1) by CARD_1:def 7;

          then ( len ((( len gs2) -' 1) |-> i2)) in ( dom ((( len gs2) -' 1) |-> i2)) & (((( len gs2) -' 1) |-> i2) . ( len ((( len gs2) -' 1) |-> i2))) = i2 by A111, Lm1, FINSEQ_3: 25;

          hence (hs1 . 1) = i1 & (hs1 . ( len hs1)) = i2 by A5, A110, A112, FINSEQ_1:def 7;

        end;

      end;

      hence thesis by A7, A12, A17, A20, A105, A21, A48;

    end;

    reserve S for set;

    theorem :: GOBRD10:8

    for Y be Subset of S, F be Matrix of n, m, ( bool S) st (ex i, j st i in ( Seg n) & j in ( Seg m) & (F * (i,j)) c= Y) & (for i1, j1, i2, j2 st i1 in ( Seg n) & i2 in ( Seg n) & j1 in ( Seg m) & j2 in ( Seg m) & (i1,j1,i2,j2) are_adjacent holds (F * (i1,j1)) c= Y iff (F * (i2,j2)) c= Y) holds for i, j st i in ( Seg n) & j in ( Seg m) holds (F * (i,j)) c= Y

    proof

      let Y be Subset of S, F be Matrix of n, m, ( bool S);

      assume that

       A1: ex i, j st i in ( Seg n) & j in ( Seg m) & (F * (i,j)) c= Y and

       A2: for i1, j1, i2, j2 st i1 in ( Seg n) & i2 in ( Seg n) & j1 in ( Seg m) & j2 in ( Seg m) & (i1,j1,i2,j2) are_adjacent holds (F * (i1,j1)) c= Y iff (F * (i2,j2)) c= Y;

      consider i1, j1 such that

       A3: i1 in ( Seg n) and

       A4: j1 in ( Seg m) and

       A5: (F * (i1,j1)) c= Y by A1;

      

       A6: j1 <= m by A4, FINSEQ_1: 1;

      1 <= i1 by A3, FINSEQ_1: 1;

      then (i1 - 1) >= (1 - 1) by XREAL_1: 9;

      then

       A7: (i1 -' 1) = (i1 - 1) by XREAL_0:def 2;

      1 <= j1 by A4, FINSEQ_1: 1;

      then (j1 - 1) >= (1 - 1) by XREAL_1: 9;

      then

       A8: (j1 -' 1) = (j1 - 1) by XREAL_0:def 2;

      

       A9: i1 <= n by A3, FINSEQ_1: 1;

      thus for i, j st i in ( Seg n) & j in ( Seg m) holds (F * (i,j)) c= Y

      proof

        let i2, j2;

        assume that

         A10: i2 in ( Seg n) and

         A11: j2 in ( Seg m);

        

         A12: j2 <= m by A11, FINSEQ_1: 1;

        1 <= i2 by A10, FINSEQ_1: 1;

        then (i2 - 1) >= (1 - 1) by XREAL_1: 9;

        then

         A13: (i2 -' 1) = (i2 - 1) by XREAL_0:def 2;

        1 <= j2 by A11, FINSEQ_1: 1;

        then (j2 - 1) >= (1 - 1) by XREAL_1: 9;

        then

         A14: (j2 -' 1) = (j2 - 1) by XREAL_0:def 2;

        

         A15: i2 <= n by A10, FINSEQ_1: 1;

        now

          per cases ;

            case n = 0 or m = 0 ;

            hence contradiction by A3, A4;

          end;

            case

             A16: n <> 0 & m <> 0 ;

            then m >= ( 0 + 1) by NAT_1: 13;

            then (m - 1) >= 0 by XREAL_1: 19;

            then

             A17: (m -' 1) = (m - 1) by XREAL_0:def 2;

            then

             A18: (j1 -' 1) <= (m -' 1) & (j2 -' 1) <= (m -' 1) by A6, A8, A12, A14, XREAL_1: 9;

            n >= ( 0 + 1) by A16, NAT_1: 13;

            then (n - 1) >= 0 by XREAL_1: 19;

            then

             A19: (n -' 1) = (n - 1) by XREAL_0:def 2;

            then (i1 -' 1) <= (n -' 1) & (i2 -' 1) <= (n -' 1) by A9, A7, A15, A13, XREAL_1: 9;

            then

            consider fs1,fs2 be FinSequence of NAT such that

             A20: for i, k1, k2 st i in ( dom fs1) & k1 = (fs1 . i) & k2 = (fs2 . i) holds k1 <= (n -' 1) & k2 <= (m -' 1) and

             A21: (fs1 . 1) = (i1 -' 1) and

             A22: (fs1 . ( len fs1)) = (i2 -' 1) and

             A23: (fs2 . 1) = (j1 -' 1) and

             A24: (fs2 . ( len fs2)) = (j2 -' 1) and

             A25: ( len fs1) = ( len fs2) and

             A26: ( len fs1) = ((((((i1 -' 1) -' (i2 -' 1)) + ((i2 -' 1) -' (i1 -' 1))) + ((j1 -' 1) -' (j2 -' 1))) + ((j2 -' 1) -' (j1 -' 1))) + 1) and

             A27: for i st 1 <= i & i < ( len fs1) holds ((fs1 /. i),(fs2 /. i),(fs1 /. (i + 1)),(fs2 /. (i + 1))) are_adjacent by A18, Th7;

            deffunc F( Nat) = ((fs1 /. $1) + 1);

            ex p be FinSequence of NAT st ( len p) = ( len fs1) & for j be Nat st j in ( dom p) holds (p . j) = F(j) from FINSEQ_2:sch 1;

            then

            consider p1 be FinSequence of NAT such that

             A28: ( len p1) = ( len fs1) and

             A29: for k be Nat st k in ( dom p1) holds (p1 . k) = ((fs1 /. k) + 1);

            deffunc F( Nat) = ((fs2 /. $1) + 1);

            ex p be FinSequence of NAT st ( len p) = ( len fs2) & for k be Nat st k in ( dom p) holds (p . k) = F(k) from FINSEQ_2:sch 1;

            then

            consider p2 be FinSequence of NAT such that

             A30: ( len p2) = ( len fs2) and

             A31: for k be Nat st k in ( dom p2) holds (p2 . k) = ((fs2 /. k) + 1);

            

             A32: ( dom p2) = ( Seg ( len fs2)) by A30, FINSEQ_1:def 3;

            defpred P[ Nat] means ($1 + 1) <= ( len p1) implies (F * ((p1 /. ($1 + 1)),(p2 /. ($1 + 1)))) c= Y;

            

             A33: ( dom p1) = ( Seg ( len fs1)) by A28, FINSEQ_1:def 3;

            

             A34: for k be Nat st P[k] holds P[(k + 1)]

            proof

              let k be Nat;

              

               A35: 1 <= (k + 1) by NAT_1: 12;

              assume

               A36: (k + 1) <= ( len p1) implies (F * ((p1 /. (k + 1)),(p2 /. (k + 1)))) c= Y;

              now

                per cases ;

                  case

                   A37: (k + 1) <= ( len p1);

                  now

                    per cases ;

                      case

                       A38: ((k + 1) + 1) <= ( len p1);

                      set lp11 = (fs1 /. ((k + 1) + 1)), lp21 = (fs2 /. ((k + 1) + 1));

                      1 <= ((k + 1) + 1) by NAT_1: 12;

                      then

                       A39: ((k + 1) + 1) in ( Seg ( len p1)) by A38, FINSEQ_1: 1;

                      then ((k + 1) + 1) in ( dom fs2) by A25, A28, FINSEQ_1:def 3;

                      then

                       A40: (fs2 /. ((k + 1) + 1)) = (fs2 . ((k + 1) + 1)) by PARTFUN1:def 6;

                      

                       A41: ((k + 1) + 1) in ( dom fs1) by A28, A39, FINSEQ_1:def 3;

                      then

                       A42: (fs1 /. ((k + 1) + 1)) = (fs1 . ((k + 1) + 1)) by PARTFUN1:def 6;

                      then lp11 <= (n - 1) by A19, A20, A41, A40;

                      then

                       A43: (lp11 + 1) <= ((n - 1) + 1) by XREAL_1: 6;

                      ((k + 1) + 1) in ( dom p2) by A25, A28, A30, A39, FINSEQ_1:def 3;

                      then (p2 . ((k + 1) + 1)) = (p2 /. ((k + 1) + 1)) by PARTFUN1:def 6;

                      then

                       A44: (p2 /. ((k + 1) + 1)) = (lp21 + 1) by A25, A28, A31, A32, A39;

                      lp21 <= (m -' 1) by A20, A41, A42, A40;

                      then

                       A45: (lp21 + 1) <= ((m - 1) + 1) by A17, XREAL_1: 6;

                      1 <= (1 + lp21) by NAT_1: 11;

                      then

                       A46: (p2 /. ((k + 1) + 1)) in ( Seg m) by A44, A45, FINSEQ_1: 1;

                      ((k + 1) + 1) in ( dom p1) by A39, FINSEQ_1:def 3;

                      

                      then

                       A47: (p1 /. ((k + 1) + 1)) = (p1 . ((k + 1) + 1)) by PARTFUN1:def 6

                      .= (lp11 + 1) by A28, A29, A33, A39;

                      set lp1 = (fs1 /. (k + 1)), lp2 = (fs2 /. (k + 1));

                      

                       A48: (k + 1) < ( len p1) by A38, NAT_1: 13;

                      then

                       A49: (k + 1) in ( Seg ( len p1)) by A35, FINSEQ_1: 1;

                      then (k + 1) in ( dom fs2) by A25, A28, FINSEQ_1:def 3;

                      then

                       A50: lp2 = (fs2 . (k + 1)) by PARTFUN1:def 6;

                      (k + 1) in ( dom p1) by A49, FINSEQ_1:def 3;

                      

                      then

                       A51: (p1 /. (k + 1)) = (p1 . (k + 1)) by PARTFUN1:def 6

                      .= (lp1 + 1) by A28, A29, A33, A49;

                      

                       A52: (k + 1) in ( dom fs1) by A28, A49, FINSEQ_1:def 3;

                      then

                       A53: lp1 = (fs1 . (k + 1)) by PARTFUN1:def 6;

                      then lp1 <= (n - 1) by A19, A20, A52, A50;

                      then

                       A54: (lp1 + 1) <= ((n - 1) + 1) by XREAL_1: 6;

                      1 <= (1 + lp1) by NAT_1: 11;

                      then

                       A55: (p1 /. (k + 1)) in ( Seg n) by A51, A54, FINSEQ_1: 1;

                      (k + 1) in ( dom p2) by A25, A28, A30, A49, FINSEQ_1:def 3;

                      

                      then

                       A56: (p2 /. (k + 1)) = (p2 . (k + 1)) by PARTFUN1:def 6

                      .= (lp2 + 1) by A25, A28, A31, A32, A49;

                      lp2 <= (m -' 1) by A20, A52, A53, A50;

                      then

                       A57: (lp2 + 1) <= ((m - 1) + 1) by A17, XREAL_1: 6;

                      1 <= (1 + lp2) by NAT_1: 11;

                      then

                       A58: (p2 /. (k + 1)) in ( Seg m) by A56, A57, FINSEQ_1: 1;

                      1 <= (1 + lp11) by NAT_1: 11;

                      then

                       A59: (p1 /. ((k + 1) + 1)) in ( Seg n) by A47, A43, FINSEQ_1: 1;

                      ((k + 1) + 1) in ( dom p2) by A25, A28, A30, A39, FINSEQ_1:def 3;

                      

                      then (p2 /. ((k + 1) + 1)) = (p2 . ((k + 1) + 1)) by PARTFUN1:def 6

                      .= (lp21 + 1) by A25, A28, A31, A32, A39;

                      then ((p1 /. (k + 1)),(p2 /. (k + 1)),(p1 /. ((k + 1) + 1)),(p2 /. ((k + 1) + 1))) are_adjacent by A27, A28, A35, A48, A51, A56, A47, Th3;

                      hence thesis by A2, A36, A37, A55, A58, A59, A46;

                    end;

                      case ((k + 1) + 1) > ( len p1);

                      hence thesis;

                    end;

                  end;

                  hence thesis;

                end;

                  case (k + 1) > ( len p1);

                  hence thesis by NAT_1: 13;

                end;

              end;

              hence thesis;

            end;

            

             A60: 1 <= ( len fs1) by A26, NAT_1: 11;

            then

             A61: 1 in ( Seg ( len fs1)) by FINSEQ_1: 1;

            then 1 in ( dom fs2) by A25, FINSEQ_1:def 3;

            then

             A62: (fs2 /. 1) = (j1 -' 1) by A23, PARTFUN1:def 6;

            1 in ( dom p2) by A25, A30, A61, FINSEQ_1:def 3;

            

            then

             A63: (p2 /. 1) = (p2 . 1) by PARTFUN1:def 6

            .= ((j1 -' 1) + 1) by A25, A31, A32, A61, A62

            .= j1 by A8;

            1 in ( dom fs1) by A61, FINSEQ_1:def 3;

            then

             A64: (fs1 /. 1) = (i1 -' 1) by A21, PARTFUN1:def 6;

            1 in ( dom p1) by A28, A61, FINSEQ_1:def 3;

            

            then (p1 /. 1) = (p1 . 1) by PARTFUN1:def 6

            .= ((i1 -' 1) + 1) by A29, A33, A61, A64

            .= i1 by A7;

            then

             A65: P[ 0 ] by A5, A63;

            

             A66: for i be Nat holds P[i] from NAT_1:sch 2( A65, A34);

            (1 - 1) <= (( len fs1) - 1) by A60, XREAL_1: 9;

            then (( len fs1) -' 1) = (( len fs1) - 1) by XREAL_0:def 2;

            then

             A67: ((( len fs1) -' 1) + 1) = ( len fs1);

            

             A68: ( len fs1) in ( Seg ( len fs1)) by A60, FINSEQ_1: 1;

            then ( len fs1) in ( dom fs2) by A25, FINSEQ_1:def 3;

            then

             A69: (fs2 /. ( len fs1)) = (j2 -' 1) by A24, A25, PARTFUN1:def 6;

            ( len fs1) in ( dom p1) by A28, A68, FINSEQ_1:def 3;

            

            then

             A70: (p1 /. ( len fs1)) = (p1 . ( len fs1)) by PARTFUN1:def 6

            .= ((fs1 /. ( len fs1)) + 1) by A29, A33, A68;

            ( len fs1) in ( dom fs1) by A68, FINSEQ_1:def 3;

            then

             A71: (fs1 /. ( len fs1)) = (i2 -' 1) by A22, PARTFUN1:def 6;

            ( len fs1) in ( dom p2) by A25, A30, A68, FINSEQ_1:def 3;

            

            then (p2 /. ( len fs1)) = (p2 . ( len fs1)) by PARTFUN1:def 6

            .= ((fs2 /. ( len fs1)) + 1) by A25, A31, A32, A68;

            hence thesis by A13, A14, A28, A66, A67, A70, A71, A69;

          end;

        end;

        hence thesis;

      end;

    end;