:: deftheorem defines being_transposition MATRIX_1:def 14 :
for n being Nat
for p being Permutation of (Seg n) holds
( p is being_transposition iff ex i, j being Nat st
( i in dom p & j in dom p & i <> j & p . i = j & p . j = i & ( for k being Nat st k <> i & k <> j & k in dom p holds
p . k = k ) ) );