take seq_const 1 ; :: thesis: ( seq_const 1 is positive-yielding & seq_const 1 is NAT -valued )
thus ( seq_const 1 is positive-yielding & seq_const 1 is NAT -valued ) ; :: thesis: verum