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