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) )
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;
set x = dom (F | X);
consider b being FinSequence such that
A2: F | (dom (F | X)),b are_fiberwise_equipotent by A1, RFINSEQ:18;
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 ;
( rng (F | (dom (F | X))) c= rng F & rng F c= REAL & rng (F | (dom (F | X))) = rng b ) by A2, CLASSES1:83, RELAT_1:99;
then reconsider b = b as FinSequence of REAL by FINSEQ_1:def 4;
F | X, FinS F,X are_fiberwise_equipotent by A1, Def14;
then A4: Sum b = Sum F,X by A2, A3, CLASSES1:84, RFINSEQ:22;
A5: 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 ;
A6: ( rng (r * b) c= REAL & rng ((r (#) F) | X) c= REAL & rng b c= REAL & rng (F | X) c= REAL ) ;
A7: rng b = rng (F | X) by A2, A3, CLASSES1:83;
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;

now

let x be Real; :: thesis: card (Coim (r * b),x) = card (Coim rFX,x)
A8: 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 A9: not x in rng (r * b) ; :: thesis: card ((r * b) " {x}) = card (rFX " {x})

then A10: (r * b) " {x} = {} by Lm2;

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
A11: ( d in dom (r (#) (F | X)) & (r (#) (F | X)) . d = x ) by PARTFUN1:26;
A12: ( x = r * ((F | X) . d) & d in dom (F | X) ) by A11, VALUED_1:def 5;
then (F | X) . d in rng (F | X) by FUNCT_1:def 5;
then consider n being Nat such that
A13: ( n in dom b & b . n = (F | X) . d ) by A7, FINSEQ_2:11;
A14: n in dom (r * b) by A8, A13, FINSEQ_3:31;
x = (r * b) . n by A12, A13, RVSUM_1:66;
hence contradiction by A9, A14, FUNCT_1:def 5; :: thesis: verum

end;

hence card ((r * b) " {x}) = card (rFX " {x}) by A10, 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
A15: ( n in dom (r * b) & (r * b) . n = x ) by FINSEQ_2:11;
reconsider p = b . n as Real ;
A16: x = r * p by A15, RVSUM_1:66;

now

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

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

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

end;

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

then A20: 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 A19, Th8 ;
hence card (Coim (r * b),x) = card (Coim rFX,x) by A2, A3, A20, 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;

then A21: r * b,(r (#) F) | X are_fiberwise_equipotent by A6, CLASSES1:87;
(r (#) F) | X, FinS (r (#) F),X are_fiberwise_equipotent by A1, A5, Def14;
hence Sum (r (#) F),X = Sum (r * b) by A21, CLASSES1:84, RFINSEQ:22
.= r * (Sum F,X) by A4, RVSUM_1:117 ;
:: thesis: verum