let K be Field; :: thesis: for L being Element of K holds {} is FinSequence_of_Jordan_block of L,K
let L be Element of K; :: thesis: {} is FinSequence_of_Jordan_block of L,K
reconsider F = <*> {} as FinSequence_of_Jordan_block of K by Lm2;
for i being Nat st i in dom F holds
ex n being Nat st F . i = Jordan_block (L,n) ;
hence {} is FinSequence_of_Jordan_block of L,K by Def3; :: thesis: verum