take {} ; :: thesis: for a being FinSequence st a in {} holds
len a = k
thus for a being FinSequence st a in {} holds
len a = k ; :: thesis: verum