let X, Y, Z be non empty set ; :: thesis: for f being Function of X,[:Y,Z:] holds rng f is Relation of Y,Z
let f be Function of X,[:Y,Z:]; :: thesis: rng f is Relation of Y,Z
rng f c= [:Y,Z:] by RELSET_1:12;
hence rng f is Relation of Y,Z by RELSET_1:def 1; :: thesis: verum