take f = seq_const 0; :: thesis: ( f is NAT -valued & f is INT -valued )
thus ( f is NAT -valued & f is INT -valued ) ; :: thesis: verum