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