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 )
p is Permutation of (Seg n) by MATRIX_1:def 16;
hence ( i in Seg n implies p . i in Seg n ) by FUNCT_2:5; :: thesis: verum