let A be non empty set ; for D being non empty a_partition of A
for f being finite-support Function of A,REAL
for s1 being one-to-one FinSequence of A
for s2 being one-to-one FinSequence of D st rng s2 = (proj D) .: (rng s1) & ( for X being Element of D st X in rng s2 holds
eqSupport (f,X) c= rng s1 ) holds
Sum ((D eqSumOf f) * s2) = Sum (f * s1)
let D be non empty a_partition of A; for f being finite-support Function of A,REAL
for s1 being one-to-one FinSequence of A
for s2 being one-to-one FinSequence of D st rng s2 = (proj D) .: (rng s1) & ( for X being Element of D st X in rng s2 holds
eqSupport (f,X) c= rng s1 ) holds
Sum ((D eqSumOf f) * s2) = Sum (f * s1)
let f be finite-support Function of A,REAL; for s1 being one-to-one FinSequence of A
for s2 being one-to-one FinSequence of D st rng s2 = (proj D) .: (rng s1) & ( for X being Element of D st X in rng s2 holds
eqSupport (f,X) c= rng s1 ) holds
Sum ((D eqSumOf f) * s2) = Sum (f * s1)
let s1 be one-to-one FinSequence of A; for s2 being one-to-one FinSequence of D st rng s2 = (proj D) .: (rng s1) & ( for X being Element of D st X in rng s2 holds
eqSupport (f,X) c= rng s1 ) holds
Sum ((D eqSumOf f) * s2) = Sum (f * s1)
let s2 be one-to-one FinSequence of D; ( rng s2 = (proj D) .: (rng s1) & ( for X being Element of D st X in rng s2 holds
eqSupport (f,X) c= rng s1 ) implies Sum ((D eqSumOf f) * s2) = Sum (f * s1) )
assume that
A1:
rng s2 = (proj D) .: (rng s1)
and
A2:
for X being Element of D st X in rng s2 holds
eqSupport (f,X) c= rng s1
; Sum ((D eqSumOf f) * s2) = Sum (f * s1)
defpred S1[ Nat] means for t1 being one-to-one FinSequence of A
for t2 being one-to-one FinSequence of D st rng t2 = (proj D) .: (rng t1) & ( for X being Element of D st X in rng t2 holds
eqSupport (f,X) c= rng t1 ) & len t2 = $1 holds
Sum ((D eqSumOf f) * t2) = Sum (f * t1);
A3:
S1[ 0 ]
A7:
for j being Nat st S1[j] holds
S1[j + 1]
proof
let j be
Nat;
( S1[j] implies S1[j + 1] )
assume A8:
S1[
j]
;
S1[j + 1]
let t1 be
one-to-one FinSequence of
A;
for t2 being one-to-one FinSequence of D st rng t2 = (proj D) .: (rng t1) & ( for X being Element of D st X in rng t2 holds
eqSupport (f,X) c= rng t1 ) & len t2 = j + 1 holds
Sum ((D eqSumOf f) * t2) = Sum (f * t1)let t2 be
one-to-one FinSequence of
D;
( rng t2 = (proj D) .: (rng t1) & ( for X being Element of D st X in rng t2 holds
eqSupport (f,X) c= rng t1 ) & len t2 = j + 1 implies Sum ((D eqSumOf f) * t2) = Sum (f * t1) )
assume that A9:
rng t2 = (proj D) .: (rng t1)
and A10:
for
X being
Element of
D st
X in rng t2 holds
eqSupport (
f,
X)
c= rng t1
;
( not len t2 = j + 1 or Sum ((D eqSumOf f) * t2) = Sum (f * t1) )
assume A11:
len t2 = j + 1
;
Sum ((D eqSumOf f) * t2) = Sum (f * t1)
then consider r2 being
FinSequence of
D,
X being
Element of
D such that A12:
t2 = r2 ^ <*X*>
by FINSEQ_2:19;
rng <*X*> = {X}
by FINSEQ_1:38;
then
rng r2 misses {X}
by A12, FINSEQ_3:91;
then A13:
not
X in rng r2
by ZFMISC_1:48;
1
+ (len r2) = j + 1
by A12, A11, FINSEQ_2:16;
then A14:
len r2 = j
;
reconsider r2 =
r2 as
one-to-one FinSequence of
D by A12, FINSEQ_3:91;
set r1 =
t1 - ((proj D) " {X});
A15:
rng (t1 - ((proj D) " {X})) c= rng t1
by FINSEQ_3:66;
rng t1 c= A
by FINSEQ_1:def 4;
then
rng (t1 - ((proj D) " {X})) c= A
by A15;
then reconsider r1 =
t1 - ((proj D) " {X}) as
FinSequence of
A by FINSEQ_1:def 4;
reconsider r1 =
r1 as
one-to-one FinSequence of
A by FINSEQ_3:87;
A16:
rng r2 = (proj D) .: (rng r1)
for
Y being
Element of
D st
Y in rng r2 holds
eqSupport (
f,
Y)
c= rng r1
then A30:
Sum ((D eqSumOf f) * r2) = Sum (f * r1)
by A16, A14, A8;
reconsider canEq =
canFS (eqSupport (f,X)) as
FinSequence of
A by FINSEQ_2:24;
reconsider qt1 =
r1 ^ canEq as
FinSequence of
A ;
for
x being
object holds not
x in (rng r1) /\ (rng (canFS (eqSupport (f,X))))
then
rng r1 misses rng canEq
by XBOOLE_0:def 1;
then reconsider qt1 =
qt1 as
one-to-one FinSequence of
A by FINSEQ_3:91;
for
x being
object st
x in rng qt1 holds
x in rng t1
then A36:
rng qt1 c= rng t1
;
for
x being
Element of
A st
x in (rng t1) \ (rng qt1) holds
f . x = 0
then A41:
Sum (f * qt1) = Sum (f * t1)
by A36, Th9;
thus Sum ((D eqSumOf f) * t2) =
Sum (((D eqSumOf f) * r2) ^ <*((D eqSumOf f) . X)*>)
by A12, FINSEQOP:8
.=
(Sum (f * r1)) + ((D eqSumOf f) . X)
by RVSUM_1:74, A30
.=
(Sum (f * r1)) + (Sum (f * (canFS (eqSupport (f,X)))))
by Def14
.=
Sum ((f * r1) ^ (f * canEq))
by RVSUM_1:75
.=
Sum (f * t1)
by A41, FINSEQOP:9
;
verum
end;
for i being Nat holds S1[i]
from NAT_1:sch 2(A3, A7);
then
S1[ len s2]
;
hence
Sum ((D eqSumOf f) * s2) = Sum (f * s1)
by A1, A2; verum