let I be non empty set ; :: thesis: for L being AbGroup
for x being the carrier of b₁ -valued ManySortedSet of I
for J, e being Element of Fin I st e = {} holds
( Sum (x,e) = 0. L & ( for e, f being Element of Fin I st e misses f holds
Sum (x,(e \/ f)) = (Sum (x,e)) + (Sum (x,f)) ) )
let L be AbGroup; :: thesis: for x being the carrier of L -valued ManySortedSet of I
for J, e being Element of Fin I st e = {} holds
( Sum (x,e) = 0. L & ( for e, f being Element of Fin I st e misses f holds
Sum (x,(e \/ f)) = (Sum (x,e)) + (Sum (x,f)) ) )
let x be the carrier of L -valued ManySortedSet of I; :: thesis: for J, e being Element of Fin I st e = {} holds
( Sum (x,e) = 0. L & ( for e, f being Element of Fin I st e misses f holds
Sum (x,(e \/ f)) = (Sum (x,e)) + (Sum (x,f)) ) )
let J be Element of Fin I; :: thesis: for e being Element of Fin I st e = {} holds
( Sum (x,e) = 0. L & ( for e, f being Element of Fin I st e misses f holds
Sum (x,(e \/ f)) = (Sum (x,e)) + (Sum (x,f)) ) )

A1: now :: thesis: for e being Element of Fin I st e = {} holds
Sum (x,e) = 0. L

let e be Element of Fin I; :: thesis: ( e = {} implies Sum (x,e) = 0. L )
assume A2: e = {} ; :: thesis: Sum (x,e) = 0. L
consider p being one-to-one FinSequence of I such that
A3: rng p = e and
A4: Sum (x,e) = the addF of L "**" (# (p,x)) by Def1;
p = {} by A3, A2;
then ( # (p,x) = {} & the addF of L is having_a_unity & len (# (p,x)) = 0 ) by FVSUM_1:8;
then Sum (x,e) = the_unity_wrt the addF of L by A4, FINSOP_1:def 1;
hence Sum (x,e) = 0. L by FVSUM_1:7; :: thesis: verum

end;

now :: thesis: for e, f being Element of Fin I st e misses f holds
Sum (x,(e \/ f)) = (Sum (x,e)) + (Sum (x,f))

let e, f be Element of Fin I; :: thesis: ( e misses f implies Sum (x,(e \/ f)) = (Sum (x,e)) + (Sum (x,f)) )
assume A5: e misses f ; :: thesis: Sum (x,(e \/ f)) = (Sum (x,e)) + (Sum (x,f))
consider pe being one-to-one FinSequence of I such that
A6: rng pe = e and
A7: Sum (x,e) = the addF of L "**" (# (pe,x)) by Def1;
consider pf being one-to-one FinSequence of I such that
A8: rng pf = f and
A9: Sum (x,f) = the addF of L "**" (# (pf,x)) by Def1;
reconsider pepf = pe ^ pf as one-to-one FinSequence of I by A5, A6, A8, FINSEQ_3:91;
A10: # (pepf,x) = (# (pe,x)) ^ (# (pf,x)) by Th3;
rng pepf = e \/ f by A6, A8, FINSEQ_1:31;
then Sum (x,(e \/ f)) = the addF of L "**" (# (pepf,x)) by Def1;
hence Sum (x,(e \/ f)) = (Sum (x,e)) + (Sum (x,f)) by A7, A9, A10, FINSOP_1:5, FVSUM_1:8; :: thesis: verum

end;

hence for e being Element of Fin I st e = {} holds
( Sum (x,e) = 0. L & ( for e, f being Element of Fin I st e misses f holds
Sum (x,(e \/ f)) = (Sum (x,e)) + (Sum (x,f)) ) ) by A1; :: thesis: verum