let A be set ; 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; 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; 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 ;
( X in dom (D eqSumOf (- f)) implies (D eqSumOf (- f)) . X = (- (D eqSumOf f)) . X )
assume A2:
X in dom (D eqSumOf (- f))
;
(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 ;
( x in dom ((- f) * (canFS (eqSupport ((- f),Y)))) iff x in dom (- (f * (canFS (eqSupport ((- f),Y))))) )
assume
x in dom (- (f * (canFS (eqSupport ((- f),Y)))))
;
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;
verum
end;
hence
dom ((- f) * (canFS (eqSupport ((- f),Y)))) = dom (- (f * (canFS (eqSupport ((- f),Y)))))
by TARSKI:2;
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 ;
( 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))))
;
((- 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
;
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
;
verum
end;
hence
D eqSumOf (- f) = - (D eqSumOf f)
by A1, FUNCT_1:2; verum