[*1,0 *] = [*1,0 ,0 ,0 *] by Lm4;
then A1: 1q = [*1,0 ,0 ,0 *] by ARYTM_0:def 7;
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