take 1 ; :: according to FINSEQ_1:def 2 :: thesis: dom <*x*> = Seg 1
thus dom <*x*> = Seg 1 by Def8; :: thesis: verum