:: GOBRD10 semantic presentation

begin


definition
let i1, i2 be Element of NAT ;
predi1,i2 are_adjacent1  means :Def1: :: GOBRD10:def 1
( i2 = i1 + 1 or i1 = i2 + 1 );
symmetry
 for i1, i2 being Element of NAT holds
( ( not i2 = i1 + 1 & not i1 = i2 + 1 ) or i1 = i2 + 1 or i2 = i1 + 1 ) ;
irreflexivity
 for i1 being Element of NAT holds
( not i1 = i1 + 1 & not i1 = i1 + 1 ) ;
end;

:: deftheorem Def1 defines are_adjacent1 GOBRD10:def_1_:_
 for i1, i2 being Element of NAT holds
( i1,i2 are_adjacent1 iff ( i2 = i1 + 1 or i1 = i2 + 1 ) );

theorem Th1: :: GOBRD10:1
for i1, i2 being Element of NAT st i1,i2 are_adjacent1 holds
i1 + 1,i2 + 1 are_adjacent1
proof
let i1, i2 be Element of NAT ; ::_thesis: ( i1,i2 are_adjacent1 implies i1 + 1,i2 + 1 are_adjacent1 )
assume  i1,i2 are_adjacent1 ; ::_thesis: i1 + 1,i2 + 1 are_adjacent1
then  ( i2 = i1 + 1 or i1 = i2 + 1 ) by Def1;
hence  i1 + 1,i2 + 1 are_adjacent1 by Def1; ::_thesis: verum
end;

theorem Th2: :: GOBRD10:2
for i1, i2 being Element of NAT st i1,i2 are_adjacent1 & 1 <= i1 & 1 <= i2 holds
i1 -' 1,i2 -' 1 are_adjacent1
proof
let i1, i2 be Element of NAT ; ::_thesis: ( i1,i2 are_adjacent1 & 1 <= i1 & 1 <= i2 implies i1 -' 1,i2 -' 1 are_adjacent1 )
assume that
A1: i1,i2 are_adjacent1 and
A2: 1 <= i1 and
A3: 1 <= i2 ; ::_thesis: i1 -' 1,i2 -' 1 are_adjacent1
 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, Def1;
then  ( i2 - 1 = (i1 - 1) + 1 or i1 - 1 = (i2 - 1) + 1 ) ;
hence  i1 -' 1,i2 -' 1 are_adjacent1 by A4, A5, Def1; ::_thesis: verum
end;

definition
let i1, j1, i2, j2 be Element of NAT ;
predi1,j1,i2,j2 are_adjacent2  means :Def2: :: GOBRD10:def 2
( ( i1,i2 are_adjacent1 & j1 = j2 ) or ( i1 = i2 & j1,j2 are_adjacent1 ) );
end;

:: deftheorem Def2 defines are_adjacent2 GOBRD10:def_2_:_
 for i1, j1, i2, j2 being Element of NAT holds
( i1,j1,i2,j2 are_adjacent2 iff ( ( i1,i2 are_adjacent1 & j1 = j2 ) or ( i1 = i2 & j1,j2 are_adjacent1 ) ) );

theorem Th3: :: GOBRD10:3
for i1, i2, j1, j2 being Element of NAT st i1,j1,i2,j2 are_adjacent2 holds
i1 + 1,j1 + 1,i2 + 1,j2 + 1 are_adjacent2
proof
let i1, i2, j1, j2 be Element of NAT ; ::_thesis: ( i1,j1,i2,j2 are_adjacent2 implies i1 + 1,j1 + 1,i2 + 1,j2 + 1 are_adjacent2 )
assume  i1,j1,i2,j2 are_adjacent2 ; ::_thesis: i1 + 1,j1 + 1,i2 + 1,j2 + 1 are_adjacent2
then  ( ( i1,i2 are_adjacent1 & j1 = j2 ) or ( i1 = i2 & j1,j2 are_adjacent1 ) ) by Def2;
then  ( ( i1 + 1,i2 + 1 are_adjacent1 & j1 + 1 = j2 + 1 ) or ( i1 + 1 = i2 + 1 & j1 + 1,j2 + 1 are_adjacent1 ) ) by Th1;
hence  i1 + 1,j1 + 1,i2 + 1,j2 + 1 are_adjacent2 by Def2; ::_thesis: verum
end;

theorem :: GOBRD10:4
for i1, i2, j1, j2 being Element of NAT st i1,j1,i2,j2 are_adjacent2 & 1 <= i1 & 1 <= i2 & 1 <= j1 & 1 <= j2 holds
i1 -' 1,j1 -' 1,i2 -' 1,j2 -' 1 are_adjacent2
proof
let i1, i2, j1, j2 be Element of NAT ; ::_thesis: ( i1,j1,i2,j2 are_adjacent2 & 1 <= i1 & 1 <= i2 & 1 <= j1 & 1 <= j2 implies i1 -' 1,j1 -' 1,i2 -' 1,j2 -' 1 are_adjacent2 )
assume that
A1: i1,j1,i2,j2 are_adjacent2 and
A2: ( 1 <= i1 & 1 <= i2 & 1 <= j1 & 1 <= j2 ) ; ::_thesis: i1 -' 1,j1 -' 1,i2 -' 1,j2 -' 1 are_adjacent2
 ( ( i1,i2 are_adjacent1 & j1 = j2 ) or ( i1 = i2 & j1,j2 are_adjacent1 ) ) by A1, Def2;
then  ( ( i1 -' 1,i2 -' 1 are_adjacent1 & j1 -' 1 = j2 -' 1 ) or ( i1 -' 1 = i2 -' 1 & j1 -' 1,j2 -' 1 are_adjacent1 ) ) by A2, Th2;
hence  i1 -' 1,j1 -' 1,i2 -' 1,j2 -' 1 are_adjacent2 by Def2; ::_thesis: verum
end;

Lm1: now__::_thesis:_for_n,_i,_j_being_Element_of_NAT_st_1_<=_j_&_j_<=_n_holds_
(n_|->_i)_._j_=_i
let n, i, j be Element of NAT ; ::_thesis: ( 1 <= j & j <= n implies (n |-> i) . j = i )
assume  ( 1 <= j & j <= n ) ; ::_thesis: (n |-> i) . j = i
then  j in Seg n by FINSEQ_1:1;
hence  (n |-> i) . j = i by FINSEQ_2:57; ::_thesis: verum
end;

