let z be Complex; :: thesis: z |^ 17 = (((((((((((((((z * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z
A1: 17 = 16 + 1 ;
z |^ 16 = ((((((((((((((z * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z by Th6;
hence z |^ 17 = (((((((((((((((z * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z by A1, NEWTON:6; :: thesis: verum