reconsider z = zeta as Complex ;
zeta |^ (1 + 1) = zeta * zeta by lemI;
then A: zeta |^ 2 = z ^2 by SQUARE_1:def 1;
B: zeta |^ 2 = zeta ^2 by lemI;
zeta |^ 3 = z |^ 3 by lem3c;
hence zeta is CRoot of 3,1 by LZ23, COMPTRIG:def 2; :: thesis: zeta ^2 is CRoot of 3,1
(z ^2) |^ 3 = (z * z) |^ 3 by SQUARE_1:def 1
.= (z |^ 3) * (z |^ 3) by NEWTON:7
.= (z |^ 3) ^2 by SQUARE_1:def 1
.= 1 ^2 by LZ23, lem3c
.= 1 * 1 by SQUARE_1:def 1 ;
hence zeta ^2 is CRoot of 3,1 by A, B, COMPTRIG:def 2; :: thesis: verum