let R, S be Relation; :: thesis: ( ( S * R = S & R * (R \ (id (dom R))) = {} implies S * (R \ (id (dom R))) = {} ) & ( R * S = S & (R \ (id (dom R))) * R = {} implies (R \ (id (dom R))) * S = {} ) )
thus ( S * R = S & R * (R \ (id (dom R))) = {} implies S * (R \ (id (dom R))) = {} ) :: thesis: ( R * S = S & (R \ (id (dom R))) * R = {} implies (R \ (id (dom R))) * S = {} )

proof

assume ( S * R = S & R * (R \ (id (dom R))) = {} ) ; :: thesis: S * (R \ (id (dom R))) = {}
then S * (R \ (id (dom R))) = S * {} by RELAT_1:36
.= {} ;
hence S * (R \ (id (dom R))) = {} ; :: thesis: verum

end;

assume ( R * S = S & (R \ (id (dom R))) * R = {} ) ; :: thesis: (R \ (id (dom R))) * S = {}
then (R \ (id (dom R))) * S = {} * S by RELAT_1:36
.= {} ;
hence (R \ (id (dom R))) * S = {} ; :: thesis: verum