reconsider JJ = <*(Jordan_block (L,1))*> as FinSequence_of_Jordan_block of L,K by Th11;
take JJ ; :: thesis: JJ is non-empty
now :: thesis: for x being object st x in dom JJ holds
not JJ . x is empty
A1: dom JJ = {1} by FINSEQ_1:2, FINSEQ_1:def 8;
let x be object ; :: thesis: ( x in dom JJ implies not JJ . x is empty )
assume x in dom JJ ; :: thesis: not JJ . x is empty
then ( JJ . 1 = Jordan_block (L,1) & x = 1 ) by A1, FINSEQ_1:def 8, TARSKI:def 1;
hence not JJ . x is empty by Def1; :: thesis: verum
end;
hence JJ is non-empty ; :: thesis: verum