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

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