reconsider F = <*> (( the carrier of K *) *) as FinSequence of ( the carrier of K *) * ;
take F ; :: thesis: F is Jordan-block-yielding
for i being Nat st i in dom F holds
ex L being Element of K ex n being Nat st F . i = Jordan_block (L,n) ;
hence F is Jordan-block-yielding by Def2; :: thesis: verum