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