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

proof

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

end;