<:seqx,seqy:> is Function of NAT,[: the carrier of X, the carrier of Y:] ;
hence <:seqx,seqy:> is sequence of [:X,Y:] ; :: thesis: verum