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));
reconsider O = SubXFinS (cF,(B1 \/ B2)) as XFinSequence of COMPLEX ;
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