theorem :: FOMODEL0:41

for m being Nat
for p1, p2, q1, q2 being FinSequence st p1 is m -element & q1 is m -element & ( p1 ^ p2 = q1 ^ q2 or p2 ^ p1 = q2 ^ q1 ) holds
( p1 = q1 & p2 = q2 )