let k be Nat; :: thesis: for p being Element of Permutations (k + 1) st p . (k + 1) <> k + 1 holds
ex tr being Element of Permutations (k + 1) st
( tr is being_transposition & tr . (p . (k + 1)) = k + 1 & (tr * p) . (k + 1) = k + 1 )
set k1 = k + 1;
let p be Element of Permutations (k + 1); :: thesis: ( p . (k + 1) <> k + 1 implies ex tr being Element of Permutations (k + 1) st
( tr is being_transposition & tr . (p . (k + 1)) = k + 1 & (tr * p) . (k + 1) = k + 1 ) )
assume A1: p . (k + 1) <> k + 1 ; :: thesis: ex tr being Element of Permutations (k + 1) st
( tr is being_transposition & tr . (p . (k + 1)) = k + 1 & (tr * p) . (k + 1) = k + 1 )
reconsider p' = p as Permutation of (Seg (k + 1)) by MATRIX_2:def 11;
A2: ( dom p' = Seg (k + 1) & rng p' = Seg (k + 1) & k + 1 in Seg (k + 1) ) by FINSEQ_1:5, FUNCT_2:67, FUNCT_2:def 3;
then A3: p . (k + 1) in Seg (k + 1) by FUNCT_1:def 5;
then p . (k + 1) <= k + 1 by FINSEQ_1:3;
then p . (k + 1) < k + 1 by A1, XXREAL_0:1;
then consider tr being Element of Permutations (k + 1) such that
A4: ( tr is being_transposition & tr . (p . (k + 1)) = k + 1 ) by A2, A3, Th16;
reconsider tr' = tr as Permutation of (Seg (k + 1)) by MATRIX_2:def 11;
dom tr' = Seg (k + 1) by FUNCT_2:67;
then dom (tr * p) = Seg (k + 1) by A2, RELAT_1:46;
then (tr * p) . (k + 1) = tr . (p . (k + 1)) by A2, FUNCT_1:22;
hence ex tr being Element of Permutations (k + 1) st
( tr is being_transposition & tr . (p . (k + 1)) = k + 1 & (tr * p) . (k + 1) = k + 1 ) by A4; :: thesis: verum