( RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of (f * N), the InternalRel of (f * N) #) & [#] N is directed ) by Def8, WAYBEL_0:def 6;
hence [#] (f * N) is directed by WAYBEL_0:3; :: according to WAYBEL_0:def 6 :: thesis: verum