let K be Field; :: thesis: for V1 being finite-dimensional VectSp of K
for F, F1 being FinSequence of V1
for KL being Linear_Combination of V1
for p being Permutation of (dom F) st F1 = F * p holds
KL (#) F1 = (KL (#) F) * p

let V1 be finite-dimensional VectSp of K; :: thesis: for F, F1 being FinSequence of V1
for KL being Linear_Combination of V1
for p being Permutation of (dom F) st F1 = F * p holds
KL (#) F1 = (KL (#) F) * p

let F, F1 be FinSequence of V1; :: thesis: for KL being Linear_Combination of V1
for p being Permutation of (dom F) st F1 = F * p holds
KL (#) F1 = (KL (#) F) * p

let KL be Linear_Combination of V1; :: thesis: for p being Permutation of (dom F) st F1 = F * p holds
KL (#) F1 = (KL (#) F) * p

let p be Permutation of (dom F); :: thesis: ( F1 = F * p implies KL (#) F1 = (KL (#) F) * p )
assume A1: F1 = F * p ; :: thesis: KL (#) F1 = (KL (#) F) * p
dom F = Seg (len F) by FINSEQ_1:def 3;
then dom F = Seg (len (KL (#) F)) by VECTSP_6:def 5;
then A2: dom F = dom (KL (#) F) by FINSEQ_1:def 3;
then reconsider F2 = (KL (#) F) * p as FinSequence of V1 by FINSEQ_2:47;
len (KL (#) F1) = len F1 by VECTSP_6:def 5
.= len F by
.= len (KL (#) F) by VECTSP_6:def 5
.= len F2 by ;
then A3: dom (KL (#) F1) = dom ((KL (#) F) * p) by FINSEQ_3:29;
len (KL (#) F1) = len F1 by VECTSP_6:def 5;
then A4: dom (KL (#) F1) = dom F1 by FINSEQ_3:29;
now :: thesis: for k being Nat st k in dom (KL (#) F1) holds
(KL (#) F1) . k = F2 . k
let k be Nat; :: thesis: ( k in dom (KL (#) F1) implies (KL (#) F1) . k = F2 . k )
reconsider k0 = k as Element of NAT by ORDINAL1:def 12;
assume A5: k in dom (KL (#) F1) ; :: thesis: (KL (#) F1) . k = F2 . k
then k in dom p by ;
then p . k in rng p by FUNCT_1:def 3;
then A6: p . k in dom F by FUNCT_2:def 3;
then reconsider k1 = p . k0 as Element of NAT by FINSEQ_3:23;
F1 /. k = F1 . k by
.= F . (p . k) by
.= F /. (p . k) by ;
hence (KL (#) F1) . k = (KL . (F /. k1)) * (F /. k1) by
.= (KL (#) F) . k1 by
.= F2 . k by ;
:: thesis: verum
end;
hence KL (#) F1 = (KL (#) F) * p by ; :: thesis: verum