let n be Nat; :: thesis: for K being Ring
for p being Element of Permutations n
for f being FinSequence of K st n >= 1 & len f = n holds
f * p is FinSequence of K
let K be Ring; :: thesis: for p being Element of Permutations n
for f being FinSequence of K st n >= 1 & len f = n holds
f * p is FinSequence of K
let p be Element of Permutations n; :: thesis: for f being FinSequence of K st n >= 1 & len f = n holds
f * p is FinSequence of K
let f be FinSequence of K; :: thesis: ( n >= 1 & len f = n implies f * p is FinSequence of K )
assume that
A1: n >= 1 and
A2: len f = n ; :: thesis: f * p is FinSequence of K
reconsider q = p as Function of (Seg n),(Seg n) by MATRIX_1:def 12;
p is bijective Function of (Seg n),(Seg n) by MATRIX_1:def 12;
then rng q = Seg n by FUNCT_2:def 3;
then rng p c= dom f by A2, FINSEQ_1:def 3;
then dom (f * p) = dom q by RELAT_1:27
.= Seg n by A1, FUNCT_2:def 1 ;
then reconsider h = f * p as FinSequence by FINSEQ_1:def 2;
( rng h c= rng f & rng f c= the carrier of K ) by FINSEQ_1:def 4, RELAT_1:26;
then rng h c= the carrier of K ;
hence f * p is FinSequence of K by FINSEQ_1:def 4; :: thesis: verum