let n, m be Nat; :: thesis: for Rseq being Function of [:NAT,NAT:],REAL
for M being Matrix of n + 1,m + 1,REAL st ( for i, j being Nat st i <= n & j <= m holds
Rseq . (i,j) = M * ((i + 1),(j + 1)) ) holds
(Partial_Sums Rseq) . (n,m) = SumAll M
let Rseq be Function of [:NAT,NAT:],REAL; :: thesis: for M being Matrix of n + 1,m + 1,REAL st ( for i, j being Nat st i <= n & j <= m holds
Rseq . (i,j) = M * ((i + 1),(j + 1)) ) holds
(Partial_Sums Rseq) . (n,m) = SumAll M
let M be Matrix of n + 1,m + 1,REAL; :: thesis: ( ( for i, j being Nat st i <= n & j <= m holds
Rseq . (i,j) = M * ((i + 1),(j + 1)) ) implies (Partial_Sums Rseq) . (n,m) = SumAll M )
assume A1: for i, j being Nat st i <= n & j <= m holds
Rseq . (i,j) = M * ((i + 1),(j + 1)) ; :: thesis: (Partial_Sums Rseq) . (n,m) = SumAll M
A2: len M = n + 1 by MATRIX_0:25;
then A3: width M = m + 1 by MATRIX_0:20;
X1: for i being Nat st i <= n holds
(Partial_Sums_in_cod2 Rseq) . (i,m) = (LineSum M) . (i + 1)
proof
let i be Nat; :: thesis: ( i <= n implies (Partial_Sums_in_cod2 Rseq) . (i,m) = (LineSum M) . (i + 1) )
assume B0: i <= n ; :: thesis: (Partial_Sums_in_cod2 Rseq) . (i,m) = (LineSum M) . (i + 1)
then ( 1 <= i + 1 & i + 1 <= n + 1 ) by NAT_1:11, XREAL_1:6;
then B01: i + 1 in Seg (n + 1) by FINSEQ_1:1;
defpred S1[ Nat] means ( $1 + 1 <= width M implies (Partial_Sums_in_cod2 Rseq) . (i,$1) = Sum ((Line (M,(i + 1))) | ($1 + 1)) );
now :: thesis: ( 0 + 1 <= width M implies (Partial_Sums_in_cod2 Rseq) . (i,0) = Sum ((Line (M,(i + 1))) | (0 + 1)) )
assume 0 + 1 <= width M ; :: thesis: (Partial_Sums_in_cod2 Rseq) . (i,0) = Sum ((Line (M,(i + 1))) | (0 + 1))
B2: (Partial_Sums_in_cod2 Rseq) . (i,0) = Rseq . (i,0) by DefCS;
len (Line (M,(i + 1))) = m + 1 by A3, MATRIX_0:def 7;
then B5: len ((Line (M,(i + 1))) | 1) = 1 by NAT_1:11, FINSEQ_1:59;
1 <= width M by A3, NAT_1:11;
then B4: 1 in Seg (width M) by FINSEQ_1:1;
((Line (M,(i + 1))) | 1) . 1 = (Line (M,(i + 1))) . 1 by FINSEQ_3:112;
then (Line (M,(i + 1))) | (0 + 1) = <*(M * ((i + 1),1))*> by B5, B4, MATRIX_0:def 7, FINSEQ_1:40;
then B6: Sum ((Line (M,(i + 1))) | (0 + 1)) = M * ((i + 1),1) by RVSUM_1:73;
thus (Partial_Sums_in_cod2 Rseq) . (i,0) = Sum ((Line (M,(i + 1))) | (0 + 1)) by A1, B0, B2, B6; :: thesis: verum
end;
then P0: S1[ 0 ] ;
P1: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume C1: S1[k] ; :: thesis: S1[k + 1]
now :: thesis: ( (k + 1) + 1 <= width M implies (Partial_Sums_in_cod2 Rseq) . (i,(k + 1)) = Sum ((Line (M,(i + 1))) | ((k + 1) + 1)) )
assume C2: (k + 1) + 1 <= width M ; :: thesis: (Partial_Sums_in_cod2 Rseq) . (i,(k + 1)) = Sum ((Line (M,(i + 1))) | ((k + 1) + 1))
then C3: ( k + 1 <= (k + 1) + 1 & (k + 1) + 1 <= len (Line (M,(i + 1))) ) by MATRIX_0:def 7, NAT_1:11;
then C5: len ((Line (M,(i + 1))) | ((k + 1) + 1)) = (k + 1) + 1 by FINSEQ_1:59;
then (Line (M,(i + 1))) | ((k + 1) + 1) = (((Line (M,(i + 1))) | ((k + 1) + 1)) | (k + 1)) ^ <*(((Line (M,(i + 1))) | ((k + 1) + 1)) /. (len ((Line (M,(i + 1))) | ((k + 1) + 1))))*> by FINSEQ_5:21;
then C6: (Line (M,(i + 1))) | ((k + 1) + 1) = ((Line (M,(i + 1))) | (k + 1)) ^ <*(((Line (M,(i + 1))) | (k + 2)) /. (k + 2))*> by C5, FINSEQ_1:82, NAT_1:11;
1 <= (k + 1) + 1 by NAT_1:11;
then C7: k + 2 in Seg (width M) by C2, FINSEQ_1:1;
C8: k + 1 <= m by A3, C2, XREAL_1:6;
k + 2 in Seg (len ((Line (M,(i + 1))) | (k + 2))) by C5, FINSEQ_1:4;
then k + 2 in dom ((Line (M,(i + 1))) | (k + 2)) by FINSEQ_1:def 3;
then ((Line (M,(i + 1))) | (k + 2)) /. (k + 2) = ((Line (M,(i + 1))) | (k + 2)) . (k + 2) by PARTFUN1:def 6;
then ((Line (M,(i + 1))) | (k + 2)) /. (k + 2) = (Line (M,(i + 1))) . (k + 2) by FINSEQ_3:112;
then ((Line (M,(i + 1))) | (k + 2)) /. (k + 2) = M * ((i + 1),(k + 2)) by C7, MATRIX_0:def 7;
then Sum ((Line (M,(i + 1))) | ((k + 1) + 1)) = (Sum ((Line (M,(i + 1))) | (k + 1))) + (M * ((i + 1),(k + 2))) by C6, RVSUM_1:74;
then Sum ((Line (M,(i + 1))) | ((k + 1) + 1)) = ((Partial_Sums_in_cod2 Rseq) . (i,k)) + (Rseq . (i,(k + 1))) by C3, B0, A1, C8, C1, C2, XXREAL_0:2;
hence (Partial_Sums_in_cod2 Rseq) . (i,(k + 1)) = Sum ((Line (M,(i + 1))) | ((k + 1) + 1)) by DefCS; :: thesis: verum
end;
hence S1[k + 1] ; :: thesis: verum
end;
C9: m + 1 = len (Line (M,(i + 1))) by A3, MATRIX_0:def 7;
for k being Nat holds S1[k] from NAT_1:sch 2(P0, P1);
 then (Partial_Sums_in_cod2 Rseq) . (i,m) = Sum ((Line (M,(i + 1))) | (m + 1)) by A3;
