let cF be complex-valued XFinSequence; :: thesis: for B1, B2 being finite natural-membered set st B1 <N< B2 holds
Sum (SubXFinS (cF,(B1 \/ B2))) = (Sum (SubXFinS (cF,B1))) + (Sum (SubXFinS (cF,B2)))
let B1, B2 be finite natural-membered set ; :: thesis: ( B1 <N< B2 implies Sum (SubXFinS (cF,(B1 \/ B2))) = (Sum (SubXFinS (cF,B1))) + (Sum (SubXFinS (cF,B2))) )
assume A1: B1 <N< B2 ; :: thesis: Sum (SubXFinS (cF,(B1 \/ B2))) = (Sum (SubXFinS (cF,B1))) + (Sum (SubXFinS (cF,B2)))
set B12 = B1 \/ B2;
set B12L = (B1 \/ B2) /\ (len cF);
set B1L = B1 /\ (len cF);
set B2L = B2 /\ (len cF);
(B1 /\ (len cF)) \/ (B2 /\ (len cF)) = (B1 \/ B2) /\ (len cF) by XBOOLE_1:23;
then A3: Sgm0 ((B1 \/ B2) /\ (len cF)) = (Sgm0 (B1 /\ (len cF))) ^ (Sgm0 (B2 /\ (len cF))) by Th35, A1, Th25;
( rng (Sgm0 (B1 /\ (len cF))) = B1 /\ (len cF) & rng (Sgm0 (B2 /\ (len cF))) = B2 /\ (len cF) ) by Def4;
then ( rng (Sgm0 (B1 /\ (len cF))) c= dom cF & rng (Sgm0 (B2 /\ (len cF))) c= dom cF ) by XBOOLE_1:17;
then (SubXFinS (cF,B1)) ^ (SubXFinS (cF,B2)) = SubXFinS (cF,(B1 \/ B2)) by A3, Th69;
hence Sum (SubXFinS (cF,(B1 \/ B2))) = (Sum (SubXFinS (cF,B1))) + (Sum (SubXFinS (cF,B2))) by Th54; :: thesis: verum