let X, Y be set ; :: thesis: for f1, f2, f3 being FinSequence of REAL st X \/ Y = dom f1 & X misses Y & f2 = f1 * (Sgm X) & f3 = f1 * (Sgm Y) holds
Sum f1 = (Sum f2) + (Sum f3)
let f1, f2, f3 be FinSequence of REAL ; :: thesis: ( X \/ Y = dom f1 & X misses Y & f2 = f1 * (Sgm X) & f3 = f1 * (Sgm Y) implies Sum f1 = (Sum f2) + (Sum f3) )
assume A1: X \/ Y = dom f1 ; :: thesis: ( not X misses Y or not f2 = f1 * (Sgm X) or not f3 = f1 * (Sgm Y) or Sum f1 = (Sum f2) + (Sum f3) )
assume A2: X misses Y ; :: thesis: ( not f2 = f1 * (Sgm X) or not f3 = f1 * (Sgm Y) or Sum f1 = (Sum f2) + (Sum f3) )
assume A3: f2 = f1 * (Sgm X) ; :: thesis: ( not f3 = f1 * (Sgm Y) or Sum f1 = (Sum f2) + (Sum f3) )
assume A4: f3 = f1 * (Sgm Y) ; :: thesis: Sum f1 = (Sum f2) + (Sum f3)

per cases ( dom f1 = {} or dom f1 <> {} ) ;

suppose A5: dom f1 = {} ; :: thesis: Sum f1 = (Sum f2) + (Sum f3)

then Y = {} by A1;
then A6: f3 = {} by A4, FINSEQ_3:43;
X = {} by A1, A5;
then f2 = {} by A3, FINSEQ_3:43;
hence Sum f1 = (Sum f2) + (Sum f3) by A5, A6, RELAT_1:41, RVSUM_1:72; :: thesis: verum

end;

suppose A7: dom f1 <> {} ; :: thesis: Sum f1 = (Sum f2) + (Sum f3)

A8: dom f1 = Seg (len f1) by FINSEQ_1:def 3;
then reconsider F = id (dom f1) as FinSequence by FINSEQ_2:48;
reconsider D = dom f1 as non empty set by A7;
reconsider F1 = f1 as FinSequence of ExtREAL by MESFUNC3:11;
A9: dom F1 = dom F ;
aa: Y c= dom f1 by A1, XBOOLE_1:7;
then Y is included_in_Seg by A8;
then rng (Sgm Y) c= dom f1 by aa, FINSEQ_1:def 14;
then reconsider sy = Sgm Y as FinSequence of D by FINSEQ_1:def 4;
(dom f1) \ X = Y by A1, A2, XBOOLE_1:88;
then (rng F) \ X = Y ;
then A10: F " ((rng F) \ X) = Y by FUNCT_2:94;
A11: X c= dom f1 by A1, XBOOLE_1:7;
then X is included_in_Seg by A8;
then rng (Sgm X) c= dom f1 by A11, FINSEQ_1:def 14;
then reconsider sx = Sgm X as FinSequence of D by FINSEQ_1:def 4;
F " X = X by A11, FUNCT_2:94;
then reconsider s = (Sgm X) ^ (Sgm Y) as Permutation of (dom F1) by A10, A9, FINSEQ_3:114;
rng s c= dom f1 by FUNCT_2:def 3;
then reconsider g = f1 * s as FinSequence of REAL by Th9;
reconsider f19 = f1 as Function of D,REAL by FINSEQ_2:26;
reconsider G = g as FinSequence of ExtREAL by MESFUNC3:11;
not -infty in rng F1 ;
then Sum F1 = Sum G by EXTREAL1:11;
then A12: Sum f1 = Sum G by MESFUNC3:2;
g = (f19 * sx) ^ (f19 * sy) by FINSEQOP:9;
then Sum g = (Sum (f19 * sx)) + (Sum (f19 * sy)) by RVSUM_1:75;
hence Sum f1 = (Sum f2) + (Sum f3) by A3, A4, A12, MESFUNC3:2; :: thesis: verum

end;

end;