let x, y be object ; :: thesis: field {[x,y]} = {x,y}
( dom {[x,y]} = {x} & rng {[x,y]} = {y} ) by Th3;
hence field {[x,y]} = {x,y} by ENUMSET1:1; :: thesis: verum