consider F being non-empty FinSequence_of_Jordan_block of 1_ K,K;
take F ; :: thesis: F is non-empty
thus F is non-empty ; :: thesis: verum