A: 0 in REAL ;
C: 0 = [*0 ,0 *] by ARYTM_0:def 7;
consider x', y' being Element of REAL such that
B: ( x' = 0 & y' = 0 & [*0 ,0 ,0 ,0 *] = [*x',y'*] ) by Def6;
thus 0 = [*0 ,0 ,0 ,0 *] by B, A, C, Def6; :: thesis: verum