theorem Th5: :: GOBRD10:5
for n, i, j being Element of NAT st i <= n & j <= n holds
ex fs1 being FinSequence of NAT st
( fs1 . 1 = i & fs1 . (len fs1) = j & len fs1 = ((i -' j) + (j -' i)) + 1 & ( for k, k1 being Element of NAT st 1 <= k & k <= len fs1 & k1 = fs1 . k holds
k1 <= n ) & ( for i1 being Element of NAT st 1 <= i1 & i1 < len fs1 & not fs1 . (i1 + 1) = (fs1 /. i1) + 1 holds
fs1 . i1 = (fs1 /. (i1 + 1)) + 1 ) )
proof
let n, i, j be Element of NAT ; ::_thesis: ( i <= n & j <= n implies ex fs1 being FinSequence of NAT st
( fs1 . 1 = i & fs1 . (len fs1) = j & len fs1 = ((i -' j) + (j -' i)) + 1 & ( for k, k1 being Element of NAT st 1 <= k & k <= len fs1 & k1 = fs1 . k holds
k1 <= n ) & ( for i1 being Element of NAT st 1 <= i1 & i1 < len fs1 & not fs1 . (i1 + 1) = (fs1 /. i1) + 1 holds
fs1 . i1 = (fs1 /. (i1 + 1)) + 1 ) ) )
assume that
A1: i <= n and
A2: j <= n ; ::_thesis: ex fs1 being FinSequence of NAT st
( fs1 . 1 = i & fs1 . (len fs1) = j & len fs1 = ((i -' j) + (j -' i)) + 1 & ( for k, k1 being Element of NAT st 1 <= k & k <= len fs1 & k1 = fs1 . k holds
k1 <= n ) & ( for i1 being Element of NAT st 1 <= i1 & i1 < len fs1 & not fs1 . (i1 + 1) = (fs1 /. i1) + 1 holds
fs1 . i1 = (fs1 /. (i1 + 1)) + 1 ) )
now__::_thesis:_(_(_i_<_j_&_ex_fs1_being_FinSequence_of_NAT_st_
(_fs1_._1_=_i_&_fs1_._(len_fs1)_=_j_&_len_fs1_=_((i_-'_j)_+_(j_-'_i))_+_1_&_(_for_k,_k1_being_Element_of_NAT_st_1_<=_k_&_k_<=_len_fs1_&_k1_=_fs1_._k_holds_
k1_<=_n_)_&_(_for_i1_being_Element_of_NAT_st_1_<=_i1_&_i1_<_len_fs1_&_not_fs1_._(i1_+_1)_=_(fs1_/._i1)_+_1_holds_
fs1_._i1_=_(fs1_/._(i1_+_1))_+_1_)_)_)_or_(_i_=_j_&_ex_fs1_being_FinSequence_of_NAT_st_
(_fs1_._1_=_i_&_fs1_._(len_fs1)_=_j_&_len_fs1_=_((i_-'_j)_+_(j_-'_i))_+_1_&_(_for_k,_k1_being_Element_of_NAT_st_1_<=_k_&_k_<=_len_fs1_&_k1_=_fs1_._k_holds_
k1_<=_n_)_&_(_for_i1_being_Element_of_NAT_st_1_<=_i1_&_i1_<_len_fs1_&_not_fs1_._(i1_+_1)_=_(fs1_/._i1)_+_1_holds_
fs1_._i1_=_(fs1_/._(i1_+_1))_+_1_)_)_)_or_(_j_<_i_&_ex_fs1_being_FinSequence_of_NAT_st_
(_fs1_._1_=_i_&_fs1_._(len_fs1)_=_j_&_len_fs1_=_((i_-'_j)_+_(j_-'_i))_+_1_&_(_for_k,_k1_being_Element_of_NAT_st_1_<=_k_&_k_<=_len_fs1_&_k1_=_fs1_._k_holds_
k1_<=_n_)_&_(_for_i1_being_Element_of_NAT_st_1_<=_i1_&_i1_<_len_fs1_&_not_fs1_._(i1_+_1)_=_(fs1_/._i1)_+_1_holds_
fs1_._i1_=_(fs1_/._(i1_+_1))_+_1_)_)_)_)
percases ( i < j or i = j or j < i ) by XXREAL_0:1;
caseA3: i < j ; ::_thesis: ex fs1 being FinSequence of NAT st
( fs1 . 1 = i & fs1 . (len fs1) = j & len fs1 = ((i -' j) + (j -' i)) + 1 & ( for k, k1 being Element of NAT st 1 <= k & k <= len fs1 & k1 = fs1 . k holds
k1 <= n ) & ( for i1 being Element of NAT st 1 <= i1 & i1 < len fs1 & not fs1 . (i1 + 1) = (fs1 /. i1) + 1 holds
fs1 . i1 = (fs1 /. (i1 + 1)) + 1 ) )
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 H1( Nat) ->  Element of NAT = (i + $1) -' 1;
 ex p being FinSequence st
( len p = (j + 1) -' i & ( for k being Nat st k in dom p holds
p . k = H1(k) ) ) from FINSEQ_1:sch_2();
then consider p being FinSequence such that
A8: len p = (j + 1) -' i and
A9: for k being 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 set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng p or x in NAT )
assume  x in rng p ; ::_thesis: x in NAT
then consider y being set  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 is Element of NAT : ( 1 <= k & k <= len p )  }  by FINSEQ_1:def_1;
then consider k being Element of NAT  such that
A15: k = y and
 1 <= k and
 k <= len p ;
 p . k = (i + k) -' 1 by A9, A13, A15;
hence  x in NAT by A14, A15; ::_thesis: verum
end;
then reconsider fs2 = p as FinSequence of NAT by FINSEQ_1:def_4;
A16: for i1 being Element of NAT st 1 <= i1 & i1 < len fs2 & not fs2 . (i1 + 1) = (fs2 /. i1) + 1 holds
fs2 . i1 = (fs2 /. (i1 + 1)) + 1
proof
let i1 be Element of NAT ; ::_thesis: ( 1 <= i1 & i1 < len fs2 & not fs2 . (i1 + 1) = (fs2 /. i1) + 1 implies fs2 . i1 = (fs2 /. (i1 + 1)) + 1 )
assume that
A17: 1 <= i1 and
A18: i1 < len fs2 ; ::_thesis: ( fs2 . (i1 + 1) = (fs2 /. i1) + 1 or fs2 . i1 = (fs2 /. (i1 + 1)) + 1 )
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  ( fs2 . (i1 + 1) = (fs2 /. i1) + 1 or fs2 . i1 = (fs2 /. (i1 + 1)) + 1 ) by A9, A20, A22, A21; ::_thesis: verum
end;
A23: for k, k1 being Element of NAT st 1 <= k & k <= len p & k1 = p . k holds
k1 <= n
proof
let k, k1 be Element of NAT ; ::_thesis: ( 1 <= k & k <= len p & k1 = p . k implies k1 <= n )
assume that
A24: 1 <= k and
A25: k <= len p and
A26: k1 = p . k ; ::_thesis: k1 <= n
 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  k1 <= n by A2, XXREAL_0:2; ::_thesis: verum
end;
 len p in dom p by A5, A8, A11, FINSEQ_3:25;
