let F be XFinSequence of INT ; :: 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 A1: ( F is empty & F . ((len F) -' 1) = 0 ) by FUNCT_1:def 2;
then Sum F = 0 ;
hence c * (Sum F) = (Sum ((c (#) F) | ((len F) -' 1))) + (c * (F . ((len F) -' 1))) by A1; :: thesis: verum

end;

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

then A2: ((len F) -' 1) + 1 = len F by NAT_1:14, XREAL_1:235;
A3: dom F = dom (c (#) F) by VALUED_1:def 5;
A4: c * (Sum F) = Sum (c (#) F) by AFINSQ_2:64;
A5: Sum (c (#) F) = Sum ((c (#) F) | (len F)) by A3;
(len F) -' 1 in Segm (len F) by A2, NAT_1:45;
then Sum ((c (#) F) | (((len F) -' 1) + 1)) = (Sum ((c (#) F) | ((len F) -' 1))) + ((c (#) F) . ((len F) -' 1)) by A3, AFINSQ_2:65;
hence c * (Sum F) = (Sum ((c (#) F) | ((len F) -' 1))) + (c * (F . ((len F) -' 1))) by A4, A5, A2, VALUED_1:6; :: thesis: verum

end;

end;