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

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