let K be Field; :: thesis: for n being Element of NAT
for p being Element of Permutations n
for i being Element of NAT st i in Seg n holds
p . i in Seg n
let n be Element of NAT ; :: thesis: for p being Element of Permutations n
for i being Element of NAT st i in Seg n holds
p . i in Seg n
let p be Element of Permutations n; :: thesis: for i being Element of NAT st i in Seg n holds
p . i in Seg n
let i be Element of NAT ; :: thesis: ( i in Seg n implies p . i in Seg n )
assume A1: i in Seg n ; :: thesis: p . i in Seg n
p is Permutation of (Seg n) by MATRIX_2:def 11;
hence p . i in Seg n by A1, FUNCT_2:7; :: thesis: verum