let n be Nat; :: thesis: for tr being Element of Permutations (n + 2) st tr is being_transposition holds
not tr is even
set K = the Fanoian Field;
let tr be Element of Permutations (n + 2); :: thesis: ( tr is being_transposition implies not tr is even )
assume tr is being_transposition ; :: thesis: not tr is even
then sgn (tr, the Fanoian Field) = - (1_ the Fanoian Field) by Th14;
hence not tr is even by Th23; :: thesis: verum