let Rseq1, Rseq2 be Function of [:NAT,NAT:],REAL; :: thesis: ( Partial_Sums_in_cod2 (Rseq1 + Rseq2) = (Partial_Sums_in_cod2 Rseq1) + (Partial_Sums_in_cod2 Rseq2) & Partial_Sums_in_cod1 (Rseq1 + Rseq2) = (Partial_Sums_in_cod1 Rseq1) + (Partial_Sums_in_cod1 Rseq2) )
set CS1 = Partial_Sums_in_cod2 Rseq1;
set CS2 = Partial_Sums_in_cod2 Rseq2;
set CS12 = Partial_Sums_in_cod2 (Rseq1 + Rseq2);
set RS1 = Partial_Sums_in_cod1 Rseq1;
set RS2 = Partial_Sums_in_cod1 Rseq2;
set RS12 = Partial_Sums_in_cod1 (Rseq1 + Rseq2);

now :: thesis: for n, m being Element of NAT holds (Partial_Sums_in_cod2 (Rseq1 + Rseq2)) . (n,m) = ((Partial_Sums_in_cod2 Rseq1) + (Partial_Sums_in_cod2 Rseq2)) . (n,m)

let n, m be Element of NAT ; :: thesis: (Partial_Sums_in_cod2 (Rseq1 + Rseq2)) . (n,m) = ((Partial_Sums_in_cod2 Rseq1) + (Partial_Sums_in_cod2 Rseq2)) . (n,m)
defpred S₁[ Nat] means (Partial_Sums_in_cod2 (Rseq1 + Rseq2)) . (n,$1) = ((Partial_Sums_in_cod2 Rseq1) . (n,$1)) + ((Partial_Sums_in_cod2 Rseq2) . (n,$1));
(Partial_Sums_in_cod2 (Rseq1 + Rseq2)) . (n,0) = (Rseq1 + Rseq2) . (n,0) by DefCS
.= (Rseq1 . (n,0)) + (Rseq2 . (n,0)) by lmADD
.= ((Partial_Sums_in_cod2 Rseq1) . (n,0)) + (Rseq2 . (n,0)) by DefCS ;
then a1: S₁[ 0 ] by DefCS;
a2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume a3: S₁[k] ; :: thesis: S₁[k + 1]
(Partial_Sums_in_cod2 (Rseq1 + Rseq2)) . (n,(k + 1)) = ((Partial_Sums_in_cod2 (Rseq1 + Rseq2)) . (n,k)) + ((Rseq1 + Rseq2) . (n,(k + 1))) by DefCS
.= (((Partial_Sums_in_cod2 Rseq1) . (n,k)) + ((Partial_Sums_in_cod2 Rseq2) . (n,k))) + ((Rseq1 . (n,(k + 1))) + (Rseq2 . (n,(k + 1)))) by a3, lmADD
.= ((((Partial_Sums_in_cod2 Rseq1) . (n,k)) + (Rseq1 . (n,(k + 1)))) + ((Partial_Sums_in_cod2 Rseq2) . (n,k))) + (Rseq2 . (n,(k + 1)))
.= (((Partial_Sums_in_cod2 Rseq1) . (n,(k + 1))) + ((Partial_Sums_in_cod2 Rseq2) . (n,k))) + (Rseq2 . (n,(k + 1))) by DefCS
.= ((Partial_Sums_in_cod2 Rseq1) . (n,(k + 1))) + (((Partial_Sums_in_cod2 Rseq2) . (n,k)) + (Rseq2 . (n,(k + 1)))) ;
hence S₁[k + 1] by DefCS; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(a1, a2);
then S₁[m] ;
hence (Partial_Sums_in_cod2 (Rseq1 + Rseq2)) . (n,m) = ((Partial_Sums_in_cod2 Rseq1) + (Partial_Sums_in_cod2 Rseq2)) . (n,m) by lmADD; :: thesis: verum

end;

hence Partial_Sums_in_cod2 (Rseq1 + Rseq2) = (Partial_Sums_in_cod2 Rseq1) + (Partial_Sums_in_cod2 Rseq2) by BINOP_1:2; :: thesis: Partial_Sums_in_cod1 (Rseq1 + Rseq2) = (Partial_Sums_in_cod1 Rseq1) + (Partial_Sums_in_cod1 Rseq2)

now :: thesis: for n, m being Element of NAT holds (Partial_Sums_in_cod1 (Rseq1 + Rseq2)) . (n,m) = ((Partial_Sums_in_cod1 Rseq1) + (Partial_Sums_in_cod1 Rseq2)) . (n,m)

let n, m be Element of NAT ; :: thesis: (Partial_Sums_in_cod1 (Rseq1 + Rseq2)) . (n,m) = ((Partial_Sums_in_cod1 Rseq1) + (Partial_Sums_in_cod1 Rseq2)) . (n,m)
defpred S₁[ Nat] means (Partial_Sums_in_cod1 (Rseq1 + Rseq2)) . ($1,m) = ((Partial_Sums_in_cod1 Rseq1) . ($1,m)) + ((Partial_Sums_in_cod1 Rseq2) . ($1,m));
(Partial_Sums_in_cod1 (Rseq1 + Rseq2)) . (0,m) = (Rseq1 + Rseq2) . (0,m) by DefRS
.= (Rseq1 . (0,m)) + (Rseq2 . (0,m)) by lmADD
.= ((Partial_Sums_in_cod1 Rseq1) . (0,m)) + (Rseq2 . (0,m)) by DefRS ;
then a4: S₁[ 0 ] by DefRS;
a5: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume a6: S₁[k] ; :: thesis: S₁[k + 1]
(Partial_Sums_in_cod1 (Rseq1 + Rseq2)) . ((k + 1),m) = ((Partial_Sums_in_cod1 (Rseq1 + Rseq2)) . (k,m)) + ((Rseq1 + Rseq2) . ((k + 1),m)) by DefRS
.= (((Partial_Sums_in_cod1 Rseq1) . (k,m)) + ((Partial_Sums_in_cod1 Rseq2) . (k,m))) + ((Rseq1 . ((k + 1),m)) + (Rseq2 . ((k + 1),m))) by a6, lmADD
.= ((((Partial_Sums_in_cod1 Rseq1) . (k,m)) + (Rseq1 . ((k + 1),m))) + ((Partial_Sums_in_cod1 Rseq2) . (k,m))) + (Rseq2 . ((k + 1),m))
.= (((Partial_Sums_in_cod1 Rseq1) . ((k + 1),m)) + ((Partial_Sums_in_cod1 Rseq2) . (k,m))) + (Rseq2 . ((k + 1),m)) by DefRS
.= ((Partial_Sums_in_cod1 Rseq1) . ((k + 1),m)) + (((Partial_Sums_in_cod1 Rseq2) . (k,m)) + (Rseq2 . ((k + 1),m))) ;
hence S₁[k + 1] by DefRS; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(a4, a5);
then S₁[n] ;
hence (Partial_Sums_in_cod1 (Rseq1 + Rseq2)) . (n,m) = ((Partial_Sums_in_cod1 Rseq1) + (Partial_Sums_in_cod1 Rseq2)) . (n,m) by lmADD; :: thesis: verum

end;

hence Partial_Sums_in_cod1 (Rseq1 + Rseq2) = (Partial_Sums_in_cod1 Rseq1) + (Partial_Sums_in_cod1 Rseq2) by BINOP_1:2; :: thesis: verum