let V be RealLinearSpace; for L being Linear_Combination of V
for F, G being FinSequence of the carrier of V
for P being Permutation of (dom F) st G = F * P holds
Sum (L (#) F) = Sum (L (#) G)
let L be Linear_Combination of V; for F, G being FinSequence of the carrier of V
for P being Permutation of (dom F) st G = F * P holds
Sum (L (#) F) = Sum (L (#) G)
let F, G be FinSequence of the carrier of V; for P being Permutation of (dom F) st G = F * P holds
Sum (L (#) F) = Sum (L (#) G)
set p = L (#) F;
set q = L (#) G;
let P be Permutation of (dom F); ( G = F * P implies Sum (L (#) F) = Sum (L (#) G) )
assume A1:
G = F * P
; Sum (L (#) F) = Sum (L (#) G)
A2:
len G = len F
by A1, FINSEQ_2:44;
len F = len (L (#) F)
by RLVECT_2:def 7;
then A3:
dom F = dom (L (#) F)
by FINSEQ_3:29;
then reconsider r = (L (#) F) * P as FinSequence of the carrier of V by FINSEQ_2:47;
len r = len (L (#) F)
by A3, FINSEQ_2:44;
then A4:
dom r = dom (L (#) F)
by FINSEQ_3:29;
A5:
len (L (#) F) = len F
by RLVECT_2:def 7;
then A6:
dom F = dom (L (#) F)
by FINSEQ_3:29;
len (L (#) G) = len G
by RLVECT_2:def 7;
then A7:
dom (L (#) F) = dom (L (#) G)
by A5, A2, FINSEQ_3:29;
A8:
dom F = dom G
by A2, FINSEQ_3:29;
A9:
now for k being Nat st k in dom (L (#) G) holds
(L (#) G) . k = r . klet k be
Nat;
( k in dom (L (#) G) implies (L (#) G) . k = r . k )assume A10:
k in dom (L (#) G)
;
(L (#) G) . k = r . kset l =
P . k;
(
dom P = dom F &
rng P = dom F )
by FUNCT_2:52, FUNCT_2:def 3;
then A11:
P . k in dom F
by A7, A6, A10, FUNCT_1:def 3;
then reconsider l =
P . k as
Element of
NAT ;
G /. k =
G . k
by A7, A8, A6, A10, PARTFUN1:def 6
.=
F . (P . k)
by A1, A7, A8, A6, A10, FUNCT_1:12
.=
F /. l
by A11, PARTFUN1:def 6
;
then (L (#) G) . k =
(L . (F /. l)) * (F /. l)
by A10, RLVECT_2:def 7
.=
(L (#) F) . (P . k)
by A6, A11, RLVECT_2:def 7
.=
r . k
by A7, A4, A10, FUNCT_1:12
;
hence
(L (#) G) . k = r . k
;
verum end;
thus Sum (L (#) F) =
Sum r
by A3, RLVECT_2:7
.=
Sum (L (#) G)
by A7, A4, A9, FINSEQ_1:13
; verum