reconsider s1 = NAT --> (0. S) as sequence of S by FUNCOP_1:57;
take s1 ; :: thesis: s1 is constant
thus s1 is constant ; :: thesis: verum