let M be Matrix of D; :: thesis: M is FinSequence-yielding
let x be set ; :: according to MATRLIN:def 1 :: thesis: ( x in dom M implies M . x is FinSequence )
assume A1: x in dom M ; :: thesis: M . x is FinSequence
then reconsider i = x as Nat by FINSEQ_3:25;
M . i = Line M,i by A1, MATRIX_2:18;
hence M . x is FinSequence ; :: thesis: verum