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