let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; :: thesis: for F, G being FinSequence of the carrier of V

for f being Permutation of (dom F) st G = F * f holds

Sum F = Sum G

let F, G be FinSequence of the carrier of V; :: thesis: for f being Permutation of (dom F) st G = F * f holds

Sum F = Sum G

let f be Permutation of (dom F); :: thesis: ( G = F * f implies Sum F = Sum G )

assume G = F * f ; :: thesis: Sum F = Sum G

then ( len F = len G & ( for i being Nat st i in dom G holds

G . i = F . (f . i) ) ) by FINSEQ_2:44, FUNCT_1:12;

hence Sum F = Sum G by Th6; :: thesis: verum

for f being Permutation of (dom F) st G = F * f holds

Sum F = Sum G

let F, G be FinSequence of the carrier of V; :: thesis: for f being Permutation of (dom F) st G = F * f holds

Sum F = Sum G

let f be Permutation of (dom F); :: thesis: ( G = F * f implies Sum F = Sum G )

assume G = F * f ; :: thesis: Sum F = Sum G

then ( len F = len G & ( for i being Nat st i in dom G holds

G . i = F . (f . i) ) ) by FINSEQ_2:44, FUNCT_1:12;

hence Sum F = Sum G by Th6; :: thesis: verum