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 Th53;
then R | (dom (CL R)) = id (dom (CL R)) by A1, Th54;
hence ( R | (dom (CL R)) = id (dom (CL R)) & R | (rng (CL R)) = id (dom (CL R)) ) by Th45; :: thesis: verum

end;

thus ( (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)) ) ) :: thesis: verum

proof

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 Th53;
then (rng (CL R)) | R = id (rng (CL R)) by A2, Th54;
then (dom (CL R)) | R = id (rng (CL R)) by Th45;
hence ( (dom (CL R)) | R = id (dom (CL R)) & (rng (CL R)) | R = id (rng (CL R)) ) by Th45; :: thesis: verum

end;