for X being non empty set
for f being sequence of X
for i, j being Nat ex g being sequence of X st
( ( for n being Nat st n <> i & n <> j holds
f . n = g . n ) & f . i = g . j & f . j = g . i )