let M be Matrix of REAL; :: thesis: for p being FinSequence of REAL * st ( for k being Nat st k >= 1 & k < len M holds
p . (k + 1) = (p . k) ^ (M . (k + 1)) ) holds
for k being Nat st k >= 1 & k < len M holds
Sum (p . (k + 1)) = (Sum (p . k)) + (Sum (M . (k + 1)))
let p be FinSequence of REAL * ; :: thesis: ( ( for k being Nat st k >= 1 & k < len M holds
p . (k + 1) = (p . k) ^ (M . (k + 1)) ) implies for k being Nat st k >= 1 & k < len M holds
Sum (p . (k + 1)) = (Sum (p . k)) + (Sum (M . (k + 1))) )
assume A1: for k being Nat st k >= 1 & k < len M holds
p . (k + 1) = (p . k) ^ (M . (k + 1)) ; :: thesis: for k being Nat st k >= 1 & k < len M holds
Sum (p . (k + 1)) = (Sum (p . k)) + (Sum (M . (k + 1)))
let k be Nat; :: thesis: ( k >= 1 & k < len M implies Sum (p . (k + 1)) = (Sum (p . k)) + (Sum (M . (k + 1))) )
assume that
A2: k >= 1 and
A3: k < len M ; :: thesis: Sum (p . (k + 1)) = (Sum (p . k)) + (Sum (M . (k + 1)))
p . (k + 1) = (p . k) ^ (M . (k + 1)) by A1, A2, A3;
hence Sum (p . (k + 1)) = (Sum (p . k)) + (Sum (M . (k + 1))) by RVSUM_1:75; :: thesis: verum