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