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