let V1 be free finite-rank Z_Module; 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; 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; for p being Permutation of (dom F) st F1 = F * p holds
KL (#) F1 = (KL (#) F) * p
let p be Permutation of (dom F); ( F1 = F * p implies KL (#) F1 = (KL (#) F) * p )
assume A1:
F1 = F * p
; 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;
A31: 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 for k being Nat st k in dom (KL (#) F1) holds
(KL (#) F1) . k = F2 . klet k be
Nat;
( 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)
;
(KL (#) F1) . k = F2 . kthen
k in dom p
by A3, FUNCT_1:11;
then A6:
p . k in rng p
by FUNCT_1:def 3;
then
p . k in dom F
;
then reconsider k1 =
p . k0 as
Element of
NAT ;
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
;
verum end;
hence
KL (#) F1 = (KL (#) F) * p
by A31, FINSEQ_3:29; verum