theorem :: RELAT_1:10

for a, b, x, y being object holds
( dom {[a,b],[x,y]} = {a,x} & rng {[a,b],[x,y]} = {b,y} )