the carrier of T c= Funcs I,the carrier of S by A1, YELLOW_1:28;
then A2: 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;
A3: the mapping of N in Funcs the carrier of N,the carrier of T by FUNCT_2:11;
then A4: rng ((commute the mapping of N) . i) c= the carrier of S by A2, EQUATION:3;
dom ((commute the mapping of N) . i) = the carrier of N by A3, A2, EQUATION:3;
then reconsider f = (commute the mapping of N) . i as Function of the carrier of N,the carrier of S by A4, FUNCT_2:def 1, RELSET_1:11;
set A = NetStr(# the carrier of N,the InternalRel of N,f #);
A5: 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 #) ;
[#] N is directed by WAYBEL_0:def 6;
then [#] NetStr(# the carrier of N,the InternalRel of N,f #) is directed by A5, WAYBEL_0:3;
then reconsider A = NetStr(# the carrier of N,the InternalRel of N,f #) as strict net of S by A5, WAYBEL_0:def 6, 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