let A be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: Sum ((D eqSumOf f) * s2) = Sum (f * s1)

defpred S_{1}[ 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_{1}[ 0 ]
_{1}[j] holds

S_{1}[j + 1]
_{1}[i]
from NAT_1:sch 2(A3, A7);

then S_{1}[ len s2]
;

hence Sum ((D eqSumOf f) * s2) = Sum (f * s1) by A1, A2; :: thesis: verum

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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: Sum ((D eqSumOf f) * s2) = Sum (f * s1)

defpred S

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

proof

A7:
for j being Nat st S
let t1 be one-to-one FinSequence of A; :: thesis: 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 = 0 holds

Sum ((D eqSumOf f) * t2) = Sum (f * t1)

let t2 be one-to-one FinSequence of D; :: thesis: ( 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 = 0 implies Sum ((D eqSumOf f) * t2) = Sum (f * t1) )

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: ( not len t2 = 0 or Sum ((D eqSumOf f) * t2) = Sum (f * t1) )

assume len t2 = 0 ; :: thesis: Sum ((D eqSumOf f) * t2) = Sum (f * t1)

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: verum

end;eqSupport (f,X) c= rng t1 ) & len t2 = 0 holds

Sum ((D eqSumOf f) * t2) = Sum (f * t1)

let t2 be one-to-one FinSequence of D; :: thesis: ( 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 = 0 implies Sum ((D eqSumOf f) * t2) = Sum (f * t1) )

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: ( not len t2 = 0 or Sum ((D eqSumOf f) * t2) = Sum (f * t1) )

assume len t2 = 0 ; :: thesis: Sum ((D eqSumOf f) * t2) = Sum (f * t1)

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: verum

S

proof

for i being Nat holds S
let j be Nat; :: thesis: ( S_{1}[j] implies S_{1}[j + 1] )

assume A8: S_{1}[j]
; :: thesis: S_{1}[j + 1]

let t1 be one-to-one FinSequence of A; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( not len t2 = j + 1 or Sum ((D eqSumOf f) * t2) = Sum (f * t1) )

assume A11: len t2 = j + 1 ; :: thesis: 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)

eqSupport (f,Y) c= rng r1

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

for x being Element of A st x in (rng t1) \ (rng qt1) holds

f . x = 0

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: verum

end;assume A8: S

let t1 be one-to-one FinSequence of A; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( not len t2 = j + 1 or Sum ((D eqSumOf f) * t2) = Sum (f * t1) )

assume A11: len t2 = j + 1 ; :: thesis: 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)

proof

for Y being Element of D st Y in rng r2 holds
for x being object st x in rng r2 holds

x in (proj D) .: (rng r1)

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

x in rng r2

end;x in (proj D) .: (rng r1)

proof

hence
rng r2 c= (proj D) .: (rng r1)
; :: according to XBOOLE_0:def 10 :: thesis: (proj D) .: (rng r1) c= rng r2
let x be object ; :: thesis: ( x in rng r2 implies x in (proj D) .: (rng r1) )

assume A17: x in rng r2 ; :: thesis: x in (proj D) .: (rng r1)

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}

then w in rng r1 by FINSEQ_3:65;

hence x in (proj D) .: (rng r1) by A18, A20, FUNCT_1:def 6; :: thesis: verum

end;assume A17: x in rng r2 ; :: thesis: x in (proj D) .: (rng r1)

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

then
w in (rng t1) \ ((proj D) " {X})
by A19, XBOOLE_0:def 5;
assume
w in (proj D) " {X}
; :: thesis: contradiction

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: verum

end;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: verum

then w in rng r1 by FINSEQ_3:65;

hence x in (proj D) .: (rng r1) by A18, A20, FUNCT_1:def 6; :: thesis: verum

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

x in rng r2

proof

hence
(proj D) .: (rng r1) c= rng r2
; :: thesis: verum
let x be object ; :: thesis: ( x in (proj D) .: (rng r1) implies x in rng r2 )

assume A21: x in (proj D) .: (rng r1) ; :: thesis: x in rng r2

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: verum

end;assume A21: x in (proj D) .: (rng r1) ; :: thesis: x in rng r2

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: verum

eqSupport (f,Y) c= rng r1

proof

then A30:
Sum ((D eqSumOf f) * r2) = Sum (f * r1)
by A16, A14, A8;
let Y be Element of D; :: thesis: ( Y in rng r2 implies eqSupport (f,Y) c= rng r1 )

assume A26: Y in rng r2 ; :: thesis: eqSupport (f,Y) c= rng r1

for x being object st x in eqSupport (f,Y) holds

x in rng r1

end;assume A26: Y in rng r2 ; :: thesis: eqSupport (f,Y) c= rng r1

for x being object st x in eqSupport (f,Y) holds

x in rng r1

proof

hence
eqSupport (f,Y) c= rng r1
; :: thesis: verum
let x be object ; :: thesis: ( x in eqSupport (f,Y) implies x in rng r1 )

assume A27: x in eqSupport (f,Y) ; :: thesis: x in rng r1

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}

hence x in rng r1 by FINSEQ_3:65; :: thesis: verum

end;assume A27: x in eqSupport (f,Y) ; :: thesis: x in rng r1

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

then
x in (rng t1) \ ((proj D) " {X})
by A28, XBOOLE_0:def 5;
assume
x in (proj D) " {X}
; :: thesis: contradiction

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: verum

end;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: verum

hence x in rng r1 by FINSEQ_3:65; :: thesis: verum

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

then
rng r1 misses rng canEq
by XBOOLE_0:def 1;
given x being object such that A31:
x in (rng r1) /\ (rng (canFS (eqSupport (f,X))))
; :: thesis: contradiction

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: verum

end;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: verum

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

then A36:
rng qt1 c= rng t1
;
let x be object ; :: thesis: ( x in rng qt1 implies x in rng t1 )

assume x in rng qt1 ; :: thesis: x in rng t1

then x in (rng r1) \/ (rng canEq) by FINSEQ_1:31;

end;assume x in rng qt1 ; :: thesis: x in rng t1

then x in (rng r1) \/ (rng canEq) by FINSEQ_1:31;

per cases then
( x in rng r1 or x in rng (canFS (eqSupport (f,X))) )
by XBOOLE_0:def 3;

end;

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

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: verum

end;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: verum

for x being Element of A st x in (rng t1) \ (rng qt1) holds

f . x = 0

proof

then A41:
Sum (f * qt1) = Sum (f * t1)
by A36, Th9;
let x be Element of A; :: thesis: ( x in (rng t1) \ (rng qt1) implies f . x = 0 )

assume x in (rng t1) \ (rng qt1) ; :: thesis: f . x = 0

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;

end;assume x in (rng t1) \ (rng qt1) ; :: thesis: f . x = 0

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 then
( not x in support f or not x in X )
by XBOOLE_0:def 4;

end;

suppose A39:
not x in X
; :: thesis: f . x = 0

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: verum

end;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: verum

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: verum

then S

hence Sum ((D eqSumOf f) * s2) = Sum (f * s1) by A1, A2; :: thesis: verum