let A be non empty set ; :: thesis:
let D be non empty a_partition of A; :: thesis:
let f be finite-support Function of A,REAL; :: thesis:
let s1 be one-to-one FinSequence of A; :: thesis:
let s2 be one-to-one FinSequence of D; :: thesis:
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 ; :: thesis:
defpred S₁[ 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: S₁[ 0 ]

proof

let t1 be one-to-one FinSequence of A; :: thesis:
let t2 be one-to-one FinSequence of D; :: thesis:
assume that
A4: rng t2 = (proj D) .: (rng t1) and
for X being Element of D st X in rng t2 holds
eqSupport (f,X) c= rng t1 ; :: thesis:
assume len t2 = 0 ; :: thesis:
then A5: t2 = <*> D ;
dom (proj D) = A by FUNCT_2:def 1;
then rng t1 c= dom (proj D) by FINSEQ_1:def 4;
then A6: t1 = <*> A by A5, A4;
thus Sum ((D eqSumOf f) * t2) = Sum (f * t1) by A5, A6; :: thesis:

end;

A7: for j being Nat st S₁[j] holds
S₁[j + 1]

proof

let j be Nat; :: thesis:
assume A8: S₁[j] ; :: thesis:
let t1 be one-to-one FinSequence of A; :: thesis:
let t2 be one-to-one FinSequence of D; :: thesis:
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 ; :: thesis:
assume A11: len t2 = j + 1 ; :: thesis:
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)

proof

for x being object st x in rng r2 holds
x in (proj D) .: (rng r1)

proof

let x be object ; :: thesis:
assume A17: x in rng r2 ; :: thesis:
then x in rng t2 by A12, FINSEQ_1:29, TARSKI:def 3;
then consider w being object such that
A18: w in dom (proj D) and
A19: w in rng t1 and
A20: x = (proj D) . w by A9, FUNCT_1:def 6;
not w in (proj D) " {X}

proof

assume w in (proj D) " {X} ; :: thesis:
then (proj D) . w in {X} by FUNCT_1:def 7;
then X in rng r2 by A20, A17, TARSKI:def 1;
hence contradiction by A13; :: thesis:

end;

