let X be set ; :: thesis: for R being Relation st dom R c= X holds
(id X) * R = R
let R be Relation; :: thesis: ( dom R c= X implies (id X) * R = R )
assume A1: dom R c= X ; :: thesis: (id X) * R = R
A2: R c= (id X) * R

proof

let x be set ; :: according to RELAT_1:def 3 :: thesis: for b being set st [x,b] in R holds
[x,b] in (id X) * R
let y be set ; :: thesis: ( [x,y] in R implies [x,y] in (id X) * R )
assume A3: [x,y] in R ; :: thesis: [x,y] in (id X) * R
then x in dom R by Def4;
then [x,x] in id X by A1, Def10;
hence [x,y] in (id X) * R by A3, Def8; :: thesis: verum

end;

(id X) * R c= R by Th76;
hence (id X) * R = R by A2, XBOOLE_0:def 10; :: thesis: verum