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