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 i in dom (J | n) ; :: thesis: ex L being Element of K 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 L being Element of K ex k being Nat st (J | n) . i = Jordan_block (L,k) by Def2; :: thesis: verum
end;
hence J | n is FinSequence_of_Jordan_block of K by Def2; :: thesis: verum