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