let D be non empty set ; for F being PartFunc of D,REAL
for X being set
for r being Real st dom (F | X) is finite holds
Sum ((r (#) F),X) = r * (Sum (F,X))
let F be PartFunc of D,REAL; for X being set
for r being Real st dom (F | X) is finite holds
Sum ((r (#) F),X) = r * (Sum (F,X))
let X be set ; for r being Real st dom (F | X) is finite holds
Sum ((r (#) F),X) = r * (Sum (F,X))
let r be Real; ( dom (F | X) is finite implies Sum ((r (#) F),X) = r * (Sum (F,X)) )
set x = dom (F | X);
reconsider rr = r as Real ;
assume A1:
dom (F | X) is finite
; Sum ((r (#) F),X) = r * (Sum (F,X))
then reconsider FX = F | X as finite Function by FINSET_1:10;
dom ((r (#) F) | X) =
dom (r (#) (F | X))
by RFUNCT_1:49
.=
dom (F | X)
by VALUED_1:def 5
;
then reconsider rFX = (r (#) F) | X as finite Function by A1, FINSET_1:10;
consider b being FinSequence such that
A2:
F | (dom (F | X)),b are_fiberwise_equipotent
by A1, RFINSEQ:5;
rng (F | (dom (F | X))) = rng b
by A2, CLASSES1:75;
then reconsider b = b as FinSequence of REAL by FINSEQ_1:def 4;
dom (F | X) = (dom F) /\ X
by RELAT_1:61;
then A3: F | (dom (F | X)) =
(F | (dom F)) | X
by RELAT_1:71
.=
F | X
by RELAT_1:68
;
then A4:
rng b = rng (F | X)
by A2, CLASSES1:75;
A5:
now for x being Element of REAL holds card (Coim ((r * b),x)) = card (Coim (rFX,x))let x be
Element of
REAL ;
card (Coim ((r * b),x)) = card (Coim (rFX,x))A6:
len (r * b) = len b
by FINSEQ_2:33;
now ( ( not x in rng (r * b) & card ((r * b) " {x}) = card (rFX " {x}) ) or ( x in rng (r * b) & card ((r * b) " {x}) = card (rFX " {x}) ) )per cases
( not x in rng (r * b) or x in rng (r * b) )
;
case
x in rng (r * b)
;
card ((r * b) " {x}) = card (rFX " {x})then consider n being
Nat such that
n in dom (r * b)
and A14:
(r * b) . n = x
by FINSEQ_2:10;
reconsider p =
b . n as
Real ;
A15:
x = r * p
by A14, RVSUM_1:44;
now ( ( r = 0 & card ((r * b) " {x}) = card (rFX " {x}) ) or ( r <> 0 & card (Coim ((r * b),x)) = card (Coim (rFX,x)) ) )per cases
( r = 0 or r <> 0 )
;
case A18:
r <> 0
;
card (Coim ((r * b),x)) = card (Coim (rFX,x))then A19:
Coim (
(rr * b),
x)
= Coim (
b,
(x / rr))
by RFINSEQ:24;
Coim (
((r (#) F) | X),
x) =
(r (#) (F | X)) " {x}
by RFUNCT_1:49
.=
Coim (
FX,
(x / r))
by A18, Th6
;
hence
card (Coim ((r * b),x)) = card (Coim (rFX,x))
by A2, A3, A19, CLASSES1:def 10;
verum end; end; end; hence
card ((r * b) " {x}) = card (rFX " {x})
;
verum end; end; end; hence
card (Coim ((r * b),x)) = card (Coim (rFX,x))
;
verum end;
( rng (r * b) c= REAL & rng ((r (#) F) | X) c= REAL )
;
then A20:
r * b,(r (#) F) | X are_fiberwise_equipotent
by A5, CLASSES1:79;
F | X, FinS (F,X) are_fiberwise_equipotent
by A1, Def13;
then A21:
Sum b = Sum (F,X)
by A2, A3, CLASSES1:76, RFINSEQ:9;
dom ((r (#) F) | X) =
(dom (r (#) F)) /\ X
by RELAT_1:61
.=
(dom F) /\ X
by VALUED_1:def 5
.=
dom (F | X)
by RELAT_1:61
;
then
(r (#) F) | X, FinS ((r (#) F),X) are_fiberwise_equipotent
by A1, Def13;
hence Sum ((r (#) F),X) =
Sum (r * b)
by A20, CLASSES1:76, RFINSEQ:9
.=
r * (Sum (F,X))
by A21, RVSUM_1:87
;
verum