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