theorem Th16: :: SURREALI:16

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
transitions_of (x,I1) = transitions_of (x,I2)