[*1,0*] = [*1,0,0,0*] by Lm4;
then A1: 1q = [*1,0,0,0*] by ARYTM_0:def 5;
A2: Rea [*1,0,0,0*] = 1 by Th23;
A3: Im1 [*1,0,0,0*] = 0 by Th23;
A4: Im2 [*1,0,0,0*] = 0 by Th23;
Im3 [*1,0,0,0*] = 0 by Th23;
hence 1q *' = 1q by A1, A2, A3, A4, Th43; :: thesis: verum