let z be Complex; :: thesis: z |^ 20 = ((((((((((((((((((z * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z
A1: 20 = 19 + 1 ;
z |^ 19 = (((((((((((((((((z * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z by Th9;
hence z |^ 20 = ((((((((((((((((((z * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z by A1, NEWTON:6; :: thesis: verum