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 :: thesis: for i being Nat st i in dom <*(Jordan_block (L,n))*> holds
ex a being Element of K ex k being Nat st <*(Jordan_block (L,n))*> . i = Jordan_block (a,k)
A1: dom <*(Jordan_block (L,n))*> = {1} by FINSEQ_1:2, 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 :: thesis: for i being Nat st i in dom JJ holds
ex n being Nat st JJ . i = Jordan_block (L,n)
A2: dom JJ = {1} by FINSEQ_1:2, 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