let R be Ring; for V being RightMod of R
for S, T being finite Subset of V st T misses S holds
Sum (T \/ S) = (Sum T) + (Sum S)
let V be RightMod of R; for S, T being finite Subset of V st T misses S holds
Sum (T \/ S) = (Sum T) + (Sum S)
let S, T be finite Subset of V; ( T misses S implies Sum (T \/ S) = (Sum T) + (Sum S) )
consider F being FinSequence of V such that
A1:
rng F = T \/ S
and
A2:
( F is one-to-one & Sum (T \/ S) = Sum F )
by Def1;
consider G being FinSequence of V such that
A3:
rng G = T
and
A4:
G is one-to-one
and
A5:
Sum T = Sum G
by Def1;
consider H being FinSequence of V such that
A6:
rng H = S
and
A7:
H is one-to-one
and
A8:
Sum S = Sum H
by Def1;
set I = G ^ H;
assume
T misses S
; Sum (T \/ S) = (Sum T) + (Sum S)
then A9:
G ^ H is one-to-one
by A3, A4, A6, A7, FINSEQ_3:91;
rng (G ^ H) = rng F
by A1, A3, A6, FINSEQ_1:31;
hence Sum (T \/ S) =
Sum (G ^ H)
by A2, A9, RLVECT_1:42
.=
(Sum T) + (Sum S)
by A5, A8, RLVECT_1:41
;
verum