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