let X, Y be set ; :: thesis: rng [:X,Y:] c= Y
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng [:X,Y:] or x in Y )
assume x in rng [:X,Y:] ; :: thesis: x in Y
then ex y being object st [y,x] in [:X,Y:] by XTUPLE_0:def 13;
hence x in Y by ZFMISC_1:87; :: thesis: verum