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 )