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