let I be non empty set ; :: thesis: for L being AbGroup

for x being the carrier of b_{1} -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)) ) )

( 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

for x being the carrier of b

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

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;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

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))

hence
for e being Element of Fin I st e = {} 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;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

( 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