let a be Surreal; :: thesis: for r1, r2, s being Sequence of REAL
for y, z being strictly_decreasing Surreal-Sequence
for S, T being non empty Ordinal
for r12 being Sequence of REAL st r1 ^ r2 = r12 & dom y c= dom r1 & dom y c= S & dom z c= T holds
Partial_Sums (y,z,r1,s,a,S,T) = Partial_Sums (y,z,r12,s,a,S,T)
let r1, r2, s be Sequence of REAL ; :: thesis: for y, z being strictly_decreasing Surreal-Sequence
for S, T being non empty Ordinal
for r12 being Sequence of REAL st r1 ^ r2 = r12 & dom y c= dom r1 & dom y c= S & dom z c= T holds
Partial_Sums (y,z,r1,s,a,S,T) = Partial_Sums (y,z,r12,s,a,S,T)
let y, z be strictly_decreasing Surreal-Sequence; :: thesis: for S, T being non empty Ordinal
for r12 being Sequence of REAL st r1 ^ r2 = r12 & dom y c= dom r1 & dom y c= S & dom z c= T holds
Partial_Sums (y,z,r1,s,a,S,T) = Partial_Sums (y,z,r12,s,a,S,T)
let S, T be non empty Ordinal; :: thesis: for r12 being Sequence of REAL st r1 ^ r2 = r12 & dom y c= dom r1 & dom y c= S & dom z c= T holds
Partial_Sums (y,z,r1,s,a,S,T) = Partial_Sums (y,z,r12,s,a,S,T)
let r12 be Sequence of REAL ; :: thesis: ( r1 ^ r2 = r12 & dom y c= dom r1 & dom y c= S & dom z c= T implies Partial_Sums (y,z,r1,s,a,S,T) = Partial_Sums (y,z,r12,s,a,S,T) )
assume A1: ( r1 ^ r2 = r12 & dom y c= dom r1 & dom y c= S & dom z c= T ) ; :: thesis: Partial_Sums (y,z,r1,s,a,S,T) = Partial_Sums (y,z,r12,s,a,S,T)
set S1 = (y,z,S,T) += a;
set AD1 = Product (r1,s,S,T);
set AD12 = Product (r12,s,S,T);
A2: (y,z,S,T) += a c= [:S,T:] by FINSUB_1:def 5;
( dom (Product (r12,s,S,T)) = [:S,T:] & dom (Product (r1,s,S,T)) = [:S,T:] ) by FUNCT_2:def 1;
then A3: ( dom ((Product (r12,s,S,T)) | ((y,z,S,T) += a)) = (y,z,S,T) += a & (y,z,S,T) += a = dom ((Product (r1,s,S,T)) | ((y,z,S,T) += a)) ) by A2, RELAT_1:62;
for x being object st x in (y,z,S,T) += a holds
((Product (r12,s,S,T)) | ((y,z,S,T) += a)) . x = ((Product (r1,s,S,T)) | ((y,z,S,T) += a)) . x

proof

let x be object ; :: thesis: ( x in (y,z,S,T) += a implies ((Product (r12,s,S,T)) | ((y,z,S,T) += a)) . x = ((Product (r1,s,S,T)) | ((y,z,S,T) += a)) . x )
assume A4: x in (y,z,S,T) += a ; :: thesis: ((Product (r12,s,S,T)) | ((y,z,S,T) += a)) . x = ((Product (r1,s,S,T)) | ((y,z,S,T) += a)) . x
consider i, j being object such that
A5: ( i in S & j in T & x = [i,j] ) by A2, A4, ZFMISC_1:def 2;
reconsider i = i, j = j as Ordinal by A5;
A6: ( i in dom y & j in dom z & (y .. i) + (z .. j) == a ) by A5, A1, A4, Def16;
( ((Product (r12,s,S,T)) | ((y,z,S,T) += a)) . x = (Product (r12,s,S,T)) . x & (Product (r12,s,S,T)) . x = (Product (r12,s,S,T)) . (i,j) ) by A4, A5, FUNCT_1:49, BINOP_1:def 1;
then A7: ((Product (r12,s,S,T)) | ((y,z,S,T) += a)) . x = (r12 . i) * (s . j) by A5, Def15;
( ((Product (r1,s,S,T)) | ((y,z,S,T) += a)) . x = (Product (r1,s,S,T)) . x & (Product (r1,s,S,T)) . x = (Product (r1,s,S,T)) . (i,j) ) by A4, A5, FUNCT_1:49, BINOP_1:def 1;
then ((Product (r1,s,S,T)) | ((y,z,S,T) += a)) . x = (r1 . i) * (s . j) by A5, Def15;
hence ((Product (r12,s,S,T)) | ((y,z,S,T) += a)) . x = ((Product (r1,s,S,T)) | ((y,z,S,T) += a)) . x by A7, A1, A6, ORDINAL4:def 1; :: thesis: verum

end;

then (Product (r12,s,S,T)) | ((y,z,S,T) += a) = (Product (r1,s,S,T)) | ((y,z,S,T) += a) by A3, FUNCT_1:2;
hence Partial_Sums (y,z,r1,s,a,S,T) = Partial_Sums (y,z,r12,s,a,S,T) by SETWOP_2:7; :: thesis: verum