let i, n be Element of NAT ; :: thesis: for p being Element of Permutations n st i in Seg n holds
ex k being Element of NAT st
( k in Seg n & i = p . k )
let p be Element of Permutations n; :: thesis: ( i in Seg n implies ex k being Element of NAT st
( k in Seg n & i = p . k ) )
A1: p is Permutation of (Seg n) by MATRIX_1:def 12;
then A2: dom p = Seg n by FUNCT_2:52;
then reconsider s = p as FinSequence by FINSEQ_1:def 2;
assume i in Seg n ; :: thesis: ex k being Element of NAT st
( k in Seg n & i = p . k )
then i in rng s by A1, FUNCT_2:def 3;
then ex k being Nat st
( k in dom s & i = s . k ) by FINSEQ_2:10;
hence ex k being Element of NAT st
( k in Seg n & i = p . k ) by A2; :: thesis: verum