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

proof

[#] N is directed by WAYBEL_0:def 6;
hence [#] (f * N) is directed by A1, WAYBEL_0:3; :: thesis: verum

end;