defpred S₁[ object ] means ex y being Element of N st
( y = $1 & i <= y );
consider X being set such that
A1: for x being object holds
( x in X iff ( x in the carrier of N & S₁[x] ) ) from XBOOLE_0:sch 1();
X c= the carrier of N by A1;
then reconsider f = the mapping of N | X as Function of X, the carrier of L by FUNCT_2:32;
set IT = NetStr(# X,( the InternalRel of N |_2 X),f #);
take NetStr(# X,( the InternalRel of N |_2 X),f #) ; :: thesis: ( ( for x being object holds
( x in the carrier of NetStr(# X,( the InternalRel of N |_2 X),f #) iff ex y being Element of N st
( y = x & i <= y ) ) ) & the InternalRel of NetStr(# X,( the InternalRel of N |_2 X),f #) = the InternalRel of N |_2 the carrier of NetStr(# X,( the InternalRel of N |_2 X),f #) & the mapping of NetStr(# X,( the InternalRel of N |_2 X),f #) = the mapping of N | the carrier of NetStr(# X,( the InternalRel of N |_2 X),f #) )
thus for x being object holds
( x in the carrier of NetStr(# X,( the InternalRel of N |_2 X),f #) iff ex y being Element of N st
( y = x & i <= y ) ) by A1; :: thesis: ( the InternalRel of NetStr(# X,( the InternalRel of N |_2 X),f #) = the InternalRel of N |_2 the carrier of NetStr(# X,( the InternalRel of N |_2 X),f #) & the mapping of NetStr(# X,( the InternalRel of N |_2 X),f #) = the mapping of N | the carrier of NetStr(# X,( the InternalRel of N |_2 X),f #) )
thus ( the InternalRel of NetStr(# X,( the InternalRel of N |_2 X),f #) = the InternalRel of N |_2 the carrier of NetStr(# X,( the InternalRel of N |_2 X),f #) & the mapping of NetStr(# X,( the InternalRel of N |_2 X),f #) = the mapping of N | the carrier of NetStr(# X,( the InternalRel of N |_2 X),f #) ) ; :: thesis: verum