consider f being non constant FinSequence;
take f ; :: thesis: not f is constant
thus not f is constant ; :: thesis: verum