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