then  p . (len p) = j by A8, A9, A11, A7;
hence  ex fs1 being FinSequence of NAT st
( fs1 . 1 = i & fs1 . (len fs1) = j & len fs1 = ((i -' j) + (j -' i)) + 1 & ( for k, k1 being Element of NAT st 1 <= k & k <= len fs1 & k1 = fs1 . k holds
k1 <= n ) & ( for i1 being Element of NAT st 1 <= i1 & i1 < len fs1 & not fs1 . (i1 + 1) = (fs1 /. i1) + 1 holds
fs1 . i1 = (fs1 /. (i1 + 1)) + 1 ) ) by A23, A12, A10, A16; ::_thesis: verum
end;
caseA29: i = j ; ::_thesis: ex fs1 being FinSequence of NAT st
( fs1 . 1 = i & fs1 . (len fs1) = j & len fs1 = ((i -' j) + (j -' i)) + 1 & ( for k, k1 being Element of NAT st 1 <= k & k <= len fs1 & k1 = fs1 . k holds
k1 <= n ) & ( for i1 being Element of NAT st 1 <= i1 & i1 < len fs1 & not fs1 . (i1 + 1) = (fs1 /. i1) + 1 holds
fs1 . i1 = (fs1 /. (i1 + 1)) + 1 ) )
then  i - j = 0 ;
then A30: i -' j = 0 by XREAL_0:def_2;
consider f being 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 being Element of NAT st 1 <= i1 & i1 < len fs1 & not fs1 . (i1 + 1) = (fs1 /. i1) + 1 holds
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 being Element of NAT st 1 <= k & k <= len fs1 & k1 = fs1 . k holds
k1 <= n by A1, A34, XXREAL_0:1;
hence  ex fs1 being FinSequence of NAT st
( fs1 . 1 = i & fs1 . (len fs1) = j & len fs1 = ((i -' j) + (j -' i)) + 1 & ( for k, k1 being Element of NAT st 1 <= k & k <= len fs1 & k1 = fs1 . k holds
k1 <= n ) & ( for i1 being Element of NAT st 1 <= i1 & i1 < len fs1 & not fs1 . (i1 + 1) = (fs1 /. i1) + 1 holds
fs1 . i1 = (fs1 /. (i1 + 1)) + 1 ) ) by A29, A34, A35, A30, A33; ::_thesis: verum
end;
caseA36: j < i ; ::_thesis: ex fs1 being FinSequence of NAT st
( fs1 . 1 = i & fs1 . (len fs1) = j & len fs1 = ((i -' j) + (j -' i)) + 1 & ( for k, k1 being Element of NAT st 1 <= k & k <= len fs1 & k1 = fs1 . k holds
k1 <= n ) & ( for i1 being Element of NAT st 1 <= i1 & i1 < len fs1 & not fs1 . (i1 + 1) = (fs1 /. i1) + 1 holds
fs1 . i1 = (fs1 /. (i1 + 1)) + 1 ) )
then A37: i - j >= j - j by XREAL_1:9;
A38: now__::_thesis:_(_(_i_-_j_=_0_&_j_-'_i_=_0_)_or_(_i_-_j_>_0_&_j_-'_i_=_0_)_)
percases ( i - j = 0 or i - j > 0 ) by A37;
case i - j = 0 ; ::_thesis: j -' i = 0
hence  j -' i = 0 by XREAL_0:def_2; ::_thesis: verum
end;
case i - j > 0 ; ::_thesis: j -' i = 0
then  - (- (i - j)) > 0 ;
then  j - i < 0 ;
hence  j -' i = 0 by XREAL_0:def_2; ::_thesis: verum
end;
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 H1( Nat) ->  Element of 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 being FinSequence st
( len p = (i + 1) -' j & ( for k being Nat st k in dom p holds
p . k = H1(k) ) ) from FINSEQ_1:sch_2();
then consider p being FinSequence such that
A43: len p = (i + 1) -' j and
A44: for k being 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 set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng p or x in NAT )
assume  x in rng p ; ::_thesis: x in NAT
then consider y being set  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 is Element of NAT : ( 1 <= k & k <= len p )  }  by FINSEQ_1:def_1;
then consider k being Element of 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  x in NAT by A48, A49; ::_thesis: verum
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 being Element of NAT st 1 <= i1 & i1 < len fs2 & not fs2 . (i1 + 1) = (fs2 /. i1) + 1 holds
fs2 . i1 = (fs2 /. (i1 + 1)) + 1
proof
let i1 be Element of NAT ; ::_thesis: ( 1 <= i1 & i1 < len fs2 & not fs2 . (i1 + 1) = (fs2 /. i1) + 1 implies fs2 . i1 = (fs2 /. (i1 + 1)) + 1 )
assume that
A53: 1 <= i1 and
A54: i1 < len fs2 ; ::_thesis: ( fs2 . (i1 + 1) = (fs2 /. i1) + 1 or fs2 . i1 = (fs2 /. (i1 + 1)) + 1 )
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  ( fs2 . (i1 + 1) = (fs2 /. i1) + 1 or fs2 . i1 = (fs2 /. (i1 + 1)) + 1 ) by A58, A56, XREAL_0:def_2; ::_thesis: verum
end;
A59: for k, k1 being Element of NAT st 1 <= k & k <= len p & k1 = p . k holds
k1 <= n
proof
let k, k1 be Element of NAT ; ::_thesis: ( 1 <= k & k <= len p & k1 = p . k implies k1 <= n )
assume that
A60: 1 <= k and
A61: k <= len p and
A62: k1 = p . k ; ::_thesis: k1 <= n
 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  k1 <= n by A1, A64, XXREAL_0:2; ::_thesis: verum
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  ex fs1 being FinSequence of NAT st
( fs1 . 1 = i & fs1 . (len fs1) = j & len fs1 = ((i -' j) + (j -' i)) + 1 & ( for k, k1 being Element of NAT st 1 <= k & k <= len fs1 & k1 = fs1 . k holds
k1 <= n ) & ( for i1 being Element of NAT st 1 <= i1 & i1 < len fs1 & not fs1 . (i1 + 1) = (fs1 /. i1) + 1 holds
fs1 . i1 = (fs1 /. (i1 + 1)) + 1 ) ) by A43, A59, A45, A46, A39, A52; ::_thesis: verum
end;
end;
end;
hence  ex fs1 being FinSequence of NAT st
( fs1 . 1 = i & fs1 . (len fs1) = j & len fs1 = ((i -' j) + (j -' i)) + 1 & ( for k, k1 being Element of NAT st 1 <= k & k <= len fs1 & k1 = fs1 . k holds
k1 <= n ) & ( for i1 being Element of NAT st 1 <= i1 & i1 < len fs1 & not fs1 . (i1 + 1) = (fs1 /. i1) + 1 holds
fs1 . i1 = (fs1 /. (i1 + 1)) + 1 ) ) ; ::_thesis: verum
end;

theorem Th6: :: GOBRD10:6
for n, i, j being Element of NAT st i <= n & j <= n holds
ex fs1 being FinSequence of NAT st
( fs1 . 1 = i & fs1 . (len fs1) = j & len fs1 = ((i -' j) + (j -' i)) + 1 & ( for k, k1 being Element of NAT st 1 <= k & k <= len fs1 & k1 = fs1 . k holds
k1 <= n ) & ( for i1 being Element of NAT st 1 <= i1 & i1 < len fs1 holds
fs1 /. i1,fs1 /. (i1 + 1) are_adjacent1 ) )
proof
let n, i, j be Element of NAT ; ::_thesis: ( i <= n & j <= n implies ex fs1 being FinSequence of NAT st
( fs1 . 1 = i & fs1 . (len fs1) = j & len fs1 = ((i -' j) + (j -' i)) + 1 & ( for k, k1 being Element of NAT st 1 <= k & k <= len fs1 & k1 = fs1 . k holds
k1 <= n ) & ( for i1 being Element of NAT st 1 <= i1 & i1 < len fs1 holds
fs1 /. i1,fs1 /. (i1 + 1) are_adjacent1 ) ) )
assume  ( i <= n & j <= n ) ; ::_thesis: ex fs1 being FinSequence of NAT st
( fs1 . 1 = i & fs1 . (len fs1) = j & len fs1 = ((i -' j) + (j -' i)) + 1 & ( for k, k1 being Element of NAT st 1 <= k & k <= len fs1 & k1 = fs1 . k holds
k1 <= n ) & ( for i1 being Element of NAT st 1 <= i1 & i1 < len fs1 holds
fs1 /. i1,fs1 /. (i1 + 1) are_adjacent1 ) )
then consider fs1 being FinSequence of NAT  such that
A1: ( fs1 . 1 = i & fs1 . (len fs1) = j & len fs1 = ((i -' j) + (j -' i)) + 1 & ( for k, k1 being Element of NAT st 1 <= k & k <= len fs1 & k1 = fs1 . k holds
k1 <= n ) ) and
A2: for i1 being Element of NAT st 1 <= i1 & i1 < len fs1 & not fs1 . (i1 + 1) = (fs1 /. i1) + 1 holds
fs1 . i1 = (fs1 /. (i1 + 1)) + 1 by Th5;
 for i1 being Element of NAT st 1 <= i1 & i1 < len fs1 holds
fs1 /. i1,fs1 /. (i1 + 1) are_adjacent1
proof
let i1 be Element of NAT ; ::_thesis: ( 1 <= i1 & i1 < len fs1 implies fs1 /. i1,fs1 /. (i1 + 1) are_adjacent1 )
assume A3: ( 1 <= i1 & i1 < len fs1 ) ; ::_thesis: fs1 /. i1,fs1 /. (i1 + 1) are_adjacent1
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  fs1 /. i1,fs1 /. (i1 + 1) are_adjacent1 by A5, A4, Def1; ::_thesis: verum
end;
hence  ex fs1 being FinSequence of NAT st
( fs1 . 1 = i & fs1 . (len fs1) = j & len fs1 = ((i -' j) + (j -' i)) + 1 & ( for k, k1 being Element of NAT st 1 <= k & k <= len fs1 & k1 = fs1 . k holds
k1 <= n ) & ( for i1 being Element of NAT st 1 <= i1 & i1 < len fs1 holds
fs1 /. i1,fs1 /. (i1 + 1) are_adjacent1 ) ) by A1; ::_thesis: verum
end;

