let x be Element of X; :: thesis: x is FinSequence of D
reconsider y = x as Element of D * ;
y is FinSequence of D ;
hence x is FinSequence of D ; :: thesis: verum