now :: thesis: for i being Nat st i in dom (J /^ n) holds
ex L being Element of K ex k being Nat st (J /^ n) . i = Jordan_block (L,k)

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:26;
then ( 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 6;
hence ex L being Element of K ex k being Nat st (J /^ n) . i = Jordan_block (L,k) by A1, FINSEQ_5:27; :: thesis: verum

end;

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