theorem Th153: :: ZF_LANG1:153

for x1, x2, y1, y2 being Variable ex z1, z2 being Variable st (x1 '=' x2) / (y1,y2) = z1 '=' z2