let x, y be Element of REAL ; :: thesis: [*x,y,0,0*] = [*x,y*]
ex x9, y9 being Element of REAL st
( x9 = x & y9 = y & [*x,y,0,0*] = [*x9,y9*] ) by Def5;
hence [*x,y,0,0*] = [*x,y*] ; :: thesis: verum