let A be set ; :: thesis: for D being a_partition of A

for f being finite-support Function of A,REAL holds D eqSumOf (- f) = - (D eqSumOf f)

let D be a_partition of A; :: thesis: for f being finite-support Function of A,REAL holds D eqSumOf (- f) = - (D eqSumOf f)

let f be finite-support Function of A,REAL; :: thesis: D eqSumOf (- f) = - (D eqSumOf f)

dom (D eqSumOf (- f)) = D by FUNCT_2:def 1;

then A1: dom (D eqSumOf (- f)) = dom (- (D eqSumOf f)) by FUNCT_2:def 1;

for X being object st X in dom (D eqSumOf (- f)) holds

(D eqSumOf (- f)) . X = (- (D eqSumOf f)) . X

for f being finite-support Function of A,REAL holds D eqSumOf (- f) = - (D eqSumOf f)

let D be a_partition of A; :: thesis: for f being finite-support Function of A,REAL holds D eqSumOf (- f) = - (D eqSumOf f)

let f be finite-support Function of A,REAL; :: thesis: D eqSumOf (- f) = - (D eqSumOf f)

dom (D eqSumOf (- f)) = D by FUNCT_2:def 1;

then A1: dom (D eqSumOf (- f)) = dom (- (D eqSumOf f)) by FUNCT_2:def 1;

for X being object st X in dom (D eqSumOf (- f)) holds

(D eqSumOf (- f)) . X = (- (D eqSumOf f)) . X

proof

hence
D eqSumOf (- f) = - (D eqSumOf f)
by A1, FUNCT_1:2; :: thesis: verum
let X be object ; :: thesis: ( X in dom (D eqSumOf (- f)) implies (D eqSumOf (- f)) . X = (- (D eqSumOf f)) . X )

assume A2: X in dom (D eqSumOf (- f)) ; :: thesis: (D eqSumOf (- f)) . X = (- (D eqSumOf f)) . X

then reconsider Y = X as Element of D ;

set s = canFS (eqSupport (f,Y));

set t = canFS (eqSupport ((- f),Y));

A3: dom f = A by FUNCT_2:def 1;

A4: rng (canFS (eqSupport (f,Y))) = eqSupport (f,Y) by FUNCT_2:def 3;

A5: rng (canFS (eqSupport ((- f),Y))) = eqSupport ((- f),Y) by FUNCT_2:def 3;

A6: dom (canFS (eqSupport (f,Y))) = Seg (len (canFS (eqSupport (f,Y)))) by FINSEQ_1:def 3

.= Seg (len (canFS (eqSupport ((- f),Y)))) by Th52

.= dom (canFS (eqSupport ((- f),Y))) by FINSEQ_1:def 3 ;

A7: ( rng (canFS (eqSupport (f,Y))) c= dom f & rng (canFS (eqSupport ((- f),Y))) c= dom f ) by A3, A4, A5;

canFS (eqSupport (f,Y)), canFS (eqSupport ((- f),Y)) are_fiberwise_equipotent by Th52;

then A8: f * (canFS (eqSupport (f,Y))),f * (canFS (eqSupport ((- f),Y))) are_fiberwise_equipotent by A7, A6, CLASSES1:83;

A9: ( rng (f * (canFS (eqSupport (f,Y)))) c= REAL & rng (f * (canFS (eqSupport ((- f),Y)))) c= REAL ) ;

then A10: ( f * (canFS (eqSupport (f,Y))) is FinSequence of REAL & f * (canFS (eqSupport ((- f),Y))) is FinSequence of REAL ) by FINSEQ_1:def 4;

A11: dom ((- f) * (canFS (eqSupport ((- f),Y)))) = dom (- (f * (canFS (eqSupport ((- f),Y)))))

((- f) * (canFS (eqSupport ((- f),Y)))) . x = (- (f * (canFS (eqSupport ((- f),Y))))) . x

thus (D eqSumOf (- f)) . X = Sum ((- f) * (canFS (eqSupport ((- f),Y)))) by A2, Def14

.= - (Sum (f * (canFS (eqSupport ((- f),Y))))) by A14, RVSUM_1:88

.= - (Sum (f * (canFS (eqSupport (f,Y))))) by A8, A10, RFINSEQ:9

.= - ((D eqSumOf f) . Y) by A2, Def14

.= (- (D eqSumOf f)) . X by A2, RFUNCT_1:58 ; :: thesis: verum

end;assume A2: X in dom (D eqSumOf (- f)) ; :: thesis: (D eqSumOf (- f)) . X = (- (D eqSumOf f)) . X

then reconsider Y = X as Element of D ;

set s = canFS (eqSupport (f,Y));

set t = canFS (eqSupport ((- f),Y));

A3: dom f = A by FUNCT_2:def 1;

A4: rng (canFS (eqSupport (f,Y))) = eqSupport (f,Y) by FUNCT_2:def 3;

