let D be set ; :: thesis: for R being D -valued Relation
for y being object st y in rng R holds
y in D
let R be D -valued Relation; :: thesis: for y being object st y in rng R holds
y in D
rng R c= D by Def17;
hence for y being object st y in rng R holds
y in D ; :: thesis: verum