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