for y being object st y in rng <*x*> holds
y in D ;
hence <*x*> is FinSequence of D ; :: thesis: verum