let F be XFinSequence of ; :: thesis: for c being Integer holds c * (Sum F) = (Sum ((c (#) F) | ((len F) -' 1))) + (c * (F . ((len F) -' 1)))
let c be Integer; :: thesis: c * (Sum F) = (Sum ((c (#) F) | ((len F) -' 1))) + (c * (F . ((len F) -' 1)))

per cases ( len F = 0 or len F > 0 ) ;

suppose len F = 0 ; :: thesis: c * (Sum F) = (Sum ((c (#) F) | ((len F) -' 1))) + (c * (F . ((len F) -' 1)))

then A: ( F is empty & F . ((len F) -' 1) = 0 ) by FUNCT_1:def 4;
then Sum F = 0 ;
hence c * (Sum F) = (Sum ((c (#) F) | ((len F) -' 1))) + (c * (F . ((len F) -' 1))) by A; :: thesis: verum

end;

suppose len F > 0 ; :: thesis: c * (Sum F) = (Sum ((c (#) F) | ((len F) -' 1))) + (c * (F . ((len F) -' 1)))

then B: ((len F) -' 1) + 1 = len F by XREAL_1:237, NAT_1:14;
F: dom F = dom (c (#) F) by VALUED_1:def 5;
Z: c * (Sum F) = Sum (c (#) F) by AFINSQ_2:76;
Y: Sum (c (#) F) = Sum ((c (#) F) | (len F)) by RELAT_1:98, F;
Sum ((c (#) F) | (((len F) -' 1) + 1)) = (Sum ((c (#) F) | ((len F) -' 1))) + ((c (#) F) . ((len F) -' 1)) by AFINSQ_2:77, F, NAT_1:46, B;
hence c * (Sum F) = (Sum ((c (#) F) | ((len F) -' 1))) + (c * (F . ((len F) -' 1))) by VALUED_1:6, Z, Y, B; :: thesis: verum

end;

end;