now

let i be Nat; :: thesis: ( i in dom (J | n) implies ex L being Element of K ex k being Nat st (J | n) . i = Jordan_block L,k )
assume i in dom (J | n) ; :: thesis: ex L being Element of K ex k being Nat st (J | n) . i = Jordan_block L,k
then ( i in dom J & (J | n) . i = J . i ) by FUNCT_1:70, RELAT_1:86;
hence ex L being Element of K ex k being Nat st (J | n) . i = Jordan_block L,k by Def2; :: thesis: verum

end;

hence J | n is FinSequence_of_Jordan_block of K by Def2; :: thesis: verum