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);
reconsider rr = r as Real ;
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: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 :: thesis: for x being Element of REAL holds card (Coim ((r * b),x)) = card (Coim (rFX,x))

let x be Element of REAL ; :: thesis: card (Coim ((r * b),x)) = card (Coim (rFX,x))
A6: len (r * b) = len b by FINSEQ_2:33;

now :: thesis: ( ( 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 A7: not x in rng (r * b) ; :: thesis: card ((r * b) " {x}) = card (rFX " {x})

A8: now :: thesis: not x in rng ((r (#) F) | X)

assume x in rng ((r (#) F) | X) ; :: thesis: contradiction
then x in rng (r (#) (F | X)) by RFUNCT_1:49;
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:3;
d in dom (F | X) by A9, VALUED_1:def 5;
then (F | X) . d in rng (F | X) by FUNCT_1:def 3;
then consider n being Nat such that
A11: n in dom b and
A12: b . n = (F | X) . d by A4, FINSEQ_2:10;
x = r * ((F | X) . d) by A9, A10, VALUED_1:def 5;
then A13: x = (r * b) . n by A12, RVSUM_1:44;
n in dom (r * b) by A6, A11, FINSEQ_3:29;
hence contradiction by A7, A13, FUNCT_1:def 3; :: 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:10;
reconsider p = b . n as Real ;
A15: x = r * p by A14, RVSUM_1:44;

now :: thesis: ( ( 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 A16: r = 0 ; :: thesis: card ((r * b) " {x}) = card (rFX " {x})

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

end;

case A18: r <> 0 ; :: thesis: 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; :: 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: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 ;
:: thesis: verum