ex x9, y9 being Element of REAL st
( x9 = 0 & y9 = 0 & [*0 ,0 ,0 ,0 *] = [*x9,y9*] ) by Def6;
hence 0 = [*0 ,0 ,0 ,0 *] by ARYTM_0:def 7; :: thesis: verum