consider p being Element of R;
consider N being net of R;
take ConstantNet (N,p) ; :: thesis: ( ConstantNet (N,p) is strict & ConstantNet (N,p) is Function-yielding )
thus ( ConstantNet (N,p) is strict & ConstantNet (N,p) is Function-yielding ) ; :: thesis: verum