let Y be set ; for R being Relation st rng R c= Y holds
R * (id Y) = R
let R be Relation; ( rng R c= Y implies R * (id Y) = R )
assume A1:
rng R c= Y
; R * (id Y) = R
R c= R * (id Y)
proof
let x be
object ;
RELAT_1:def 3 for b being object st [x,b] in R holds
[x,b] in R * (id Y)let y be
object ;
( [x,y] in R implies [x,y] in R * (id Y) )
assume A2:
[x,y] in R
;
[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;
verum
end;
hence
R * (id Y) = R
by Th44; verum