let x, y be object ; :: thesis: ( x in dom <*y*> implies x = 1 )
assume x in dom <*y*> ; :: thesis: x = 1
then x in Seg 1 by Th38;
hence x = 1 by Th2, TARSKI:def 1; :: thesis: verum