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

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

suppose A4: len M = 0 ; :: thesis: SumAll M = Sum (p . (len M))

then p = {} by A1;
hence Sum (p . (len M)) = 0 by FUNCT_1:def 2, RELAT_1:38, RVSUM_1:72
.= SumAll M by A4, MATRPROB:23 ;
:: thesis: verum

end;

suppose A5: len M > 0 ; :: thesis: SumAll M = Sum (p . (len M))

then A6: len M >= 1 by NAT_1:14;
set q = LineSum M;
A7: len (LineSum M) = len M by MATRPROB:def 1;
then consider qq being FinSequence of REAL such that
A8: len qq = len (LineSum M) and
A9: qq . 1 = (LineSum M) . 1 and
A10: for k being Nat st 0 <> k & k < len (LineSum M) holds
qq . (k + 1) = (qq . k) + ((LineSum M) . (k + 1)) and
A11: Sum (LineSum M) = qq . (len (LineSum M)) by A5, Th9, NAT_1:14;
A12: len qq = len M by A8, MATRPROB:def 1
.= len (Sum p) by A1, MATRPROB:def 1 ;
A13: dom qq = Seg (len qq) by FINSEQ_1:def 3;
A14: len (Sum p) = len p by MATRPROB:def 1;
then A15: dom (Sum p) = dom p by FINSEQ_3:29;
for j being Nat st j in dom qq holds
qq . j = (Sum p) . j

proof

defpred S₁[ Nat] means ( $1 in dom qq implies qq . $1 = (Sum p) . $1 );
A16: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A17: S₁[k] ; :: thesis: S₁[k + 1]
assume A18: k + 1 in dom qq ; :: thesis: qq . (k + 1) = (Sum p) . (k + 1)
then A19: k + 1 <= len qq by A13, FINSEQ_1:1;
A20: k + 1 in dom (Sum p) by A1, A7, A14, A8, A13, A18, FINSEQ_1:def 3;
A21: k + 1 in dom M by A7, A8, A13, A18, FINSEQ_1:def 3;
k + 1 >= 1 by A13, A18, FINSEQ_1:1;
then A22: ( k + 1 = 1 or k + 1 > 1 ) by XXREAL_0:1;

per cases ( k + 1 = 1 or k >= 1 ) by A22, NAT_1:13;

suppose A23: k + 1 = 1 ; :: thesis: qq . (k + 1) = (Sum p) . (k + 1)

A24: 1 in Seg (len M) by A6, FINSEQ_1:1;
then A25: 1 in dom M by FINSEQ_1:def 3;
A26: 1 in dom p by A1, A24, FINSEQ_1:def 3;
qq . (k + 1) = Sum (Line (M,1)) by A9, A23, A24, MATRPROB:20
.= Sum (M . 1) by A25, MATRIX_0:60
.= (Sum p) . 1 by A2, A15, A26, MATRPROB:def 1 ;
hence qq . (k + 1) = (Sum p) . (k + 1) by A23; :: thesis: verum

end;

suppose A27: k >= 1 ; :: thesis: qq . (k + 1) = (Sum p) . (k + 1)

A28: k < len qq by A19, NAT_1:13;
then A29: k < len M by A8, MATRPROB:def 1;
k in Seg (len qq) by A27, A28, FINSEQ_1:1;
then A30: k in dom (Sum p) by A12, FINSEQ_1:def 3;
qq . (k + 1) = (qq . k) + ((LineSum M) . (k + 1)) by A8, A10, A27, A28
.= (Sum (p . k)) + ((LineSum M) . (k + 1)) by A13, A17, A27, A28, A30, FINSEQ_1:1, MATRPROB:def 1
.= (Sum (p . k)) + (Sum (Line (M,(k + 1)))) by A7, A8, A13, A18, MATRPROB:20
.= (Sum (p . k)) + (Sum (M . (k + 1))) by A21, MATRIX_0:60
.= Sum (p . (k + 1)) by A3, A27, A29, Th37
.= (Sum p) . (k + 1) by A20, MATRPROB:def 1 ;
hence qq . (k + 1) = (Sum p) . (k + 1) ; :: thesis: verum

end;

end;

end;

A31: S₁[ 0 ] by A13, FINSEQ_1:1;
for j being Nat holds S₁[j] from NAT_1:sch 2(A31, A16);
hence for j being Nat st j in dom qq holds
qq . j = (Sum p) . j ; :: thesis: verum

end;

then A32: qq = Sum p by A12, FINSEQ_2:9;
len M in Seg (len M) by A5, FINSEQ_1:3;
then A33: len M in dom (Sum p) by A1, A14, FINSEQ_1:def 3;
thus SumAll M = Sum (LineSum M) by MATRPROB:def 3
.= (Sum p) . (len M) by A11, A32, MATRPROB:def 1
.= Sum (p . (len M)) by A33, MATRPROB:def 1 ; :: thesis: verum

end;

end;