defpred S_{1}[ 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_{1}[e,u]

for i being Element of N holds S_{1}[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

( y = the mapping of N . $1 & $2 = x "/\" y );

A1: for e being Element of N ex u being Element of L st S

proof

ex g being Function of the carrier of N, the carrier of L st
let e be Element of N; :: thesis: ex u being Element of L st S_{1}[e,u]

take x "/\" ( the mapping of N . e) ; :: thesis: S_{1}[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;take x "/\" ( the mapping of N . e) ; :: thesis: S

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

for i being Element of N holds S

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