let R be Relation; :: thesis: ( ( (id (dom (CL R))) * (R \ (id (dom (CL R)))) = {} implies ( R | (dom (CL R)) = id (dom (CL R)) & R | (rng (CL R)) = id (dom (CL R)) ) ) & ( (R \ (id (rng (CL R)))) * (id (rng (CL R))) = {} implies ( (dom (CL R)) |` R = id (dom (CL R)) & (rng (CL R)) |` R = id (rng (CL R)) ) ) )
thus ( (id (dom (CL R))) * (R \ (id (dom (CL R)))) = {} implies ( R | (dom (CL R)) = id (dom (CL R)) & R | (rng (CL R)) = id (dom (CL R)) ) ) :: thesis: ( (R \ (id (rng (CL R)))) * (id (rng (CL R))) = {} implies ( (dom (CL R)) |` R = id (dom (CL R)) & (rng (CL R)) |` R = id (rng (CL R)) ) )

proof

assume A1: (id (dom (CL R))) * (R \ (id (dom (CL R)))) = {} ; :: thesis: ( R | (dom (CL R)) = id (dom (CL R)) & R | (rng (CL R)) = id (dom (CL R)) )
id (dom (CL R)) c= R by Th34;
then R | (dom (CL R)) = id (dom (CL R)) by A1, Th35;
hence ( R | (dom (CL R)) = id (dom (CL R)) & R | (rng (CL R)) = id (dom (CL R)) ) by Th26; :: thesis: verum

end;

assume A2: (R \ (id (rng (CL R)))) * (id (rng (CL R))) = {} ; :: thesis: ( (dom (CL R)) |` R = id (dom (CL R)) & (rng (CL R)) |` R = id (rng (CL R)) )
id (rng (CL R)) c= R by Th34;
then (rng (CL R)) |` R = id (rng (CL R)) by A2, Th35;
then (dom (CL R)) |` R = id (rng (CL R)) by Th26;
hence ( (dom (CL R)) |` R = id (dom (CL R)) & (rng (CL R)) |` R = id (rng (CL R)) ) by Th26; :: thesis: verum