let K be Field; :: thesis: {} is FinSequence_of_Jordan_block of K
reconsider F = <*> ((the carrier of K * ) * ) as FinSequence of (the carrier of K * ) * ;
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 {} is FinSequence_of_Jordan_block of K by Def2; :: thesis: verum