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 :: thesis: for i being Nat st i in dom <*M*> holds
<*M*> . i is Matrix of D
A1: <*M*> . 1 = M by FINSEQ_1:def 8;
A2: dom <*M*> = {1} by FINSEQ_1:2, FINSEQ_1:def 8;
let i be Nat; :: thesis: ( i in dom <*M*> implies <*M*> . i is Matrix of D )
assume i in dom <*M*> ; :: thesis: <*M*> . i is Matrix of D
hence <*M*> . i is Matrix of D by A2, A1, TARSKI:def 1; :: thesis: verum
end;
hence <*M*> is Matrix-yielding ; :: thesis: verum