let N be NetStr over R; :: thesis: N is Function-yielding
let x be object ; :: according to FUNCOP_1:def 6,YELLOW14:def 2 :: thesis: ( not x in dom the mapping of N or the mapping of N . x is set )
assume x in dom the mapping of N ; :: thesis: the mapping of N . x is set
then the mapping of N . x in rng the mapping of N by FUNCT_1:def 3;
hence the mapping of N . x is set ; :: thesis: verum