for x, y being Element of 1 holds Empty^2-to-zero . (x,y) = Empty^2-to-zero . (y,x) by Lm4;