:: 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;