let X be set ; :: thesis: for P being Relation holds P * [:(rng P),X:] = [:(dom P),X:]
let P be Relation; :: thesis: P * [:(rng P),X:] = [:(dom P),X:]
P * [:(rng P),X:] = [:(P " (rng P)),X:] by Lm61;
hence P * [:(rng P),X:] = [:(dom P),X:] by RELAT_1:134; :: thesis: verum