let n be Nat; :: thesis: for p being Permutation of (Seg n) st p = id (Seg n) holds
not p is being_transposition
let p be Permutation of (Seg n); :: thesis: ( p = id (Seg n) implies not p is being_transposition )
assume A1: p = id (Seg n) ; :: thesis: not p is being_transposition
then dom p = Seg n by FUNCT_1:17;
then for i, j being Nat holds
( not i in dom p or not j in dom p or not i <> j or not p . i = j or not p . j = i or ex k being Nat st
( k <> i & k <> j & k in dom p & not p . k = k ) ) by A1, FUNCT_1:17;
hence not p is being_transposition by MATRIX_1:def 14; :: thesis: verum