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 p9 = p as Permutation of (Seg (k + 1)) by MATRIX_1:def 12;
A2: dom p9 = Seg (k + 1) by FUNCT_2:52;
A3: rng p9 = Seg (k + 1) by FUNCT_2:def 3;
A4: k + 1 in Seg (k + 1) by FINSEQ_1:3;
then A5: p . (k + 1) in Seg (k + 1) by A2, A3, FUNCT_1:def 3;
then p . (k + 1) <= k + 1 by FINSEQ_1:1;
then p . (k + 1) < k + 1 by A1, XXREAL_0:1;
then consider tr being Element of Permutations (k + 1) such that
A6: tr is being_transposition and
A7: tr . (p . (k + 1)) = k + 1 by A4, A5, Th16;
reconsider tr9 = tr as Permutation of (Seg (k + 1)) by MATRIX_1:def 12;
dom tr9 = Seg (k + 1) by FUNCT_2:52;
then dom (tr * p) = Seg (k + 1) by A2, A3, RELAT_1:27;
then (tr * p) . (k + 1) = tr . (p . (k + 1)) by FINSEQ_1:3, FUNCT_1:12;
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 A6, A7; :: thesis: verum