theorem Th8: :: MATRIX11:8

for n being Nat
for P being Permutation of (Seg n) st P is being_transposition holds
for i, j being Nat st i < j holds
( P . i = j iff ( i in dom P & j in dom P & P . i = j & P . j = i & ( for k being Nat st k <> i & k <> j & k in dom P holds
P . k = k ) ) )