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