reconsider F = <*> (( the carrier of K *) *) as FinSequence of ( the carrier of K *) * ;
take F ; :: thesis: F is Jordan-block-yielding
thus F is Jordan-block-yielding ; :: thesis: verum