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 A6:
dom f1 <> {}
;
:: thesis: Sum f1 = (Sum f2) + (Sum f3)reconsider F1 =
f1 as
FinSequence of
ExtREAL by MESFUNC3:11;
A7:
dom f1 = Seg (len f1)
by FINSEQ_1:def 3;
then reconsider F =
id (dom f1) as
FinSequence by FINSEQ_2:52;
(dom f1) \ X = Y
by A1, A2, XBOOLE_1:88;
then A8:
(rng F) \ X = Y
by RELAT_1:71;
A9:
X c= dom f1
by A1, XBOOLE_1:7;
then A10:
F " X = X
by FUNCT_2:171;
A11:
Y c= dom f1
by A1, XBOOLE_1:7;
then A12:
F " ((rng F) \ X) = Y
by A8, FUNCT_2:171;
dom F1 = dom F
by RELAT_1:71;
then reconsider s =
(Sgm X) ^ (Sgm Y) as
Permutation of
(dom F1) by A10, A12, FINSEQ_3:123;
rng s c= dom f1
by FUNCT_2:def 3;
then reconsider g =
f1 * s as
FinSequence of
REAL by Th9;
reconsider G =
g as
FinSequence of
ExtREAL by MESFUNC3:11;
not
-infty in rng F1
;
then
Sum F1 = Sum G
by CONVFUN1:8;
then A13:
Sum f1 = Sum G
by MESFUNC3:2;
reconsider D =
dom f1 as non
empty set by A6;
rng (Sgm Y) c= dom f1
by A7, A11, FINSEQ_1:def 13;
then reconsider sy =
Sgm Y as
FinSequence of
D by FINSEQ_1:def 4;
rng (Sgm X) c= dom f1
by A7, A9, FINSEQ_1:def 13;
then reconsider sx =
Sgm X as
FinSequence of
D by FINSEQ_1:def 4;
reconsider f1' =
f1 as
Function of
D,
REAL by FINSEQ_2:30;
g = (f1' * sx) ^ (f1' * sy)
by FINSEQOP:10;
then
Sum g = (Sum (f1' * sx)) + (Sum (f1' * sy))
by RVSUM_1:105;
hence
Sum f1 = (Sum f2) + (Sum f3)
by A13, A3, A4, MESFUNC3:2;
:: thesis: verum end;