then (Partial_Sums_in_cod2 Rseq) . (i,m) = Sum (Line (M,(i + 1))) by C9, FINSEQ_1:58;
hence (Partial_Sums_in_cod2 Rseq) . (i,m) = (LineSum M) . (i + 1) by B01, A2, MATRPROB:20; :: thesis: verum
end;
defpred S1[ Nat] means ( $1 <= n implies (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . ($1,m) = Sum ((LineSum M) | ($1 + 1)) );
now :: thesis: ( 0 <= n implies (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (0,m) = Sum ((LineSum M) | (0 + 1)) )
assume 0 <= n ; :: thesis: (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (0,m) = Sum ((LineSum M) | (0 + 1))
0 + 1 <= n + 1 by XREAL_1:6;
then 0 + 1 <= len (LineSum M) by A2, MATRPROB:20;
then len ((LineSum M) | (0 + 1)) = 1 by FINSEQ_1:59;
then D2: (LineSum M) | (0 + 1) = <*(((LineSum M) | (0 + 1)) . 1)*> by FINSEQ_1:40;
(Partial_Sums_in_cod2 Rseq) . (0,m) = (LineSum M) . (0 + 1) by X1;
then (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (0,m) = (LineSum M) . (0 + 1) by DefRS
.= Sum <*((LineSum M) . (0 + 1))*> by RVSUM_1:73 ;
hence (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (0,m) = Sum ((LineSum M) | (0 + 1)) by D2, FINSEQ_3:112; :: thesis: verum
end;
then P2: S1[ 0 ] ;
P3: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume E1: S1[k] ; :: thesis: S1[k + 1]
now :: thesis: ( k + 1 <= n implies (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . ((k + 1),m) = Sum ((LineSum M) | ((k + 1) + 1)) )
assume E2: k + 1 <= n ; :: thesis: (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . ((k + 1),m) = Sum ((LineSum M) | ((k + 1) + 1))
then ( k + 1 <= (k + 1) + 1 & (k + 1) + 1 <= n + 1 ) by NAT_1:11, XREAL_1:6;
then (k + 1) + 1 <= len (LineSum M) by A2, MATRPROB:20;
then E3: len ((LineSum M) | ((k + 1) + 1)) = (k + 1) + 1 by FINSEQ_1:59;
then E5: (LineSum M) | ((k + 1) + 1) = (((LineSum M) | ((k + 1) + 1)) | (k + 1)) ^ <*(((LineSum M) | ((k + 1) + 1)) /. (len ((LineSum M) | ((k + 1) + 1))))*> by FINSEQ_5:21
.= ((LineSum M) | (k + 1)) ^ <*(((LineSum M) | ((k + 1) + 1)) /. ((k + 1) + 1))*> by E3, NAT_1:11, FINSEQ_1:82 ;
E7: k <= k + 1 by NAT_1:11;
k + 2 in Seg (len ((LineSum M) | (k + 2))) by E3, FINSEQ_1:4;
then k + 2 in dom ((LineSum M) | (k + 2)) by FINSEQ_1:def 3;
then ((LineSum M) | (k + 2)) /. (k + 2) = ((LineSum M) | (k + 2)) . (k + 2) by PARTFUN1:def 6
.= (LineSum M) . (k + 2) by FINSEQ_3:112 ;
then Sum ((LineSum M) | ((k + 1) + 1)) = (Sum ((LineSum M) | (k + 1))) + ((LineSum M) . ((k + 1) + 1)) by E5, RVSUM_1:74
.= ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (k,m)) + ((Partial_Sums_in_cod2 Rseq) . ((k + 1),m)) by E1, E7, E2, X1, XXREAL_0:2 ;
hence (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . ((k + 1),m) = Sum ((LineSum M) | ((k + 1) + 1)) by DefRS; :: thesis: verum
end;
hence S1[k + 1] ; :: thesis: verum
end;
for k being Nat holds S1[k] from NAT_1:sch 2(P2, P3);
 then X2: (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (n,m) = Sum ((LineSum M) | (n + 1)) ;
len (LineSum M) = n + 1 by A2, MATRPROB:20;
then (LineSum M) | (n + 1) = LineSum M by FINSEQ_1:58;
then (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (n,m) = SumAll M by X2, MATRPROB:def 3;
hence (Partial_Sums Rseq) . (n,m) = SumAll M by th103; :: thesis: verum