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
R c= (id X) * R

proof

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

end;

hence (id X) * R = R by Th44; :: thesis: verum