let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; :: thesis: for F, G being FinSequence of the carrier of V st len F = len G & ( for k being Nat st k in dom F holds
G . k = - (F /. k) ) holds
Sum G = - (Sum F)

let F, G be FinSequence of the carrier of V; :: thesis: ( len F = len G & ( for k being Nat st k in dom F holds
G . k = - (F /. k) ) implies Sum G = - (Sum F) )

assume that
A1: len F = len G and
A2: for k being Nat st k in dom F holds
G . k = - (F /. k) ; :: thesis: Sum G = - (Sum F)
now :: thesis: for k being Nat
for v being Element of V st k in dom G & v = F . k holds
G . k = - v
let k be Nat; :: thesis: for v being Element of V st k in dom G & v = F . k holds
G . k = - v

let v be Element of V; :: thesis: ( k in dom G & v = F . k implies G . k = - v )
assume that
A3: k in dom G and
A4: v = F . k ; :: thesis: G . k = - v
A5: ( dom G = Seg (len G) & dom F = Seg (len F) ) by FINSEQ_1:def 3;
then v = F /. k by ;
hence G . k = - v by A1, A2, A3, A5; :: thesis: verum
end;
hence Sum G = - (Sum F) by ; :: thesis: verum