( XSeq . n in rng XSeq & rng XSeq c= Si ) by NAT_1:52, RELAT_1:def 19;
hence XSeq . n is Element of Si ; :: thesis: verum