A2: the mapping of N in Funcs the carrier of N,the carrier of T by FUNCT_2:11;
the carrier of T c= Funcs I,the carrier of S by A1, YELLOW_1:28;
then Funcs the carrier of N,the carrier of T c= Funcs the carrier of N,(Funcs I,the carrier of S) by FUNCT_5:63;
then ( dom ((commute the mapping of N) . i) = the carrier of N & rng ((commute the mapping of N) . i) c= the carrier of S ) by A2, EQUATION:3;
then reconsider f = (commute the mapping of N) . i as Function of the carrier of N,the carrier of S by FUNCT_2:def 1, RELSET_1:11;
set A = NetStr(# the carrier of N,the InternalRel of N,f #);
A3: RelStr(# the carrier of NetStr(# the carrier of N,the InternalRel of N,f #),the InternalRel of NetStr(# the carrier of N,the InternalRel of N,f #) #) = RelStr(# the carrier of N,the InternalRel of N #) ;
NetStr(# the carrier of N,the InternalRel of N,f #) is directed

proof

[#] N is directed by WAYBEL_0:def 6;
hence [#] NetStr(# the carrier of N,the InternalRel of N,f #) is directed by A3, WAYBEL_0:3; :: according to WAYBEL_0:def 6 :: thesis: verum

end;

then reconsider A = NetStr(# the carrier of N,the InternalRel of N,f #) as strict net of S by A3, WAYBEL_8:13;
take A ; :: thesis: ( RelStr(# the carrier of A,the InternalRel of A #) = RelStr(# the carrier of N,the InternalRel of N #) & the mapping of A = (commute the mapping of N) . i )
thus ( RelStr(# the carrier of A,the InternalRel of A #) = RelStr(# the carrier of N,the InternalRel of N #) & the mapping of A = (commute the mapping of N) . i ) ; :: thesis: verum