for x, y being Element of REAL holds [*x,y,0,0*] = [*x,y*] by Lm3;