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
A2: R c= R * (id Y)

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 R * (id Y)
let y be set ; :: thesis: ( [x,y] in R implies [x,y] in R * (id Y) )
assume A3: [x,y] in R ; :: thesis: [x,y] in R * (id Y)
then y in rng R by Def5;
then [y,y] in id Y by A1, Def10;
hence [x,y] in R * (id Y) by A3, Def8; :: thesis: verum

end;

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