let cF be complex-valued XFinSequence; :: thesis: for B1, B2 being natural-membered finite set st B1 <N< B2 holds
Sum (SubXFinS cF,(B1 \/ B2)) = (Sum (SubXFinS cF,B1)) + (Sum (SubXFinS cF,B2))
let B1, B2 be natural-membered finite 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);
A2: (B1 /\ (len cF)) \/ (B2 /\ (len cF)) = (B1 \/ B2) /\ (len cF) by XBOOLE_1:23;
B1 /\ (len cF) <N< B2 /\ (len cF) by A1, Th36;
then A3: Sgm0 ((B1 \/ B2) /\ (len cF)) = (Sgm0 (B1 /\ (len cF))) ^ (Sgm0 (B2 /\ (len cF))) by Th46, A2;
( rng (Sgm0 (B1 /\ (len cF))) = B1 /\ (len cF) & rng (Sgm0 (B2 /\ (len cF))) = B2 /\ (len cF) ) by Def5;
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, Th79;
hence Sum (SubXFinS cF,(B1 \/ B2)) = (Sum (SubXFinS cF,B1)) + (Sum (SubXFinS cF,B2)) by Th65; :: thesis: verum