for p, q being FinSequence of NAT
for x, y being Variable st All (x,p) = All (y,q) holds
( x = y & p = q )