let r, s be Sequence of REAL ; :: thesis: 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
let y, z, yz be strictly_decreasing Surreal-Sequence; :: thesis: 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
let S, T be non empty Ordinal; :: thesis: ( y = {} & dom z c= T implies Sum ((Sum (y,z,yz,r,s,S,T)),(No_omega^ yz)) = 0_No )
assume ( y = {} & dom z c= T ) ; :: thesis: Sum ((Sum (y,z,yz,r,s,S,T)),(No_omega^ yz)) = 0_No
then rng (Sum (y,z,yz,r,s,S,T)) c= {0} by Th91;
hence Sum ((Sum (y,z,yz,r,s,S,T)),(No_omega^ yz)) = 0_No by Th66; :: thesis: verum