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

end;

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