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