let V be non empty Abelian add-associative right_zeroed addLoopStr ; :: 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 the carrier of V such that

A1: rng F = T \/ S and

A2: ( F is one-to-one & Sum (T \/ S) = Sum F ) by Def2;

consider G being FinSequence of the carrier of V such that

A3: rng G = T and

A4: G is one-to-one and

A5: Sum T = Sum G by Def2;

consider H being FinSequence of the carrier of V such that

A6: rng H = S and

A7: H is one-to-one and

A8: Sum S = Sum H by Def2;

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

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 the carrier of V such that

A1: rng F = T \/ S and

A2: ( F is one-to-one & Sum (T \/ S) = Sum F ) by Def2;

consider G being FinSequence of the carrier of V such that

A3: rng G = T and

A4: G is one-to-one and

A5: Sum T = Sum G by Def2;

consider H being FinSequence of the carrier of V such that

A6: rng H = S and

A7: H is one-to-one and

A8: Sum S = Sum H by Def2;

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