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 A1, FINSEQ_2:44
.= len (KL (#) F) by VECTSP_6:def 5
.= len F2 by A2, FINSEQ_2:44 ;
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 A3, FUNCT_1:11;
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 A4, A5, PARTFUN1:def 6
.= F . (p . k) by A1, A4, A5, FUNCT_1:12
.= F /. (p . k) by A6, PARTFUN1:def 6 ;
hence (KL (#) F1) . k = (KL . (F /. k1)) * (F /. k1) by A5, VECTSP_6:def 5
.= (KL (#) F) . k1 by A2, A6, VECTSP_6:def 5
.= F2 . k by A3, A5, FUNCT_1:12 ;
:: thesis: verum

end;

hence KL (#) F1 = (KL (#) F) * p by A3, FINSEQ_1:13; :: thesis: verum