defpred S1[ 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 S1[e,u]
proof
let e be Element of N; :: thesis: ex u being Element of L st S1[e,u]
take x "/\" ( the mapping of N . e) ; :: thesis: S1[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 S1[i,g . i] from 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