let R be Ring; :: thesis: for V being RightMod of R
for T, S 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 T, S being finite Subset of V st T misses S holds
Sum (T \/ S) = (Sum T) + (Sum S)
let T, S be finite Subset of V; :: thesis: ( T misses S implies Sum (T \/ S) = (Sum T) + (Sum S) )
assume A1: T misses S ; :: thesis: Sum (T \/ S) = (Sum T) + (Sum S)
consider F being FinSequence of V such that
A2: rng F = T \/ S and
A3: ( F is one-to-one & Sum (T \/ S) = Sum F ) by Def3;
consider G being FinSequence of V such that
A4: ( rng G = T & G is one-to-one ) and
A5: Sum T = Sum G by Def3;
consider H being FinSequence of V such that
A6: ( rng H = S & H is one-to-one ) and
A7: Sum S = Sum H by Def3;
set I = G ^ H;
A8: rng (G ^ H) = rng F by A2, A4, A6, FINSEQ_1:44;
G ^ H is one-to-one by A1, A4, A6, FINSEQ_3:98;
hence Sum (T \/ S) = Sum (G ^ H) by A3, A8, RLVECT_1:59
.= (Sum T) + (Sum S) by A5, A7, RLVECT_1:58 ;
:: thesis: verum