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 + n in dom J by A1, FINSEQ_5:29;
then A2: ( J . (n + i) = J /. (n + i) & ex L being Element of K ex k being Nat st J . (n + i) = Jordan_block L,k ) by Def2, PARTFUN1:def 8;
(J /^ n) . i = (J /^ n) /. i by A1, PARTFUN1:def 8;
hence ex L being Element of K ex k being Nat st (J /^ n) . i = Jordan_block L,k by A1, A2, FINSEQ_5:30; :: thesis: verum

end;

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