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