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