0 = [*0 ,0 *] by ARYTM_0:def 7;
hence 0 = [*0 ,0 ,0 ,0 *] by Def6; :: thesis: verum