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