[*1,0,0,0*] = [*1,0*] by Lm4;
hence [*1,0,0,0*] = 1 by ARYTM_0:def 5; :: thesis: verum