let K be Ring; :: thesis: for n being Nat
for p being Element of Permutations n
for i being Nat st i in Seg n holds
p . i in Seg n
let n be Nat; :: thesis: for p being Element of Permutations n
for i being Nat st i in Seg n holds
p . i in Seg n
let p be Element of Permutations n; :: thesis: for i being Nat st i in Seg n holds
p . i in Seg n
let i be Nat; :: thesis: ( i in Seg n implies p . i in Seg n )
A1: p is Permutation of (Seg n) by MATRIX_1:def 12;
assume i in Seg n ; :: thesis: p . i in Seg n
hence p . i in Seg n by A1, FUNCT_2:5; :: thesis: verum