theorem Th30: :: SURREALI:30

for x, y, x1, y1, Ix1 being Surreal st x1 * Ix1 == 1_No holds
((x1 * y) + (x * y1)) - (x1 * y1) == 1_No + (x1 * (y - ((1_No + ((x1 - x) * y1)) * Ix1)))