A5: rng (canFS (eqSupport ((- f),Y))) = eqSupport ((- f),Y) by FUNCT_2:def 3;

A6: dom (canFS (eqSupport (f,Y))) = Seg (len (canFS (eqSupport (f,Y)))) by FINSEQ_1:def 3

.= Seg (len (canFS (eqSupport ((- f),Y)))) by Th52

.= dom (canFS (eqSupport ((- f),Y))) by FINSEQ_1:def 3 ;

A7: ( rng (canFS (eqSupport (f,Y))) c= dom f & rng (canFS (eqSupport ((- f),Y))) c= dom f ) by A3, A4, A5;

canFS (eqSupport (f,Y)), canFS (eqSupport ((- f),Y)) are_fiberwise_equipotent by Th52;

then A8: f * (canFS (eqSupport (f,Y))),f * (canFS (eqSupport ((- f),Y))) are_fiberwise_equipotent by A7, A6, CLASSES1:83;

A9: ( rng (f * (canFS (eqSupport (f,Y)))) c= REAL & rng (f * (canFS (eqSupport ((- f),Y)))) c= REAL ) ;

then A10: ( f * (canFS (eqSupport (f,Y))) is FinSequence of REAL & f * (canFS (eqSupport ((- f),Y))) is FinSequence of REAL ) by FINSEQ_1:def 4;

A11: dom ((- f) * (canFS (eqSupport ((- f),Y)))) = dom (- (f * (canFS (eqSupport ((- f),Y)))))

proof

for x being object st x in dom ((- f) * (canFS (eqSupport ((- f),Y)))) holds
for x being object holds

( x in dom ((- f) * (canFS (eqSupport ((- f),Y)))) iff x in dom (- (f * (canFS (eqSupport ((- f),Y))))) )

end;( x in dom ((- f) * (canFS (eqSupport ((- f),Y)))) iff x in dom (- (f * (canFS (eqSupport ((- f),Y))))) )

proof

hence
dom ((- f) * (canFS (eqSupport ((- f),Y)))) = dom (- (f * (canFS (eqSupport ((- f),Y)))))
by TARSKI:2; :: thesis: verum
rng f c= COMPLEX
by NUMBERS:11;

then reconsider fc = f as Function of (dom f),COMPLEX by FUNCT_2:2;

let x be object ; :: thesis: ( x in dom ((- f) * (canFS (eqSupport ((- f),Y)))) iff x in dom (- (f * (canFS (eqSupport ((- f),Y))))) )

then x in dom (fc * (canFS (eqSupport ((- f),Y)))) by CFUNCT_1:5;

then ( x in dom (canFS (eqSupport ((- f),Y))) & (canFS (eqSupport ((- f),Y))) . x in dom fc ) by FUNCT_1:11;

then ( x in dom (canFS (eqSupport ((- f),Y))) & (canFS (eqSupport ((- f),Y))) . x in dom (- fc) ) by CFUNCT_1:5;

hence x in dom ((- f) * (canFS (eqSupport ((- f),Y)))) by FUNCT_1:11; :: thesis: verum

end;then reconsider fc = f as Function of (dom f),COMPLEX by FUNCT_2:2;

let x be object ; :: thesis: ( x in dom ((- f) * (canFS (eqSupport ((- f),Y)))) iff x in dom (- (f * (canFS (eqSupport ((- f),Y))))) )

hereby :: thesis: ( x in dom (- (f * (canFS (eqSupport ((- f),Y))))) implies x in dom ((- f) * (canFS (eqSupport ((- f),Y)))) )

assume
x in dom (- (f * (canFS (eqSupport ((- f),Y)))))
; :: thesis: x in dom ((- f) * (canFS (eqSupport ((- f),Y))))assume
x in dom ((- f) * (canFS (eqSupport ((- f),Y))))
; :: thesis: x in dom (- (f * (canFS (eqSupport ((- f),Y)))))

then ( x in dom (canFS (eqSupport ((- f),Y))) & (canFS (eqSupport ((- f),Y))) . x in dom (- fc) ) by FUNCT_1:11;

then x in dom (fc * (canFS (eqSupport ((- f),Y)))) by FUNCT_1:11;

hence x in dom (- (f * (canFS (eqSupport ((- f),Y))))) by CFUNCT_1:5; :: thesis: verum

end;then ( x in dom (canFS (eqSupport ((- f),Y))) & (canFS (eqSupport ((- f),Y))) . x in dom (- fc) ) by FUNCT_1:11;

then x in dom (fc * (canFS (eqSupport ((- f),Y)))) by FUNCT_1:11;

hence x in dom (- (f * (canFS (eqSupport ((- f),Y))))) by CFUNCT_1:5; :: thesis: verum

then x in dom (fc * (canFS (eqSupport ((- f),Y)))) by CFUNCT_1:5;

