let F be FinSequence of (the carrier of K * ) * ; :: thesis: ( F is Jordan-block-yielding implies F is Square-Matrix-yielding )
assume A1: F is Jordan-block-yielding ; :: thesis: F is Square-Matrix-yielding
let i be Nat; :: according to MATRIXJ1:def 6 :: thesis: ( not i in dom F or ex b₁ being set st F . i is Matrix of b₁,b₁,the carrier of K )
assume A2: i in dom F ; :: thesis: ex b₁ being set st F . i is Matrix of b₁,b₁,the carrier of K
ex L being Element of K ex n being Nat st F . i = Jordan_block L,n by A1, A2, Def2;
hence ex b₁ being set st F . i is Matrix of b₁,b₁,the carrier of K ; :: thesis: verum