reconsider F = <*> ((D *) *) as FinSequence of (D *) * ;
take F ; :: thesis: F is Square-Matrix-yielding
thus F is Square-Matrix-yielding ; :: thesis: verum