let n be Nat; :: thesis: for K being Field
for L being Element of K holds <*(Jordan_block L,n)*> is FinSequence_of_Jordan_block of L,K
let K be Field; :: thesis: for L being Element of K holds <*(Jordan_block L,n)*> is FinSequence_of_Jordan_block of L,K
let L be Element of K; :: thesis: <*(Jordan_block L,n)*> is FinSequence_of_Jordan_block of L,K

now

A1: dom <*(Jordan_block L,n)*> = {1} by FINSEQ_1:4, FINSEQ_1:def 8;
let i be Nat; :: thesis: ( i in dom <*(Jordan_block L,n)*> implies ex a being Element of K ex k being Nat st <*(Jordan_block L,n)*> . i = Jordan_block a,k )
assume i in dom <*(Jordan_block L,n)*> ; :: thesis: ex a being Element of K ex k being Nat st <*(Jordan_block L,n)*> . i = Jordan_block a,k
then ( <*(Jordan_block L,n)*> . 1 = Jordan_block L,n & i = 1 ) by A1, FINSEQ_1:def 8, TARSKI:def 1;
hence ex a being Element of K ex k being Nat st <*(Jordan_block L,n)*> . i = Jordan_block a,k ; :: thesis: verum

end;

then reconsider JJ = <*(Jordan_block L,n)*> as FinSequence_of_Jordan_block of K by Def2;

now

A2: dom JJ = {1} by FINSEQ_1:4, FINSEQ_1:def 8;
let i be Nat; :: thesis: ( i in dom JJ implies ex n being Nat st JJ . i = Jordan_block L,n )
assume i in dom JJ ; :: thesis: ex n being Nat st JJ . i = Jordan_block L,n
then ( JJ . 1 = Jordan_block L,n & i = 1 ) by A2, FINSEQ_1:def 8, TARSKI:def 1;
hence ex n being Nat st JJ . i = Jordan_block L,n ; :: thesis: verum

end;

hence <*(Jordan_block L,n)*> is FinSequence_of_Jordan_block of L,K by Def3; :: thesis: verum