consider p being Element of ;
consider N being net of Function-yielding ;
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