theorem Th15: :: FINSEQ_6:193

for k being Nat
for f1 being FinSequence st k in dom f1 holds
( mid (f1,k,k) = <*(f1 . k)*> & len (mid (f1,k,k)) = 1 )