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

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 R * (id Y)
let y be object ; :: thesis: ( [x,y] in R implies [x,y] in R * (id Y) )
assume A2: [x,y] in R ; :: thesis: [x,y] in R * (id Y)
then y in rng R by XTUPLE_0:def 13;
then [y,y] in id Y by A1, Def8;
hence [x,y] in R * (id Y) by A2, Def6; :: thesis: verum

end;

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