let x be Element of D; :: thesis: x is FinSequence of S
x is Element of S * ;
hence x is FinSequence of S ; :: thesis: verum