let Y be set ; :: thesis: for y being object
for R being Relation holds
( y in rng (Y |` R) iff ( y in Y & y in rng R ) )
let y be object ; :: thesis: for R being Relation holds
( y in rng (Y |` R) iff ( y in Y & y in rng R ) )
let R be Relation; :: thesis: ( y in rng (Y |` R) iff ( y in Y & y in rng R ) )
thus ( y in rng (Y |` R) implies ( y in Y & y in rng R ) ) :: thesis: ( y in Y & y in rng R implies y in rng (Y |` R) )

proof

assume y in rng (Y |` R) ; :: thesis: ( y in Y & y in rng R )
then consider x being object such that
A1: [x,y] in Y |` R by XTUPLE_0:def 13;
[x,y] in R by A1, Def10;
hence ( y in Y & y in rng R ) by A1, Def10, XTUPLE_0:def 13; :: thesis: verum

end;

assume A2: y in Y ; :: thesis: ( not y in rng R or y in rng (Y |` R) )
assume y in rng R ; :: thesis: y in rng (Y |` R)
then consider x being object such that
A3: [x,y] in R by XTUPLE_0:def 13;
[x,y] in Y |` R by A2, A3, Def10;
hence y in rng (Y |` R) by XTUPLE_0:def 13; :: thesis: verum