let x1, x2, y1, y2 be set ; :: 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 Th65; :: according to XBOOLE_0:def 10 :: thesis: {y1,y2} c= rng (x1,x2 --> y1,y2)
let y be set ; :: 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, Th66;
dom (x1,x2 --> y1,y2) = {x1,x2} by Th65;
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 5; :: thesis: verum