reconsider JJ = <*(Jordan_block L,1)*> as FinSequence_of_Jordan_block of L,K by Th11;
take JJ ; :: thesis: JJ is non-empty

now

let x be set ; :: thesis: ( x in dom JJ implies not JJ . x is empty )
assume A1: x in dom JJ ; :: thesis: not JJ . x is empty
dom JJ = {1} by FINSEQ_1:4, FINSEQ_1:def 8;
then ( JJ . 1 = Jordan_block L,1 & x = 1 & len (Jordan_block L,1) = 1 ) by A1, Def1, FINSEQ_1:def 8, TARSKI:def 1;
hence not JJ . x is empty ; :: thesis: verum

end;

hence JJ is non-empty by FUNCT_1:def 15; :: thesis: verum