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