theorem :: SURREAL1:97

for r, s being Sequence of REAL
for y, z, yz being strictly_decreasing Surreal-Sequence
for S, T being non empty Ordinal st y = {} & dom z c= T holds
Sum ((Sum (y,z,yz,r,s,S,T)),(No_omega^ yz)) = 0_No