let R be Ring; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 ;
:: thesis: verum