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
proof
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)))))
proof
for x being object holds
( x in dom ((- f) * (canFS (eqSupport ((- f),Y)))) iff x in dom (- (f * (canFS (eqSupport ((- f),Y))))) )
proof
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))))) )
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)))))
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;
assume x in dom (- (f * (canFS (eqSupport ((- f),Y))))) ; :: thesis: 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;
hence dom ((- f) * (canFS (eqSupport ((- f),Y)))) = dom (- (f * (canFS (eqSupport ((- f),Y))))) by TARSKI:2; :: thesis: verum
end;
for x being object st x in dom ((- f) * (canFS (eqSupport ((- f),Y)))) holds
((- f) * (canFS (eqSupport ((- f),Y)))) . x = (- (f * (canFS (eqSupport ((- f),Y))))) . x
proof
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;
then A14: (- f) * (canFS (eqSupport ((- f),Y))) = - (f * (canFS (eqSupport ((- f),Y)))) by A11, FUNCT_1:2;
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;
hence D eqSumOf (- f) = - (D eqSumOf f) by A1, FUNCT_1:2; :: thesis: verum