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