theorem Th17: :: SURREALI:17

for Z being set
for I1, I2 being Function
for x being object st ((L_ x) \/ (R_ x)) \ {0_No} c= Z & I1 | Z = I2 | Z holds
( divL (x,I1) = divL (x,I2) & divR (x,I1) = divR (x,I2) )