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

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