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