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