reconsider F = <*> {} as FinSequence_of_Jordan_block of K by Lm2;
take F ; :: thesis: for i being Nat st i in dom F holds
ex n being Nat st F . i = Jordan_block (L,n)
thus for i being Nat st i in dom F holds
ex n being Nat st F . i = Jordan_block (L,n) ; :: thesis: verum