for X1, X2 being set
for F1 being SetSequence of X1
for F2 being SetSequence of X2
for n being Nat st F1 is non-descending & F2 is non-descending holds
[:(F1 . n),(F2 . n):] c= [:(F1 . (n + 1)),(F2 . (n + 1)):]