take A = NetStr(# the carrier of R,(id the carrier of R),(id the carrier of R) #); :: thesis: ( A is strict & A is Function-yielding )
thus A is strict ; :: thesis: A is Function-yielding
let x be object ; :: according to FUNCOP_1:def 6,YELLOW14:def 2 :: thesis: ( not x in dom the mapping of A or the mapping of A . x is set )
assume x in dom the mapping of A ; :: thesis: the mapping of A . x is set
hence the mapping of A . x is set by FUNCT_1:18; :: thesis: verum