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_adjacent ) ) )
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_adjacent ) )
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_adjacent

proof

let i1 be Element of NAT ; :: thesis: ( 1 <= i1 & i1 < len fs1 implies fs1 /. i1,fs1 /. (i1 + 1) are_adjacent )
assume A3: ( 1 <= i1 & i1 < len fs1 ) ; :: thesis: fs1 /. i1,fs1 /. (i1 + 1) are_adjacent
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_adjacent by A5, A4; :: 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_adjacent ) ) by A1; :: thesis: verum