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