for seq being Complex_Sequence
for Ns being V42() sequence of NAT holds (seq * Ns) " = (seq ") * Ns