let z be Complex; :: thesis: z |^ 12 = ((((((((((z * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z
A1: 12 = 11 + 1 ;
z |^ 11 = (((((((((z * z) * z) * z) * z) * z) * z) * z) * z) * z) * z by Th1;
hence z |^ 12 = ((((((((((z * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z by A1, NEWTON:6; :: thesis: verum