let D be non empty set ; :: thesis: 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; :: thesis: 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 ; :: thesis: for r being Real st dom (F | X) is finite holds
Sum ((r (#) F),X) = r * (Sum (F,X))
let r be Real; :: thesis: ( dom (F | X) is finite implies Sum ((r (#) F),X) = r * (Sum (F,X)) )
set x = dom (F | X);
assume A1: dom (F | X) is finite ; :: thesis: Sum ((r (#) F),X) = r * (Sum (F,X))
then reconsider FX = F | X as finite Function by FINSET_1:29;
dom ((r (#) F) | X) = dom (r (#) (F | X)) by RFUNCT_1:65
.= dom (F | X) by VALUED_1:def 5 ;
then reconsider rFX = (r (#) F) | X as finite Function by A1, FINSET_1:29;
consider b being FinSequence such that
A2: F | (dom (F | X)),b are_fiberwise_equipotent by A1, RFINSEQ:18;
rng (F | (dom (F | X))) = rng b by A2, CLASSES1:83;
then reconsider b = b as FinSequence of REAL by FINSEQ_1:def 4;
dom (F | X) = (dom F) /\ X by RELAT_1:90;
then A3: F | (dom (F | X)) = (F | (dom F)) | X by RELAT_1:100
.= F | X by RELAT_1:97 ;
then A4: rng b = rng (F | X) by A2, CLASSES1:83;

A5: now

let x be Real; :: thesis: card (Coim ((r * b),x)) = card (Coim (rFX,x))
A6: len (r * b) = len b by FINSEQ_2:37;

now

per cases ( not x in rng (r * b) or x in rng (r * b) ) ;

case A7: not x in rng (r * b) ; :: thesis: card ((r * b) " {x}) = card (rFX " {x})

A8: now

assume x in rng ((r (#) F) | X) ; :: thesis: contradiction
then x in rng (r (#) (F | X)) by RFUNCT_1:65;
then consider d being Element of D such that
A9: d in dom (r (#) (F | X)) and
A10: (r (#) (F | X)) . d = x by PARTFUN1:26;
d in dom (F | X) by A9, VALUED_1:def 5;
then (F | X) . d in rng (F | X) by FUNCT_1:def 5;
then consider n being Nat such that
A11: n in dom b and
A12: b . n = (F | X) . d by A4, FINSEQ_2:11;
x = r * ((F | X) . d) by A9, A10, VALUED_1:def 5;
then A13: x = (r * b) . n by A12, RVSUM_1:66;
n in dom (r * b) by A6, A11, FINSEQ_3:31;
hence contradiction by A7, A13, FUNCT_1:def 5; :: thesis: verum

end;

(r * b) " {x} = {} by A7, Lm2;
hence card ((r * b) " {x}) = card (rFX " {x}) by A8, Lm2; :: thesis: verum

end;

case x in rng (r * b) ; :: thesis: 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:11;
reconsider p = b . n as Real ;
A15: x = r * p by A14, RVSUM_1:66;

now

per cases ( r = 0 or r <> 0 ) ;

case A16: r = 0 ; :: thesis: card ((r * b) " {x}) = card (rFX " {x})

then A17: (r * b) " {x} = dom b by A15, RFINSEQ:38;
dom FX = (r (#) (F | X)) " {x} by A15, A16, Th9
.= ((r (#) F) | X) " {x} by RFUNCT_1:65 ;
hence card ((r * b) " {x}) = card (rFX " {x}) by A2, A3, A17, CLASSES1:89; :: thesis: verum

end;

case A18: r <> 0 ; :: thesis: card (Coim ((r * b),x)) = card (Coim (rFX,x))

then A19: Coim ((r * b),x) = Coim (b,(x / r)) by RFINSEQ:37;
Coim (((r (#) F) | X),x) = (r (#) (F | X)) " {x} by RFUNCT_1:65
.= Coim (FX,(x / r)) by A18, Th8 ;
hence card (Coim ((r * b),x)) = card (Coim (rFX,x)) by A2, A3, A19, CLASSES1:def 9; :: thesis: verum

end;

end;

end;

hence card ((r * b) " {x}) = card (rFX " {x}) ; :: thesis: verum

end;

end;

end;

hence card (Coim ((r * b),x)) = card (Coim (rFX,x)) ; :: thesis: 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:87;
F | X, FinS (F,X) are_fiberwise_equipotent by A1, Def14;
then A21: Sum b = Sum (F,X) by A2, A3, CLASSES1:84, RFINSEQ:22;
dom ((r (#) F) | X) = (dom (r (#) F)) /\ X by RELAT_1:90
.= (dom F) /\ X by VALUED_1:def 5
.= dom (F | X) by RELAT_1:90 ;
then (r (#) F) | X, FinS ((r (#) F),X) are_fiberwise_equipotent by A1, Def14;
hence Sum ((r (#) F),X) = Sum (r * b) by A20, CLASSES1:84, RFINSEQ:22
.= r * (Sum (F,X)) by A21, RVSUM_1:117 ;
:: thesis: verum