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