take A = NetStr(# the carrier of R,(id the carrier of R),(id the carrier of R) #); :: thesis: ( A is strict & not A is empty & A is Function-yielding )
thus ( A is strict & not A is empty ) ; :: thesis: A is Function-yielding
let x be set ; :: 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 A1: x in dom the mapping of A ; :: thesis: the mapping of A . x is set
then the mapping of A . x = x by FUNCT_1:35;
hence the mapping of A . x is set by A1; :: thesis: verum