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