now :: thesis: for i being Nat st i in dom (J | n) holds
ex k being Nat st (J | n) . i = Jordan_block (L,k)

let i be Nat; :: thesis: ( i in dom (J | n) implies ex k being Nat st (J | n) . i = Jordan_block (L,k) )
assume i in dom (J | n) ; :: thesis: ex k being Nat st (J | n) . i = Jordan_block (L,k)
then ( i in dom J & (J | n) . i = J . i ) by FUNCT_1:47, RELAT_1:57;
hence ex k being Nat st (J | n) . i = Jordan_block (L,k) by Def3; :: thesis: verum

end;

hence J | n is FinSequence_of_Jordan_block of L,K by Def3; :: thesis: verum