take {} ; :: thesis: for a being FinSequence st a in {} holds
rng a c= X
thus for a being FinSequence st a in {} holds
rng a c= X ; :: thesis: verum