let x be Real; :: thesis: (cos x) |^ 3 = ((3 * (cos x)) + (cos (3 * x))) / 4
((3 * (cos x)) + (cos (3 * x))) / 4 = ((3 * (cos x)) + ((4 * ((cos x) |^ 3)) - (3 * (cos x)))) / 4 by Th17
.= (4 * ((cos x) |^ 3)) / 4 ;
hence (cos x) |^ 3 = ((3 * (cos x)) + (cos (3 * x))) / 4 ; :: thesis: verum