let cF be complex-valued XFinSequence; :: thesis: for B1, B2 being set st B1 misses B2 holds

Sum (SubXFinS (cF,(B1 \/ B2))) = (Sum (SubXFinS (cF,B1))) + (Sum (SubXFinS (cF,B2)))

let B1, B2 be set ; :: thesis: ( B1 misses B2 implies Sum (SubXFinS (cF,(B1 \/ B2))) = (Sum (SubXFinS (cF,B1))) + (Sum (SubXFinS (cF,B2))) )

assume A1: B1 misses B2 ; :: thesis: Sum (SubXFinS (cF,(B1 \/ B2))) = (Sum (SubXFinS (cF,B1))) + (Sum (SubXFinS (cF,B2)))

set O = SubXFinS (cF,(B1 \/ B2));

rng (SubXFinS (cF,(B1 \/ B2))) c= COMPLEX by VALUED_0:def 1;

then reconsider O = SubXFinS (cF,(B1 \/ B2)) as XFinSequence of COMPLEX by RELAT_1:def 19;

consider P being Permutation of (dom O) such that

A2: O * P = (SubXFinS (cF,B1)) ^ (SubXFinS (cF,B2)) by A1, Th9;

Sum (O * P) = (Sum (SubXFinS (cF,B1))) + (Sum (SubXFinS (cF,B2))) by A2, AFINSQ_2:55;

hence Sum (SubXFinS (cF,(B1 \/ B2))) = (Sum (SubXFinS (cF,B1))) + (Sum (SubXFinS (cF,B2))) by AFINSQ_2:45; :: thesis: verum

Sum (SubXFinS (cF,(B1 \/ B2))) = (Sum (SubXFinS (cF,B1))) + (Sum (SubXFinS (cF,B2)))

let B1, B2 be set ; :: thesis: ( B1 misses B2 implies Sum (SubXFinS (cF,(B1 \/ B2))) = (Sum (SubXFinS (cF,B1))) + (Sum (SubXFinS (cF,B2))) )

assume A1: B1 misses B2 ; :: thesis: Sum (SubXFinS (cF,(B1 \/ B2))) = (Sum (SubXFinS (cF,B1))) + (Sum (SubXFinS (cF,B2)))

set O = SubXFinS (cF,(B1 \/ B2));

rng (SubXFinS (cF,(B1 \/ B2))) c= COMPLEX by VALUED_0:def 1;

then reconsider O = SubXFinS (cF,(B1 \/ B2)) as XFinSequence of COMPLEX by RELAT_1:def 19;

consider P being Permutation of (dom O) such that

A2: O * P = (SubXFinS (cF,B1)) ^ (SubXFinS (cF,B2)) by A1, Th9;

Sum (O * P) = (Sum (SubXFinS (cF,B1))) + (Sum (SubXFinS (cF,B2))) by A2, AFINSQ_2:55;

hence Sum (SubXFinS (cF,(B1 \/ B2))) = (Sum (SubXFinS (cF,B1))) + (Sum (SubXFinS (cF,B2))) by AFINSQ_2:45; :: thesis: verum