let D be non empty set ; :: thesis: for M being Matrix of D holds <*M*> is Matrix-yielding
let M be Matrix of D; :: thesis: <*M*> is Matrix-yielding

now

let i be Nat; :: thesis: ( i in dom <*M*> implies <*M*> . i is Matrix of D )
assume A1: i in dom <*M*> ; :: thesis: <*M*> . i is Matrix of D
dom <*M*> = {1} by FINSEQ_1:4, FINSEQ_1:def 8;
then ( <*M*> . 1 = M & i = 1 ) by A1, FINSEQ_1:def 8, TARSKI:def 1;
hence <*M*> . i is Matrix of D ; :: thesis: verum

end;

hence <*M*> is Matrix-yielding by Def2; :: thesis: verum