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