thus XSeq . n is Element of Si ; :: thesis: verum