theorem Th15: :: JORDAN4:15

for D being non empty set
for f1 being FinSequence of D
for k being Nat st 1 <= k & k <= len f1 holds
( mid (f1,k,k) = <*(f1 /. k)*> & len (mid (f1,k,k)) = 1 )