let n be Element of NAT ; :: thesis: for K being Field
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 Field; :: 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 A1: ( n >= 1 & len f = n ) ; :: thesis: f * p is FinSequence of K
A2: Seg n <> {} by A1;
A3: p is bijective Function of (Seg n),(Seg n) by MATRIX_2:def 11;
reconsider q = p as Function of (Seg n),(Seg n) by MATRIX_2:def 11;
rng q = Seg n by A3, FUNCT_2:def 3;
then rng p c= dom f by A1, FINSEQ_1:def 3;
then dom (f * p) = dom q by RELAT_1:46
.= Seg n by A2, FUNCT_2:def 1 ;
then reconsider h = f * p as FinSequence by FINSEQ_1:def 2;
A4: rng h c= rng f by RELAT_1:45;
rng f c= the carrier of K by FINSEQ_1:def 4;
then rng h c= the carrier of K by A4, XBOOLE_1:1;
hence f * p is FinSequence of K by FINSEQ_1:def 4; :: thesis: verum