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)

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 <> {} )
;

end;

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;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

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 ;

Y c= dom f1 by A1, XBOOLE_1:7;

then rng (Sgm Y) c= dom f1 by A8, FINSEQ_1:def 13;

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 rng (Sgm X) c= dom f1 by A8, FINSEQ_1:def 13;

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;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 ;

Y c= dom f1 by A1, XBOOLE_1:7;

then rng (Sgm Y) c= dom f1 by A8, FINSEQ_1:def 13;

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 rng (Sgm X) c= dom f1 by A8, FINSEQ_1:def 13;

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