let a, b, x, y be object ; :: thesis: ( dom {[a,b],[x,y]} = {a,x} & rng {[a,b],[x,y]} = {b,y} )
set R = {[a,b],[x,y]};
thus dom {[a,b],[x,y]} = {a,x} :: thesis: rng {[a,b],[x,y]} = {b,y}
proof
thus dom {[a,b],[x,y]} c= {a,x} :: according to XBOOLE_0:def 10 :: thesis: {a,x} c= dom {[a,b],[x,y]}
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in dom {[a,b],[x,y]} or z in {a,x} )
assume z in dom {[a,b],[x,y]} ; :: thesis: z in {a,x}
then consider c being object such that
A2: [z,c] in {[a,b],[x,y]} by XTUPLE_0:def 12;
( [z,c] = [a,b] or [z,c] = [x,y] ) by A2, TARSKI:def 2;
then ( z = a or z = x ) by XTUPLE_0:1;
hence z in {a,x} by TARSKI:def 2; :: thesis: verum
end;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in {a,x} or z in dom {[a,b],[x,y]} )
assume z in {a,x} ; :: thesis: z in dom {[a,b],[x,y]}
then ( z = a or z = x ) by TARSKI:def 2;
then ( [z,b] in {[a,b],[x,y]} or [z,y] in {[a,b],[x,y]} ) by TARSKI:def 2;
hence z in dom {[a,b],[x,y]} by XTUPLE_0:def 12; :: thesis: verum
end;
thus rng {[a,b],[x,y]} c= {b,y} :: according to XBOOLE_0:def 10 :: thesis: {b,y} c= rng {[a,b],[x,y]}
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rng {[a,b],[x,y]} or z in {b,y} )
assume z in rng {[a,b],[x,y]} ; :: thesis: z in {b,y}
then consider d being object such that
A3: [d,z] in {[a,b],[x,y]} by XTUPLE_0:def 13;
( [d,z] = [a,b] or [d,z] = [x,y] ) by A3, TARSKI:def 2;
then ( z = b or z = y ) by XTUPLE_0:1;
hence z in {b,y} by TARSKI:def 2; :: thesis: verum
end;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in {b,y} or z in rng {[a,b],[x,y]} )
assume z in {b,y} ; :: thesis: z in rng {[a,b],[x,y]}
then ( z = b or z = y ) by TARSKI:def 2;
then ( [a,z] in {[a,b],[x,y]} or [x,z] in {[a,b],[x,y]} ) by TARSKI:def 2;
hence z in rng {[a,b],[x,y]} by XTUPLE_0:def 13; :: thesis: verum