let n be Nat; 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; 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; <*(Jordan_block (L,n))*> is FinSequence_of_Jordan_block of L,K
now 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;
( 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))*>
;
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)
;
verum end;
then reconsider JJ = <*(Jordan_block (L,n))*> as FinSequence_of_Jordan_block of K by Def2;
hence
<*(Jordan_block (L,n))*> is FinSequence_of_Jordan_block of L,K
by Def3; verum