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 A1: i in dom (J | n) ; :: thesis: ex L being Element of K ex k being Nat st (J | n) . i = Jordan_block L,k
i in dom J by A1, RELAT_1:86;
then ( (J | n) . i = J . i & ex L being Element of K ex k being Nat st J . i = Jordan_block L,k ) by A1, Def2, FUNCT_1:70;
hence ex L being Element of K ex k being Nat st (J | n) . i = Jordan_block L,k ; :: thesis: verum

end;

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