let x, y be Element of REAL ; :: thesis: [*x,y,0 ,0 *] = [*x,y*]
consider x', y' being Element of REAL such that
A1: ( x' = x & y' = y & [*x,y,0 ,0 *] = [*x',y'*] ) by Def6;
thus [*x,y,0 ,0 *] = [*x,y*] by A1; :: thesis: verum