let x, y be set ; :: thesis: ( x in dom <*y*> implies x = 1 )
assume x in dom <*y*> ; :: thesis: x = 1
then x in Seg 1 by FINSEQ_1:def 8;
hence x = 1 by FINSEQ_1:2, TARSKI:def 1; :: thesis: verum