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