for x, y, z being Element of 2 holds Set_to_zero . (x,z) <= (Set_to_zero . (x,y)) + (Set_to_zero . (y,z))