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:56;
A3: the mapping of N in Funcs ( the carrier of N, the carrier of T) by FUNCT_2:8;
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:4;
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