let V be Z_Module; :: thesis: for L being Linear_Combination of V

for F, G being FinSequence 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; :: thesis: for F, G being FinSequence 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 V; :: thesis: 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); :: thesis: ( G = F * P implies Sum (L (#) F) = Sum (L (#) G) )

assume A1: G = F * P ; :: thesis: Sum (L (#) F) = Sum (L (#) G)

A2: len G = len F by A1, FINSEQ_2:44;

len F = len (L (#) F) by VECTSP_6:def 5;

then A3: dom F = dom (L (#) F) by FINSEQ_3:29;

then reconsider r = (L (#) F) * P as FinSequence 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 VECTSP_6:def 5;

then A6: dom F = dom (L (#) F) by FINSEQ_3:29;

len (L (#) G) = len G by VECTSP_6:def 5;

then A7: dom (L (#) F) = dom (L (#) G) by A1, A5, FINSEQ_2:44, FINSEQ_3:29;

A8: dom F = dom G by A2, FINSEQ_3:29;

for F, G being FinSequence 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; :: thesis: for F, G being FinSequence 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 V; :: thesis: 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); :: thesis: ( G = F * P implies Sum (L (#) F) = Sum (L (#) G) )

assume A1: G = F * P ; :: thesis: Sum (L (#) F) = Sum (L (#) G)

A2: len G = len F by A1, FINSEQ_2:44;

len F = len (L (#) F) by VECTSP_6:def 5;

then A3: dom F = dom (L (#) F) by FINSEQ_3:29;

then reconsider r = (L (#) F) * P as FinSequence 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 VECTSP_6:def 5;

then A6: dom F = dom (L (#) F) by FINSEQ_3:29;

len (L (#) G) = len G by VECTSP_6:def 5;

then A7: dom (L (#) F) = dom (L (#) G) by A1, A5, FINSEQ_2:44, FINSEQ_3:29;

A8: dom F = dom G by A2, FINSEQ_3:29;

now :: thesis: for k being Nat st k in dom (L (#) G) holds

(L (#) G) . k = r . k

hence
Sum (L (#) F) = Sum (L (#) G)
by A3, A4, A7, FINSEQ_1:13, RLVECT_2:7; :: thesis: verum(L (#) G) . k = r . k

let k be Nat; :: thesis: ( k in dom (L (#) G) implies (L (#) G) . k = r . k )

assume A9: k in dom (L (#) G) ; :: thesis: (L (#) G) . k = r . k

set l = P . k;

( dom P = dom F & rng P = dom F ) by FUNCT_2:52, FUNCT_2:def 3;

then A10: P . k in dom F by A7, A6, A9, FUNCT_1:def 3;

then reconsider l = P . k as Element of NAT ;

G /. k = G . k by A7, A8, A6, A9, PARTFUN1:def 6

.= F . (P . k) by A1, A7, A8, A6, A9, FUNCT_1:12

.= F /. l by A10, PARTFUN1:def 6 ;

then (L (#) G) . k = (L . (F /. l)) * (F /. l) by A9, VECTSP_6:def 5

.= (L (#) F) . (P . k) by A6, A10, VECTSP_6:def 5

.= r . k by A7, A4, A9, FUNCT_1:12 ;

hence (L (#) G) . k = r . k ; :: thesis: verum

end;assume A9: k in dom (L (#) G) ; :: thesis: (L (#) G) . k = r . k

set l = P . k;

( dom P = dom F & rng P = dom F ) by FUNCT_2:52, FUNCT_2:def 3;

then A10: P . k in dom F by A7, A6, A9, FUNCT_1:def 3;

then reconsider l = P . k as Element of NAT ;

G /. k = G . k by A7, A8, A6, A9, PARTFUN1:def 6

.= F . (P . k) by A1, A7, A8, A6, A9, FUNCT_1:12

.= F /. l by A10, PARTFUN1:def 6 ;

then (L (#) G) . k = (L . (F /. l)) * (F /. l) by A9, VECTSP_6:def 5

.= (L (#) F) . (P . k) by A6, A10, VECTSP_6:def 5

.= r . k by A7, A4, A9, FUNCT_1:12 ;

hence (L (#) G) . k = r . k ; :: thesis: verum