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