set F = the non-empty FinSequence_of_Jordan_block of 1_ K,K;
take the non-empty FinSequence_of_Jordan_block of 1_ K,K ; :: thesis: the non-empty FinSequence_of_Jordan_block of 1_ K,K is non-empty
thus the non-empty FinSequence_of_Jordan_block of 1_ K,K is non-empty ; :: thesis: verum