let D, E be non empty set ; :: thesis: for R being Relation of D,E

for y being object holds

( y in rng R iff ex x being Element of D st [x,y] in R )

let R be Relation of D,E; :: thesis: for y being object holds

( y in rng R iff ex x being Element of D st [x,y] in R )

let y be object ; :: thesis: ( y in rng R iff ex x being Element of D st [x,y] in R )

thus ( y in rng R implies ex x being Element of D st [x,y] in R ) :: thesis: ( ex x being Element of D st [x,y] in R implies y in rng R )

for y being object holds

( y in rng R iff ex x being Element of D st [x,y] in R )

let R be Relation of D,E; :: thesis: for y being object holds

( y in rng R iff ex x being Element of D st [x,y] in R )

let y be object ; :: thesis: ( y in rng R iff ex x being Element of D st [x,y] in R )

thus ( y in rng R implies ex x being Element of D st [x,y] in R ) :: thesis: ( ex x being Element of D st [x,y] in R implies y in rng R )

proof

thus
( ex x being Element of D st [x,y] in R implies y in rng R )
by XTUPLE_0:def 13; :: thesis: verum
assume
y in rng R
; :: thesis: ex x being Element of D st [x,y] in R

then consider x being object such that

A1: [x,y] in R by XTUPLE_0:def 13;

reconsider a = x as Element of D by A1, ZFMISC_1:87;

take a ; :: thesis: [a,y] in R

thus [a,y] in R by A1; :: thesis: verum

end;then consider x being object such that

A1: [x,y] in R by XTUPLE_0:def 13;

reconsider a = x as Element of D by A1, ZFMISC_1:87;

take a ; :: thesis: [a,y] in R

thus [a,y] in R by A1; :: thesis: verum