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