then ( x in dom (canFS (eqSupport ((- f),Y))) & (canFS (eqSupport ((- f),Y))) . x in dom fc ) by FUNCT_1:11;

then ( x in dom (canFS (eqSupport ((- f),Y))) & (canFS (eqSupport ((- f),Y))) . x in dom (- fc) ) by CFUNCT_1:5;

hence x in dom ((- f) * (canFS (eqSupport ((- f),Y)))) by FUNCT_1:11; :: thesis: verum

((- f) * (canFS (eqSupport ((- f),Y)))) . x = (- (f * (canFS (eqSupport ((- f),Y))))) . x

proof

then A14:
(- f) * (canFS (eqSupport ((- f),Y))) = - (f * (canFS (eqSupport ((- f),Y))))
by A11, FUNCT_1:2;
let x be object ; :: thesis: ( x in dom ((- f) * (canFS (eqSupport ((- f),Y)))) implies ((- f) * (canFS (eqSupport ((- f),Y)))) . x = (- (f * (canFS (eqSupport ((- f),Y))))) . x )

set domft = dom (f * (canFS (eqSupport ((- f),Y))));

rng (f * (canFS (eqSupport ((- f),Y)))) c= COMPLEX by NUMBERS:11;

then reconsider ftc = f * (canFS (eqSupport ((- f),Y))) as Function of (dom (f * (canFS (eqSupport ((- f),Y))))),COMPLEX by FUNCT_2:2;

assume A12: x in dom ((- f) * (canFS (eqSupport ((- f),Y)))) ; :: thesis: ((- f) * (canFS (eqSupport ((- f),Y)))) . x = (- (f * (canFS (eqSupport ((- f),Y))))) . x

then a13: x in dom (- ftc) by A11;

then reconsider domft = dom (f * (canFS (eqSupport ((- f),Y)))) as non empty set ;

not dom f is empty then reconsider domf = dom f as non empty set ;

reconsider tc = (canFS (eqSupport ((- f),Y))) . x as Element of domf by a13, FUNCT_1:11;

reconsider c = x as Element of domft by a13;

reconsider F = f as Function of domf,REAL by FUNCT_2:def 1;

reconsider FT = f * (canFS (eqSupport ((- f),Y))) as Function of domft,REAL by A9, FUNCT_2:2;

thus ((- f) * (canFS (eqSupport ((- f),Y)))) . x = (- f) . ((canFS (eqSupport ((- f),Y))) . x) by A12, FUNCT_1:12

.= - (F . tc) by RFUNCT_1:58

.= - (FT . c) by FUNCT_1:12

.= (- (f * (canFS (eqSupport ((- f),Y))))) . x by RFUNCT_1:58 ; :: thesis: verum

end;set domft = dom (f * (canFS (eqSupport ((- f),Y))));

rng (f * (canFS (eqSupport ((- f),Y)))) c= COMPLEX by NUMBERS:11;

then reconsider ftc = f * (canFS (eqSupport ((- f),Y))) as Function of (dom (f * (canFS (eqSupport ((- f),Y))))),COMPLEX by FUNCT_2:2;

assume A12: x in dom ((- f) * (canFS (eqSupport ((- f),Y)))) ; :: thesis: ((- f) * (canFS (eqSupport ((- f),Y)))) . x = (- (f * (canFS (eqSupport ((- f),Y))))) . x

then a13: x in dom (- ftc) by A11;

then reconsider domft = dom (f * (canFS (eqSupport ((- f),Y)))) as non empty set ;

not dom f is empty then reconsider domf = dom f as non empty set ;

reconsider tc = (canFS (eqSupport ((- f),Y))) . x as Element of domf by a13, FUNCT_1:11;

reconsider c = x as Element of domft by a13;

reconsider F = f as Function of domf,REAL by FUNCT_2:def 1;

reconsider FT = f * (canFS (eqSupport ((- f),Y))) as Function of domft,REAL by A9, FUNCT_2:2;

thus ((- f) * (canFS (eqSupport ((- f),Y)))) . x = (- f) . ((canFS (eqSupport ((- f),Y))) . x) by A12, FUNCT_1:12

.= - (F . tc) by RFUNCT_1:58

.= - (FT . c) by FUNCT_1:12

.= (- (f * (canFS (eqSupport ((- f),Y))))) . x by RFUNCT_1:58 ; :: thesis: verum

thus (D eqSumOf (- f)) . X = Sum ((- f) * (canFS (eqSupport ((- f),Y)))) by A2, Def14

.= - (Sum (f * (canFS (eqSupport ((- f),Y))))) by A14, RVSUM_1:88

.= - (Sum (f * (canFS (eqSupport (f,Y))))) by A8, A10, RFINSEQ:9

.= - ((D eqSumOf f) . Y) by A2, Def14

.= (- (D eqSumOf f)) . X by A2, RFUNCT_1:58 ; :: thesis: verum