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 FinSequence of the carrier of K * )
assume i in dom F ; :: thesis: ex b₁ being set st F . i is FinSequence of the carrier of K *
then ex L being Element of K ex n being Nat st F . i = Jordan_block (L,n) by A1;
hence ex b₁ being set st F . i is FinSequence of the carrier of K * ; :: thesis: verum