reconsider F = <*> ((D *) *) as FinSequence of (D *) * ;
take F ; :: thesis: F is Matrix-yielding
for i being Nat st i in dom F holds
F . i is Matrix of D ;
hence F is Matrix-yielding by Def2; :: thesis: verum