let X, N be XFinSequence of INT ; :: thesis: ( len N = (len X) + 1 implies for c being Integer st N | (len X) = c (#) X holds
Sum N = (c * (Sum X)) + (N . (len X)) )
assume A1: len N = (len X) + 1 ; :: thesis: for c being Integer st N | (len X) = c (#) X holds
Sum N = (c * (Sum X)) + (N . (len X))
let c be Integer; :: thesis: ( N | (len X) = c (#) X implies Sum N = (c * (Sum X)) + (N . (len X)) )
assume A2: N | (len X) = c (#) X ; :: thesis: Sum N = (c * (Sum X)) + (N . (len X))
A3: len X in Segm (len N) by A1, NAT_1:45;
thus Sum N = Sum (N | (len N))
.= (Sum (N | (len X))) + (N . (len X)) by A1, AFINSQ_2:65, A3
.= (c * (Sum X)) + (N . (len X)) by A2, AFINSQ_2:64 ; :: thesis: verum