let x be Real; :: thesis: (sin x) |^ 4 = ((3 - (4 * (cos (2 * x)))) + (cos (4 * x))) / 8
((3 - (4 * (cos (2 * x)))) + (cos ((2 * 2) * x))) / 8 = ((3 - (4 * (cos (2 * x)))) + (cos (2 * (2 * x)))) / 8
.= ((3 - (4 * (cos (2 * x)))) + (1 - (2 * ((sin (2 * x)) ^2)))) / 8 by Th7
.= ((3 - (4 * (cos (2 * x)))) + (1 - (2 * (((2 * (sin x)) * (cos x)) ^2)))) / 8 by Th5
.= ((3 - (4 * (1 - (2 * ((sin x) ^2))))) + (1 - ((8 * ((sin x) ^2)) * ((cos x) ^2)))) / 8 by Th7
.= ((sin x) ^2) * (1 - ((cos x) * (cos x)))
.= ((sin x) * (sin x)) * ((sin x) * (sin x)) by SIN_COS4:4
.= (((sin x) |^ 1) * (sin x)) * ((sin x) * (sin x))
.= ((sin x) |^ (1 + 1)) * ((sin x) * (sin x)) by NEWTON:6
.= (((sin x) |^ (1 + 1)) * (sin x)) * (sin x)
.= ((sin x) |^ (2 + 1)) * (sin x) by NEWTON:6
.= (sin x) |^ (3 + 1) by NEWTON:6 ;
hence (sin x) |^ 4 = ((3 - (4 * (cos (2 * x)))) + (cos (4 * x))) / 8 ; :: thesis: verum