now

let i be Nat; :: thesis: ( i in dom (J /^ n) implies ex k being Nat st (J /^ n) . i = Jordan_block (L,k) )
assume A1: i in dom (J /^ n) ; :: thesis: 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 k being Nat st J . (n + i) = Jordan_block (L,k) ) by Def3, PARTFUN1:def 8;
(J /^ n) . i = (J /^ n) /. i by A1, PARTFUN1:def 8;
hence 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 L,K by Def3; :: thesis: verum