theorem Th7: :: GOBRD10:7
for n, m, i1, j1, i2, j2 being Element of NAT st i1 <= n & j1 <= m & i2 <= n & j2 <= m holds
ex fs1, fs2 being FinSequence of NAT st
( ( for i, k1, k2 being Element of NAT 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 being Element of NAT st 1 <= i & i < len fs1 holds
fs1 /. i,fs2 /. i,fs1 /. (i + 1),fs2 /. (i + 1) are_adjacent2 ) )
proof
let n, m, i1, j1, i2, j2 be Element of NAT ; ::_thesis: ( i1 <= n & j1 <= m & i2 <= n & j2 <= m implies ex fs1, fs2 being FinSequence of NAT st
( ( for i, k1, k2 being Element of NAT 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 being Element of NAT st 1 <= i & i < len fs1 holds
fs1 /. i,fs2 /. i,fs1 /. (i + 1),fs2 /. (i + 1) are_adjacent2 ) ) )
assume that
A1: i1 <= n and
A2: j1 <= m and
A3: i2 <= n and
A4: j2 <= m ; ::_thesis: ex fs1, fs2 being FinSequence of NAT st
( ( for i, k1, k2 being Element of NAT 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 being Element of NAT st 1 <= i & i < len fs1 holds
fs1 /. i,fs2 /. i,fs1 /. (i + 1),fs2 /. (i + 1) are_adjacent2 ) )
consider gs1 being 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 being Element of NAT st 1 <= k & k <= len gs1 & k1 = gs1 . k holds
k1 <= n and
A9: for k being Element of NAT st 1 <= k & k < len gs1 holds
gs1 /. k,gs1 /. (k + 1) are_adjacent1 by A1, A3, Th6;
consider gs2 being 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 being Element of NAT st 1 <= k & k <= len gs2 & k1 = gs2 . k holds
k1 <= m and
A14: for k being Element of NAT st 1 <= k & k < len gs2 holds
gs2 /. k,gs2 /. (k + 1) are_adjacent1 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);
set hs2 = (((len gs1) -' 1) |-> j1) ^ gs2;
A17: len (gs1 ^ (((len gs2) -' 1) |-> i2)) = (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 ((((len gs1) -' 1) |-> j1) ^ gs2) by FINSEQ_1:22 ;
A21: for i, k1, k2 being Element of NAT st i in dom (gs1 ^ (((len gs2) -' 1) |-> i2)) & k1 = (gs1 ^ (((len gs2) -' 1) |-> i2)) . i & k2 = ((((len gs1) -' 1) |-> j1) ^ gs2) . i holds
( k1 <= n & k2 <= m )
proof
 dom ((((len gs1) -' 1) |-> j1) ^ gs2) = Seg ((len (((len gs1) -' 1) |-> j1)) + (len gs2)) by FINSEQ_1:def_7;
then  len ((((len gs1) -' 1) |-> j1) ^ gs2) = (len (((len gs1) -' 1) |-> j1)) + (len gs2) by FINSEQ_1:def_3;
then A22: len ((((len gs1) -' 1) |-> j1) ^ gs2) = ((len gs1) -' 1) + (len gs2) by CARD_1:def_7;
let i, k1, k2 be Element of NAT ; ::_thesis: ( i in dom (gs1 ^ (((len gs2) -' 1) |-> i2)) & k1 = (gs1 ^ (((len gs2) -' 1) |-> i2)) . i & k2 = ((((len gs1) -' 1) |-> j1) ^ gs2) . i implies ( k1 <= n & k2 <= m ) )
assume that
A23: i in dom (gs1 ^ (((len gs2) -' 1) |-> i2)) and
A24: k1 = (gs1 ^ (((len gs2) -' 1) |-> i2)) . i and
A25: k2 = ((((len gs1) -' 1) |-> j1) ^ gs2) . i ; ::_thesis: ( k1 <= n & k2 <= m )
 i in Seg (len (gs1 ^ (((len gs2) -' 1) |-> i2))) by A23, FINSEQ_1:def_3;
then  ( ( 1 <= i & i <= (len gs1) -' 1 ) or ( ((len gs1) -' 1) + 1 <= i & i <= len ((((len gs1) -' 1) |-> j1) ^ gs2) ) ) by A17, A20, FINSEQ_1:1, NAT_1:13;
then  ( ( 1 <= i & i <= (len gs1) -' 1 ) or ( ((len gs1) - 1) + 1 <= i & i <= len ((((len gs1) -' 1) |-> j1) ^ gs2) ) ) 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 ((((len gs1) -' 1) |-> j1) ^ gs2) ) ) 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 ((((len gs1) -' 1) |-> j1) ^ gs2)) - ((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 ((((len gs1) -' 1) |-> j1) ^ gs2)) - (len gs1)) + 1 ) ) ;
A27: now__::_thesis:_(_(_1_<=_(i_-_(len_gs1))_+_1_&_i_-_(len_gs1)_<=_(len_((((len_gs1)_-'_1)_|->_j1)_^_gs2))_-_(len_gs1)_&_k2_<=_m_)_or_(_1_<=_i_&_i_<=_(len_gs1)_-_1_&_k2_<=_m_)_)
percases ( ( 1 <= (i - (len gs1)) + 1 & i - (len gs1) <= (len ((((len gs1) -' 1) |-> j1) ^ gs2)) - (len gs1) ) or ( 1 <= i & i <= (len gs1) - 1 ) ) by A26, XREAL_1:6;
caseA28: ( 1 <= (i - (len gs1)) + 1 & i - (len gs1) <= (len ((((len gs1) -' 1) |-> j1) ^ gs2)) - (len gs1) ) ; ::_thesis: k2 <= m
then A29: (i + 1) - (len gs1) <= ((len ((((len gs1) -' 1) |-> j1) ^ gs2)) - (len gs1)) + 1 by XREAL_1:6;
A30: len (((len gs1) -' 1) |-> j1) = (len gs1) -' 1 by CARD_1:def_7;
A31: ((len ((((len gs1) -' 1) |-> j1) ^ gs2)) + 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 ((((len gs1) -' 1) |-> j1) ^ gs2)) - (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  ((((len gs1) -' 1) |-> j1) ^ gs2) . i = gs2 . ((i + 1) -' (len gs1)) by A33, FINSEQ_1:def_7;
hence  k2 <= m by A13, A25, A28, A29, A31, A32; ::_thesis: verum
end;
caseA34: ( 1 <= i & i <= (len gs1) - 1 ) ; ::_thesis: k2 <= m
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 ((((len gs1) -' 1) |-> j1) ^ gs2) . i = (((len gs1) -' 1) |-> j1) . i by FINSEQ_1:def_7
.= j1 by A34, A35, Lm1 ;
hence  k2 <= m by A2, A25; ::_thesis: verum
end;
end;
end;
 dom (gs1 ^ (((len gs2) -' 1) |-> i2)) = Seg ((len gs1) + (len (((len gs2) -' 1) |-> i2))) by FINSEQ_1:def_7;
then A36: len (gs1 ^ (((len gs2) -' 1) |-> i2)) = (len gs1) + (len (((len gs2) -' 1) |-> i2)) by FINSEQ_1:def_3;
then A37: (len (gs1 ^ (((len gs2) -' 1) |-> i2))) -' (len gs1) = (len (gs1 ^ (((len gs2) -' 1) |-> i2))) - (len gs1) by XREAL_0:def_2;
A38: len (gs1 ^ (((len gs2) -' 1) |-> i2)) = (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 (gs1 ^ (((len gs2) -' 1) |-> i2)) ) ) by A23, FINSEQ_3:25, XREAL_1:9;
now__::_thesis:_(_(_1_<=_i_&_i_<=_len_gs1_&_k1_<=_n_)_or_(_0_<_i_-_(len_gs1)_&_i_-_(len_gs1)_<=_(len_(gs1_^_(((len_gs2)_-'_1)_|->_i2)))_-'_(len_gs1)_&_k1_<=_n_)_)
percases ( ( 1 <= i & i <= len gs1 ) or ( 0 < i - (len gs1) & i - (len gs1) <= (len (gs1 ^ (((len gs2) -' 1) |-> i2))) -' (len gs1) ) ) by A37, A39, XREAL_1:9;
caseA40: ( 1 <= i & i <= len gs1 ) ; ::_thesis: k1 <= n
then  i in dom gs1 by FINSEQ_3:25;
then  (gs1 ^ (((len gs2) -' 1) |-> i2)) . i = gs1 . i by FINSEQ_1:def_7;
hence  k1 <= n by A8, A24, A40; ::_thesis: verum
end;
caseA41: ( 0 < i - (len gs1) & i - (len gs1) <= (len (gs1 ^ (((len gs2) -' 1) |-> i2))) -' (len gs1) ) ; ::_thesis: k1 <= n
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 (gs1 ^ (((len gs2) -' 1) |-> i2))) -' (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 (gs1 ^ (((len gs2) -' 1) |-> i2)) . 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; ::_thesis: verum
end;
end;
end;
hence  ( k1 <= n & k2 <= m ) by A27; ::_thesis: verum
end;
A48: for i being Element of NAT st 1 <= i & i < len (gs1 ^ (((len gs2) -' 1) |-> i2)) holds
(gs1 ^ (((len gs2) -' 1) |-> i2)) /. i,((((len gs1) -' 1) |-> j1) ^ gs2) /. i,(gs1 ^ (((len gs2) -' 1) |-> i2)) /. (i + 1),((((len gs1) -' 1) |-> j1) ^ gs2) /. (i + 1) are_adjacent2
proof
let i be Element of NAT ; ::_thesis: ( 1 <= i & i < len (gs1 ^ (((len gs2) -' 1) |-> i2)) implies (gs1 ^ (((len gs2) -' 1) |-> i2)) /. i,((((len gs1) -' 1) |-> j1) ^ gs2) /. i,(gs1 ^ (((len gs2) -' 1) |-> i2)) /. (i + 1),((((len gs1) -' 1) |-> j1) ^ gs2) /. (i + 1) are_adjacent2 )
assume that
A49: 1 <= i and
A50: i < len (gs1 ^ (((len gs2) -' 1) |-> i2)) ; ::_thesis: (gs1 ^ (((len gs2) -' 1) |-> i2)) /. i,((((len gs1) -' 1) |-> j1) ^ gs2) /. i,(gs1 ^ (((len gs2) -' 1) |-> i2)) /. (i + 1),((((len gs1) -' 1) |-> j1) ^ gs2) /. (i + 1) are_adjacent2
now__::_thesis:_(_(_i_<_len_gs1_&_(_(_(gs1_^_(((len_gs2)_-'_1)_|->_i2))_/._i,(gs1_^_(((len_gs2)_-'_1)_|->_i2))_/._(i_+_1)_are_adjacent1_&_((((len_gs1)_-'_1)_|->_j1)_^_gs2)_/._i_=_((((len_gs1)_-'_1)_|->_j1)_^_gs2)_/._(i_+_1)_)_or_(_(gs1_^_(((len_gs2)_-'_1)_|->_i2))_/._i_=_(gs1_^_(((len_gs2)_-'_1)_|->_i2))_/._(i_+_1)_&_((((len_gs1)_-'_1)_|->_j1)_^_gs2)_/._i,((((len_gs1)_-'_1)_|->_j1)_^_gs2)_/._(i_+_1)_are_adjacent1_)_)_)_or_(_i_>=_len_gs1_&_(_(_(gs1_^_(((len_gs2)_-'_1)_|->_i2))_/._i,(gs1_^_(((len_gs2)_-'_1)_|->_i2))_/._(i_+_1)_are_adjacent1_&_((((len_gs1)_-'_1)_|->_j1)_^_gs2)_/._i_=_((((len_gs1)_-'_1)_|->_j1)_^_gs2)_/._(i_+_1)_)_or_(_(gs1_^_(((len_gs2)_-'_1)_|->_i2))_/._i_=_(gs1_^_(((len_gs2)_-'_1)_|->_i2))_/._(i_+_1)_&_((((len_gs1)_-'_1)_|->_j1)_^_gs2)_/._i,((((len_gs1)_-'_1)_|->_j1)_^_gs2)_/._(i_+_1)_are_adjacent1_)_)_)_)
percases ( i < len gs1 or i >= len gs1 ) ;
caseA51: i < len gs1 ; ::_thesis: ( ( (gs1 ^ (((len gs2) -' 1) |-> i2)) /. i,(gs1 ^ (((len gs2) -' 1) |-> i2)) /. (i + 1) are_adjacent1 & ((((len gs1) -' 1) |-> j1) ^ gs2) /. i = ((((len gs1) -' 1) |-> j1) ^ gs2) /. (i + 1) ) or ( (gs1 ^ (((len gs2) -' 1) |-> i2)) /. i = (gs1 ^ (((len gs2) -' 1) |-> i2)) /. (i + 1) & ((((len gs1) -' 1) |-> j1) ^ gs2) /. i,((((len gs1) -' 1) |-> j1) ^ gs2) /. (i + 1) are_adjacent1 ) )
then A52: i + 1 <= len gs1 by NAT_1:13;
A53: now__::_thesis:_(_(_i_+_1_<=_(len_gs1)_-'_1_&_(gs1_^_(((len_gs2)_-'_1)_|->_i2))_/._i,(gs1_^_(((len_gs2)_-'_1)_|->_i2))_/._(i_+_1)_are_adjacent1_)_or_(_i_+_1_>_(len_gs1)_-'_1_&_(gs1_^_(((len_gs2)_-'_1)_|->_i2))_/._i,(gs1_^_(((len_gs2)_-'_1)_|->_i2))_/._(i_+_1)_are_adjacent1_)_)
percases ( i + 1 <= (len gs1) -' 1 or i + 1 > (len gs1) -' 1 ) ;
case i + 1 <= (len gs1) -' 1 ; ::_thesis: (gs1 ^ (((len gs2) -' 1) |-> i2)) /. i,(gs1 ^ (((len gs2) -' 1) |-> i2)) /. (i + 1) are_adjacent1
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 (gs1 ^ (((len gs2) -' 1) |-> i2)) by FINSEQ_1:26;
then A59: (gs1 ^ (((len gs2) -' 1) |-> i2)) /. (i + 1) = (gs1 ^ (((len gs2) -' 1) |-> i2)) . (i + 1) by A57, PARTFUN1:def_6
.= gs1 . (i + 1) by A57, FINSEQ_1:def_7
.= gs1 /. (i + 1) by A57, PARTFUN1:def_6 ;
(gs1 ^ (((len gs2) -' 1) |-> i2)) /. i = (gs1 ^ (((len gs2) -' 1) |-> i2)) . i by A58, A56, PARTFUN1:def_6
.= gs1 . i by A56, FINSEQ_1:def_7
.= gs1 /. i by A56, PARTFUN1:def_6 ;
hence  (gs1 ^ (((len gs2) -' 1) |-> i2)) /. i,(gs1 ^ (((len gs2) -' 1) |-> i2)) /. (i + 1) are_adjacent1 by A9, A49, A55, A59; ::_thesis: verum
end;
case i + 1 > (len gs1) -' 1 ; ::_thesis: (gs1 ^ (((len gs2) -' 1) |-> i2)) /. i,(gs1 ^ (((len gs2) -' 1) |-> i2)) /. (i + 1) are_adjacent1
 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 (gs1 ^ (((len gs2) -' 1) |-> i2)) by FINSEQ_1:26;
then A62: (gs1 ^ (((len gs2) -' 1) |-> i2)) /. (i + 1) = (gs1 ^ (((len gs2) -' 1) |-> i2)) . (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 (gs1 ^ (((len gs2) -' 1) |-> i2)) /. i = (gs1 ^ (((len gs2) -' 1) |-> i2)) . i by A61, PARTFUN1:def_6
.= gs1 . i by A63, FINSEQ_1:def_7
.= gs1 /. i by A63, PARTFUN1:def_6 ;
hence  (gs1 ^ (((len gs2) -' 1) |-> i2)) /. i,(gs1 ^ (((len gs2) -' 1) |-> i2)) /. (i + 1) are_adjacent1 by A9, A49, A51, A62; ::_thesis: verum
end;
end;
end;
A64: 1 <= i + 1 by A49, NAT_1:13;
A65: now__::_thesis:_(_(_i_+_1_<=_(len_gs1)_-'_1_&_((((len_gs1)_-'_1)_|->_j1)_^_gs2)_/._(i_+_1)_=_j1_)_or_(_i_+_1_>_(len_gs1)_-'_1_&_((((len_gs1)_-'_1)_|->_j1)_^_gs2)_/._(i_+_1)_=_j1_)_)
percases ( i + 1 <= (len gs1) -' 1 or i + 1 > (len gs1) -' 1 ) ;
caseA66: i + 1 <= (len gs1) -' 1 ; ::_thesis: ((((len gs1) -' 1) |-> j1) ^ gs2) /. (i + 1) = j1
A67: len (((len gs1) -' 1) |-> j1) = (len gs1) -' 1 by CARD_1:def_7;
A68: dom (((len gs1) -' 1) |-> j1) c= dom ((((len gs1) -' 1) |-> j1) ^ gs2) 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 ((((len gs1) -' 1) |-> j1) ^ gs2) . (i + 1) = (((len gs1) -' 1) |-> j1) . (i + 1) by FINSEQ_1:def_7
.= j1 by A64, A66, Lm1 ;
hence  ((((len gs1) -' 1) |-> j1) ^ gs2) /. (i + 1) = j1 by A69, A68, PARTFUN1:def_6; ::_thesis: verum
end;
caseA70: i + 1 > (len gs1) -' 1 ; ::_thesis: ((((len gs1) -' 1) |-> j1) ^ gs2) /. (i + 1) = j1
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 ((((len gs1) -' 1) |-> j1) ^ gs2) = Seg ((len (((len gs1) -' 1) |-> j1)) + (len gs2)) by FINSEQ_1:def_7;
then  len ((((len gs1) -' 1) |-> j1) ^ gs2) = (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 ((((len gs1) -' 1) |-> j1) ^ gs2) by NAT_1:11;
then  len gs1 in Seg (len ((((len gs1) -' 1) |-> j1) ^ gs2)) by A18, FINSEQ_1:1;
then A73: i + 1 in dom ((((len gs1) -' 1) |-> j1) ^ gs2) 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  ((((len gs1) -' 1) |-> j1) ^ gs2) . (i + 1) = j1 by A10, A74, FINSEQ_1:def_7;
hence  ((((len gs1) -' 1) |-> j1) ^ gs2) /. (i + 1) = j1 by A73, PARTFUN1:def_6; ::_thesis: verum
end;
end;
end;
A75: len (((len gs1) -' 1) |-> j1) = (len gs1) -' 1 by CARD_1:def_7;
A76: dom (((len gs1) -' 1) |-> j1) c= dom ((((len gs1) -' 1) |-> j1) ^ gs2) 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 ((((len gs1) -' 1) |-> j1) ^ gs2) . i = (((len gs1) -' 1) |-> j1) . i by FINSEQ_1:def_7
.= j1 by A49, A77, Lm1 ;
hence  ( ( (gs1 ^ (((len gs2) -' 1) |-> i2)) /. i,(gs1 ^ (((len gs2) -' 1) |-> i2)) /. (i + 1) are_adjacent1 & ((((len gs1) -' 1) |-> j1) ^ gs2) /. i = ((((len gs1) -' 1) |-> j1) ^ gs2) /. (i + 1) ) or ( (gs1 ^ (((len gs2) -' 1) |-> i2)) /. i = (gs1 ^ (((len gs2) -' 1) |-> i2)) /. (i + 1) & ((((len gs1) -' 1) |-> j1) ^ gs2) /. i,((((len gs1) -' 1) |-> j1) ^ gs2) /. (i + 1) are_adjacent1 ) ) by A78, A76, A65, A53, PARTFUN1:def_6; ::_thesis: verum
end;
caseA79: i >= len gs1 ; ::_thesis: ( ( (gs1 ^ (((len gs2) -' 1) |-> i2)) /. i,(gs1 ^ (((len gs2) -' 1) |-> i2)) /. (i + 1) are_adjacent1 & ((((len gs1) -' 1) |-> j1) ^ gs2) /. i = ((((len gs1) -' 1) |-> j1) ^ gs2) /. (i + 1) ) or ( (gs1 ^ (((len gs2) -' 1) |-> i2)) /. i = (gs1 ^ (((len gs2) -' 1) |-> i2)) /. (i + 1) & ((((len gs1) -' 1) |-> j1) ^ gs2) /. i,((((len gs1) -' 1) |-> j1) ^ gs2) /. (i + 1) are_adjacent1 ) )
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__::_thesis:_(_not_1_<=_i_-'_(len_gs1)_implies_(gs1_^_(((len_gs2)_-'_1)_|->_i2))_._i_=_i2_)
assume  not 1 <= i -' (len gs1) ; ::_thesis: (gs1 ^ (((len gs2) -' 1) |-> i2)) . i = i2
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  (gs1 ^ (((len gs2) -' 1) |-> i2)) . i = i2 by A6, A85, A87, FINSEQ_1:def_7; ::_thesis: verum
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: (gs1 ^ (((len gs2) -' 1) |-> i2)) . (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 (gs1 ^ (((len gs2) -' 1) |-> i2)) = (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__::_thesis:_(_1_<=_i_-'_(len_gs1)_implies_(gs1_^_(((len_gs2)_-'_1)_|->_i2))_._i_=_i2_)
A99: i = (len gs1) + (i - (len gs1))
.= (len gs1) + (i -' (len gs1)) by A83, XREAL_0:def_2 ;
assume A100: 1 <= i -' (len gs1) ; ::_thesis: (gs1 ^ (((len gs2) -' 1) |-> i2)) . i = i2
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 (gs1 ^ (((len gs2) -' 1) |-> i2)) . i = (((len gs2) -' 1) |-> i2) . (i -' (len gs1)) by A99, FINSEQ_1:def_7
.= i2 by A93, A100, Lm1 ;
hence  (gs1 ^ (((len gs2) -' 1) |-> i2)) . i = i2 ; ::_thesis: verum
end;
 i in dom ((((len gs1) -' 1) |-> j1) ^ gs2) by A17, A20, A49, A50, FINSEQ_3:25;
then A101: ((((len gs1) -' 1) |-> j1) ^ gs2) /. i = ((((len gs1) -' 1) |-> j1) ^ gs2) . ((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 (gs1 ^ (((len gs2) -' 1) |-> i2)) by A49, A50, FINSEQ_3:25;
then A102: (gs1 ^ (((len gs2) -' 1) |-> i2)) /. i = i2 by A86, A98, PARTFUN1:def_6;
 ( i + 1 <= len (gs1 ^ (((len gs2) -' 1) |-> i2)) & 0 + 1 <= i + 1 ) by A50, NAT_1:13;
then A103: i + 1 in Seg (len (gs1 ^ (((len gs2) -' 1) |-> i2))) by FINSEQ_1:1;
then  i + 1 in dom ((((len gs1) -' 1) |-> j1) ^ gs2) by A17, A20, FINSEQ_1:def_3;
then A104: ((((len gs1) -' 1) |-> j1) ^ gs2) /. (i + 1) = ((((len gs1) -' 1) |-> j1) ^ gs2) . ((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 (gs1 ^ (((len gs2) -' 1) |-> i2)) by A103, FINSEQ_1:def_3;
hence  ( ( (gs1 ^ (((len gs2) -' 1) |-> i2)) /. i,(gs1 ^ (((len gs2) -' 1) |-> i2)) /. (i + 1) are_adjacent1 & ((((len gs1) -' 1) |-> j1) ^ gs2) /. i = ((((len gs1) -' 1) |-> j1) ^ gs2) /. (i + 1) ) or ( (gs1 ^ (((len gs2) -' 1) |-> i2)) /. i = (gs1 ^ (((len gs2) -' 1) |-> i2)) /. (i + 1) & ((((len gs1) -' 1) |-> j1) ^ gs2) /. i,((((len gs1) -' 1) |-> j1) ^ gs2) /. (i + 1) are_adjacent1 ) ) by A14, A102, A91, A84, A94, A104, A101, PARTFUN1:def_6; ::_thesis: verum
end;
end;
end;
hence  (gs1 ^ (((len gs2) -' 1) |-> i2)) /. i,((((len gs1) -' 1) |-> j1) ^ gs2) /. i,(gs1 ^ (((len gs2) -' 1) |-> i2)) /. (i + 1),((((len gs1) -' 1) |-> j1) ^ gs2) /. (i + 1) are_adjacent2 by Def2; ::_thesis: verum
end;
A105: now__::_thesis:_(_(_(len_gs1)_-'_1_=_0_&_((((len_gs1)_-'_1)_|->_j1)_^_gs2)_._1_=_j1_&_((((len_gs1)_-'_1)_|->_j1)_^_gs2)_._(len_((((len_gs1)_-'_1)_|->_j1)_^_gs2))_=_j2_)_or_(_(len_gs1)_-'_1_<>_0_&_((((len_gs1)_-'_1)_|->_j1)_^_gs2)_._1_=_j1_&_((((len_gs1)_-'_1)_|->_j1)_^_gs2)_._(len_((((len_gs1)_-'_1)_|->_j1)_^_gs2))_=_j2_)_)
percases ( (len gs1) -' 1 = 0 or (len gs1) -' 1 <> 0 ) ;
case (len gs1) -' 1 = 0 ; ::_thesis: ( ((((len gs1) -' 1) |-> j1) ^ gs2) . 1 = j1 & ((((len gs1) -' 1) |-> j1) ^ gs2) . (len ((((len gs1) -' 1) |-> j1) ^ gs2)) = j2 )
then (((len gs1) -' 1) |-> j1) ^ gs2 = (<*> NAT) ^ gs2
.= gs2 by FINSEQ_1:34 ;
hence  ( ((((len gs1) -' 1) |-> j1) ^ gs2) . 1 = j1 & ((((len gs1) -' 1) |-> j1) ^ gs2) . (len ((((len gs1) -' 1) |-> j1) ^ gs2)) = j2 ) by A10, A11; ::_thesis: verum
end;
caseA106: (len gs1) -' 1 <> 0 ; ::_thesis: ( ((((len gs1) -' 1) |-> j1) ^ gs2) . 1 = j1 & ((((len gs1) -' 1) |-> j1) ^ gs2) . (len ((((len gs1) -' 1) |-> j1) ^ gs2)) = j2 )
 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: ((((len gs1) -' 1) |-> j1) ^ gs2) . 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 ((((len gs1) -' 1) |-> j1) ^ gs2) = (len (((len gs1) -' 1) |-> j1)) + (len gs2) ) by FINSEQ_1:22, CARD_1:def_7;
hence  ( ((((len gs1) -' 1) |-> j1) ^ gs2) . 1 = j1 & ((((len gs1) -' 1) |-> j1) ^ gs2) . (len ((((len gs1) -' 1) |-> j1) ^ gs2)) = j2 ) by A11, A107, A108, A109, Lm1, FINSEQ_1:def_7; ::_thesis: verum
end;
end;
end;
A110: 1 in dom gs1 by A18, FINSEQ_3:25;
now__::_thesis:_(_(_(len_gs2)_-'_1_=_0_&_(gs1_^_(((len_gs2)_-'_1)_|->_i2))_._1_=_i1_&_(gs1_^_(((len_gs2)_-'_1)_|->_i2))_._(len_(gs1_^_(((len_gs2)_-'_1)_|->_i2)))_=_i2_)_or_(_(len_gs2)_-'_1_<>_0_&_(gs1_^_(((len_gs2)_-'_1)_|->_i2))_._1_=_i1_&_(gs1_^_(((len_gs2)_-'_1)_|->_i2))_._(len_(gs1_^_(((len_gs2)_-'_1)_|->_i2)))_=_i2_)_)
percases ( (len gs2) -' 1 = 0 or (len gs2) -' 1 <> 0 ) ;
case (len gs2) -' 1 = 0 ; ::_thesis: ( (gs1 ^ (((len gs2) -' 1) |-> i2)) . 1 = i1 & (gs1 ^ (((len gs2) -' 1) |-> i2)) . (len (gs1 ^ (((len gs2) -' 1) |-> i2))) = i2 )
then gs1 ^ (((len gs2) -' 1) |-> i2) = gs1 ^ (<*> NAT)
.= gs1 by FINSEQ_1:34 ;
hence  ( (gs1 ^ (((len gs2) -' 1) |-> i2)) . 1 = i1 & (gs1 ^ (((len gs2) -' 1) |-> i2)) . (len (gs1 ^ (((len gs2) -' 1) |-> i2))) = i2 ) by A5, A6; ::_thesis: verum
end;
case (len gs2) -' 1 <> 0 ; ::_thesis: ( (gs1 ^ (((len gs2) -' 1) |-> i2)) . 1 = i1 & (gs1 ^ (((len gs2) -' 1) |-> i2)) . (len (gs1 ^ (((len gs2) -' 1) |-> i2))) = i2 )
then A111: 0 + 1 <= (len gs2) -' 1 by NAT_1:13;
A112: len (gs1 ^ (((len gs2) -' 1) |-> i2)) = (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  ( (gs1 ^ (((len gs2) -' 1) |-> i2)) . 1 = i1 & (gs1 ^ (((len gs2) -' 1) |-> i2)) . (len (gs1 ^ (((len gs2) -' 1) |-> i2))) = i2 ) by A5, A110, A112, FINSEQ_1:def_7; ::_thesis: verum
end;
end;
end;
hence  ex fs1, fs2 being FinSequence of NAT st
( ( for i, k1, k2 being Element of NAT 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 being Element of NAT st 1 <= i & i < len fs1 holds
fs1 /. i,fs2 /. i,fs1 /. (i + 1),fs2 /. (i + 1) are_adjacent2 ) ) by A7, A12, A17, A20, A105, A21, A48; ::_thesis: verum
end;

theorem :: GOBRD10:8
for n, m being Element of NAT
for S being set
for Y being Subset of S
for F being Matrix of n,m, bool S st ex i, j being Element of NAT st
( i in Seg n & j in Seg m & F * (i,j) c= Y ) & ( for i1, j1, i2, j2 being Element of NAT st i1 in Seg n & i2 in Seg n & j1 in Seg m & j2 in Seg m & i1,j1,i2,j2 are_adjacent2 holds
( F * (i1,j1) c= Y iff F * (i2,j2) c= Y ) ) holds
for i, j being Element of NAT st i in Seg n & j in Seg m holds
F * (i,j) c= Y
proof
let n, m be Element of NAT ; ::_thesis: for S being set
for Y being Subset of S
for F being Matrix of n,m, bool S st ex i, j being Element of NAT st
( i in Seg n & j in Seg m & F * (i,j) c= Y ) & ( for i1, j1, i2, j2 being Element of NAT st i1 in Seg n & i2 in Seg n & j1 in Seg m & j2 in Seg m & i1,j1,i2,j2 are_adjacent2 holds
( F * (i1,j1) c= Y iff F * (i2,j2) c= Y ) ) holds
for i, j being Element of NAT st i in Seg n & j in Seg m holds
F * (i,j) c= Y
let S be set ; ::_thesis: for Y being Subset of S
for F being Matrix of n,m, bool S st ex i, j being Element of NAT st
( i in Seg n & j in Seg m & F * (i,j) c= Y ) & ( for i1, j1, i2, j2 being Element of NAT st i1 in Seg n & i2 in Seg n & j1 in Seg m & j2 in Seg m & i1,j1,i2,j2 are_adjacent2 holds
( F * (i1,j1) c= Y iff F * (i2,j2) c= Y ) ) holds
for i, j being Element of NAT st i in Seg n & j in Seg m holds
F * (i,j) c= Y
let Y be Subset of S; ::_thesis: for F being Matrix of n,m, bool S st ex i, j being Element of NAT st
( i in Seg n & j in Seg m & F * (i,j) c= Y ) & ( for i1, j1, i2, j2 being Element of NAT st i1 in Seg n & i2 in Seg n & j1 in Seg m & j2 in Seg m & i1,j1,i2,j2 are_adjacent2 holds
( F * (i1,j1) c= Y iff F * (i2,j2) c= Y ) ) holds
for i, j being Element of NAT st i in Seg n & j in Seg m holds
F * (i,j) c= Y
let F be Matrix of n,m, bool S; ::_thesis: ( ex i, j being Element of NAT st
( i in Seg n & j in Seg m & F * (i,j) c= Y ) & ( for i1, j1, i2, j2 being Element of NAT st i1 in Seg n & i2 in Seg n & j1 in Seg m & j2 in Seg m & i1,j1,i2,j2 are_adjacent2 holds
( F * (i1,j1) c= Y iff F * (i2,j2) c= Y ) ) implies for i, j being Element of NAT st i in Seg n & j in Seg m holds
F * (i,j) c= Y )
assume that
A1: ex i, j being Element of NAT st
( i in Seg n & j in Seg m & F * (i,j) c= Y ) and
A2: for i1, j1, i2, j2 being Element of NAT st i1 in Seg n & i2 in Seg n & j1 in Seg m & j2 in Seg m & i1,j1,i2,j2 are_adjacent2 holds
( F * (i1,j1) c= Y iff F * (i2,j2) c= Y ) ; ::_thesis: for i, j being Element of NAT st i in Seg n & j in Seg m holds
F * (i,j) c= Y
consider i1, j1 being Element of NAT  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 being Element of NAT st i in Seg n & j in Seg m holds
F * (i,j) c= Y ::_thesis: verum
proof
let i2, j2 be Element of NAT ; ::_thesis: ( i2 in Seg n & j2 in Seg m implies F * (i2,j2) c= Y )
assume that
A10: i2 in Seg n and
A11: j2 in Seg m ; ::_thesis: F * (i2,j2) c= Y
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__::_thesis:_(_(_(_n_=_0_or_m_=_0_)_&_contradiction_)_or_(_n_<>_0_&_m_<>_0_&_F_*_(i2,j2)_c=_Y_)_)
percases ( n = 0 or m = 0 or ( n <> 0 & m <> 0 ) ) ;
case ( n = 0 or m = 0 ) ; ::_thesis: contradiction
hence  contradiction by A3, A4; ::_thesis: verum
end;
caseA16: ( n <> 0 & m <> 0 ) ; ::_thesis: F * (i2,j2) c= Y
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 being FinSequence of NAT  such that
A20: for i, k1, k2 being Element of NAT 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 being Element of NAT st 1 <= i & i < len fs1 holds
fs1 /. i,fs2 /. i,fs1 /. (i + 1),fs2 /. (i + 1) are_adjacent2 by A18, Th7;
deffunc H1( Nat) ->  Element of NAT = (fs1 /. $1) + 1;
 ex p being FinSequence of NAT st
( len p = len fs1 & ( for j being Nat st j in dom p holds
p . j = H1(j) ) ) from FINSEQ_2:sch_1();
then consider p1 being FinSequence of NAT  such that
A28: len p1 = len fs1 and
A29: for k being Nat st k in dom p1 holds
p1 . k = (fs1 /. k) + 1 ;
deffunc H2( Nat) ->  Element of NAT = (fs2 /. $1) + 1;
 ex p being FinSequence of NAT st
( len p = len fs2 & ( for k being Nat st k in dom p holds
p . k = H2(k) ) ) from FINSEQ_2:sch_1();
then consider p2 being FinSequence of NAT  such that
A30: len p2 = len fs2 and
A31: for k being 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 S1[ Element of 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 being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
A35: 1 <= k + 1 by NAT_1:12;
assume A36: ( k + 1 <= len p1 implies F * ((p1 /. (k + 1)),(p2 /. (k + 1))) c= Y ) ; ::_thesis: S1[k + 1]
now__::_thesis:_(_(_k_+_1_<=_len_p1_&_S1[k_+_1]_)_or_(_k_+_1_>_len_p1_&_S1[k_+_1]_)_)
percases ( k + 1 <= len p1 or k + 1 > len p1 ) ;
caseA37: k + 1 <= len p1 ; ::_thesis: S1[k + 1]
now__::_thesis:_(_(_(k_+_1)_+_1_<=_len_p1_&_S1[k_+_1]_)_or_(_(k_+_1)_+_1_>_len_p1_&_S1[k_+_1]_)_)
percases ( (k + 1) + 1 <= len p1 or (k + 1) + 1 > len p1 ) ;
caseA38: (k + 1) + 1 <= len p1 ; ::_thesis: S1[k + 1]
set lp11 = fs1 /. ((k + 1) + 1);
set 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  fs1 /. ((k + 1) + 1) <= n - 1 by A19, A20, A41, A40;
then A43: (fs1 /. ((k + 1) + 1)) + 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) = (fs2 /. ((k + 1) + 1)) + 1 by A25, A28, A31, A32, A39;
 fs2 /. ((k + 1) + 1) <= m -' 1 by A20, A41, A42, A40;
then A45: (fs2 /. ((k + 1) + 1)) + 1 <= (m - 1) + 1 by A17, XREAL_1:6;
 1 <= 1 + (fs2 /. ((k + 1) + 1)) 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
.= (fs1 /. ((k + 1) + 1)) + 1 by A28, A29, A33, A39 ;
set lp1 = fs1 /. (k + 1);
set 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: fs2 /. (k + 1) = 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
.= (fs1 /. (k + 1)) + 1 by A28, A29, A33, A49 ;
A52: k + 1 in dom fs1 by A28, A49, FINSEQ_1:def_3;
then A53: fs1 /. (k + 1) = fs1 . (k + 1) by PARTFUN1:def_6;
then  fs1 /. (k + 1) <= n - 1 by A19, A20, A52, A50;
then A54: (fs1 /. (k + 1)) + 1 <= (n - 1) + 1 by XREAL_1:6;
 1 <= 1 + (fs1 /. (k + 1)) 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
.= (fs2 /. (k + 1)) + 1 by A25, A28, A31, A32, A49 ;
 fs2 /. (k + 1) <= m -' 1 by A20, A52, A53, A50;
then A57: (fs2 /. (k + 1)) + 1 <= (m - 1) + 1 by A17, XREAL_1:6;
 1 <= 1 + (fs2 /. (k + 1)) by NAT_1:11;
then A58: p2 /. (k + 1) in Seg m by A56, A57, FINSEQ_1:1;
 1 <= 1 + (fs1 /. ((k + 1) + 1)) 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
.= (fs2 /. ((k + 1) + 1)) + 1 by A25, A28, A31, A32, A39 ;
then  p1 /. (k + 1),p2 /. (k + 1),p1 /. ((k + 1) + 1),p2 /. ((k + 1) + 1) are_adjacent2 by A27, A28, A35, A48, A51, A56, A47, Th3;
hence  S1[k + 1] by A2, A36, A37, A55, A58, A59, A46; ::_thesis: verum
end;
case (k + 1) + 1 > len p1 ; ::_thesis: S1[k + 1]
hence  S1[k + 1] ; ::_thesis: verum
end;
end;
end;
hence  S1[k + 1] ; ::_thesis: verum
end;
case k + 1 > len p1 ; ::_thesis: S1[k + 1]
hence  S1[k + 1] by NAT_1:13; ::_thesis: verum
end;
end;
end;
hence  S1[k + 1] ; ::_thesis: verum
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: S1[ 0 ] by A5, A63;
A66: for i being Element of NAT holds S1[i] from NAT_1:sch_1(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  F * (i2,j2) c= Y by A13, A14, A28, A66, A67, A70, A71, A69; ::_thesis: verum
end;
end;
end;
hence  F * (i2,j2) c= Y ; ::_thesis: verum
end;
end;