then w in (rng t1) \ ((proj D) " {X}) by A19, XBOOLE_0:def 5;
then w in rng r1 by FINSEQ_3:65;
hence x in (proj D) .: (rng r1) by A18, A20, FUNCT_1:def 6; :: thesis:

end;

hence rng r2 c= (proj D) .: (rng r1) ; :: according to XBOOLE_0:def 10 :: thesis:
for x being object st x in (proj D) .: (rng r1) holds
x in rng r2

proof

let x be object ; :: thesis:
assume A21: x in (proj D) .: (rng r1) ; :: thesis:
then consider w being object such that
A22: w in dom (proj D) and
A23: w in rng r1 and
A24: x = (proj D) . w by FUNCT_1:def 6;
w in (rng t1) \ ((proj D) " {X}) by A23, FINSEQ_3:65;
then not w in (proj D) " {X} by XBOOLE_0:def 5;
then not x in {X} by A22, A24, FUNCT_1:def 7;
then A25: not x in rng <*X*> by FINSEQ_1:38;
x in (proj D) .: (rng t1) by A15, A21, RELAT_1:123, TARSKI:def 3;
then x in (rng r2) \/ (rng <*X*>) by A9, A12, FINSEQ_1:31;
hence x in rng r2 by A25, XBOOLE_0:def 3; :: thesis:

end;

hence (proj D) .: (rng r1) c= rng r2 ; :: thesis:

end;

for Y being Element of D st Y in rng r2 holds
eqSupport (f,Y) c= rng r1

proof

let Y be Element of D; :: thesis:
assume A26: Y in rng r2 ; :: thesis:
for x being object st x in eqSupport (f,Y) holds
x in rng r1

proof

let x be object ; :: thesis:
assume A27: x in eqSupport (f,Y) ; :: thesis:
rng r2 c= rng t2 by A12, FINSEQ_1:29;
then eqSupport (f,Y) c= rng t1 by A10, A26;
then A28: x in rng t1 by A27;
not x in (proj D) " {X}

proof

assume x in (proj D) " {X} ; :: thesis:
then A29: ( x in dom (proj D) & (proj D) . x in {X} ) by FUNCT_1:def 7;
then reconsider y = x as Element of A ;
y in Y by A27, XBOOLE_0:def 4;
then (proj D) . y = Y by EQREL_1:65;
then X in rng r2 by A26, A29, TARSKI:def 1;
hence contradiction by A13; :: thesis:

end;

then x in (rng t1) \ ((proj D) " {X}) by A28, XBOOLE_0:def 5;
hence x in rng r1 by FINSEQ_3:65; :: thesis:

end;

hence eqSupport (f,Y) c= rng r1 ; :: thesis:

end;

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

proof

given x being object such that A31: x in (rng r1) /\ (rng (canFS (eqSupport (f,X)))) ; :: thesis:
x in rng (canFS (eqSupport (f,X))) by A31, XBOOLE_0:def 4;
then A32: x in eqSupport (f,X) by FUNCT_2:def 3;
then reconsider y = x as Element of A ;
y in X by A32, XBOOLE_0:def 4;
then A33: (proj D) . y = X by EQREL_1:65;
A34: x in rng r1 by A31, XBOOLE_0:def 4;
then x in A by FINSEQ_1:def 4, TARSKI:def 3;
then x in dom (proj D) by FUNCT_2:def 1;
then (proj D) . x in (proj D) .: (rng r1) by A34, FUNCT_1:def 6;
then X in rng r2 by A33, A16;
hence contradiction by A13; :: thesis:

end;

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

proof

let x be object ; :: thesis:
assume x in rng qt1 ; :: thesis:
then x in (rng r1) \/ (rng canEq) by FINSEQ_1:31;

per cases by XBOOLE_0:def 3;

suppose x in rng r1 ; :: thesis:

then x in (rng t1) \ ((proj D) " {X}) by FINSEQ_3:65;
hence x in rng t1 ; :: thesis:

end;

suppose x in rng (canFS (eqSupport (f,X))) ; :: thesis:

then A35: x in eqSupport (f,X) by FUNCT_2:def 3;
rng <*X*> = {X} by FINSEQ_1:39;
then X in rng <*X*> by TARSKI:def 1;
then X in (rng r2) \/ (rng <*X*>) by XBOOLE_0:def 3;
then X in rng t2 by A12, FINSEQ_1:31;
then eqSupport (f,X) c= rng t1 by A10;
hence x in rng t1 by A35; :: thesis:

end;

then A36: rng qt1 c= rng t1 ;
for x being Element of A st x in (rng t1) \ (rng qt1) holds
f . x = 0

proof

let x be Element of A; :: thesis:
assume x in (rng t1) \ (rng qt1) ; :: thesis:
then A37: ( x in rng t1 & not x in rng qt1 ) by XBOOLE_0:def 5;
then not x in (rng r1) \/ (rng canEq) by FINSEQ_1:31;
then A38: ( not x in rng r1 & not x in rng (canFS (eqSupport (f,X))) ) by XBOOLE_0:def 3;
then not x in eqSupport (f,X) by FUNCT_2:def 3;

per cases by XBOOLE_0:def 4;

suppose not x in support f ; :: thesis:

hence f . x = 0 by PRE_POLY:def 7; :: thesis:

end;

suppose A39: not x in X ; :: thesis:

not x in (rng t1) \ ((proj D) " {X}) by A38, FINSEQ_3:65;
then A40: x in (proj D) " {X} by A37, XBOOLE_0:def 5;
x in A ;
then x in dom (proj D) by FUNCT_2:def 1;
then (proj D) . x in (proj D) .: ((proj D) " {X}) by A40, FUNCT_1:def 6;
then (proj D) . x in {X} by FUNCT_1:75, TARSKI:def 3;
then (proj D) . x = X by TARSKI:def 1;
hence f . x = 0 by A39, EQREL_1:def 9; :: thesis:

end;

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

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A3, A7);
then S₁[ len s2] ;
hence Sum ((D eqSumOf f) * s2) = Sum (f * s1) by A1, A2; :: thesis: