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