defpred S₁[ set , set ] means ex y being Element of L st
( y = the mapping of N . $1 & $2 = x "/\" y );
A1: for e being Element of N ex u being Element of L st S₁[e,u]

proof

let e be Element of N; :: thesis: ex u being Element of L st S₁[e,u]
take x "/\" ( the mapping of N . e) ; :: thesis: S₁[e,x "/\" ( the mapping of N . e)]
take the mapping of N . e ; :: thesis: ( the mapping of N . e = the mapping of N . e & x "/\" ( the mapping of N . e) = x "/\" ( the mapping of N . e) )
thus ( the mapping of N . e = the mapping of N . e & x "/\" ( the mapping of N . e) = x "/\" ( the mapping of N . e) ) ; :: thesis: verum

end;

ex g being Function of the carrier of N, the carrier of L st
for i being Element of N holds S₁[i,g . i] from FUNCT_2:sch 3(A1);
then consider g being Function of the carrier of N, the carrier of L such that
A2: for i being Element of N ex y being Element of L st
( y = the mapping of N . i & g . i = x "/\" y ) ;
take NetStr(# the carrier of N, the InternalRel of N,g #) ; :: thesis: ( RelStr(# the carrier of NetStr(# the carrier of N, the InternalRel of N,g #), the InternalRel of NetStr(# the carrier of N, the InternalRel of N,g #) #) = RelStr(# the carrier of N, the InternalRel of N #) & ( for i being Element of NetStr(# the carrier of N, the InternalRel of N,g #) ex y being Element of L st
( y = the mapping of N . i & the mapping of NetStr(# the carrier of N, the InternalRel of N,g #) . i = x "/\" y ) ) )
thus ( RelStr(# the carrier of NetStr(# the carrier of N, the InternalRel of N,g #), the InternalRel of NetStr(# the carrier of N, the InternalRel of N,g #) #) = RelStr(# the carrier of N, the InternalRel of N #) & ( for i being Element of NetStr(# the carrier of N, the InternalRel of N,g #) ex y being Element of L st
( y = the mapping of N . i & the mapping of NetStr(# the carrier of N, the InternalRel of N,g #) . i = x "/\" y ) ) ) by A2; :: thesis: verum