let x1, x2, y1, y2 be object ; :: thesis: ( x1 <> x2 implies rng ((x1,x2) --> (y1,y2)) = {y1,y2} )
set h = (x1,x2) --> (y1,y2);
assume A1: x1 <> x2 ; :: thesis: rng ((x1,x2) --> (y1,y2)) = {y1,y2}
thus rng ((x1,x2) --> (y1,y2)) c= {y1,y2} by Th62; :: according to XBOOLE_0:def 10 :: thesis: {y1,y2} c= rng ((x1,x2) --> (y1,y2))
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in {y1,y2} or y in rng ((x1,x2) --> (y1,y2)) )
assume y in {y1,y2} ; :: thesis: y in rng ((x1,x2) --> (y1,y2))
then ( y = y1 or y = y2 ) by TARSKI:def 2;
then A2: ( ((x1,x2) --> (y1,y2)) . x1 = y or ((x1,x2) --> (y1,y2)) . x2 = y ) by A1, Th63;
dom ((x1,x2) --> (y1,y2)) = {x1,x2} by Th62;
then ( x1 in dom ((x1,x2) --> (y1,y2)) & x2 in dom ((x1,x2) --> (y1,y2)) ) by TARSKI:def 2;
hence y in rng ((x1,x2) --> (y1,y2)) by A2, FUNCT_1:def 3; :: thesis: verum