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;

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

hence
KL (#) F1 = (KL (#) F) * p
by A3, FINSEQ_1:13; :: thesis: verum(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;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