let c be Complex; :: thesis: c |^ 9 = (((((((c * c) * c) * c) * c) * c) * c) * c) * c
A1: 9 = 8 + 1 ;
c |^ 8 = ((((((c * c) * c) * c) * c) * c) * c) * c by Th4;
hence c |^ 9 = (((((((c * c) * c) * c) * c) * c) * c) * c) * c by A1, NEWTON:6; :: thesis: verum