let r, s, t, d be Real; :: thesis: ( (sin (2 * s)) * (cos d) = cos (2 * t) implies (((r * (cos s)) ^2) + ((r * (sin s)) ^2)) - (((2 * (r * (cos s))) * (r * (sin s))) * (cos d)) = (2 * (r ^2)) * ((sin t) ^2) )
assume A1: (sin (2 * s)) * (cos d) = cos (2 * t) ; :: thesis: (((r * (cos s)) ^2) + ((r * (sin s)) ^2)) - (((2 * (r * (cos s))) * (r * (sin s))) * (cos d)) = (2 * (r ^2)) * ((sin t) ^2)
(((r * (cos s)) ^2) + ((r * (sin s)) ^2)) - (((2 * (r * (cos s))) * (r * (sin s))) * (cos d)) = (((r * (cos s)) * (r * (cos s))) + ((r * (sin s)) ^2)) - (((2 * (r * (cos s))) * (r * (sin s))) * (cos d)) by SQUARE_1:def 1
.= (((r * (cos s)) * (r * (cos s))) + ((r * (sin s)) * (r * (sin s)))) - (((2 * (r * (cos s))) * (r * (sin s))) * (cos d)) by SQUARE_1:def 1
.= ((r * r) * (((cos s) * (cos s)) + ((sin s) * (sin s)))) - (((((r * 2) * r) * (cos s)) * (sin s)) * (cos d))
.= ((r * r) * 1) - (((((r * 2) * r) * (cos s)) * (sin s)) * (cos d)) by SIN_COS:29
.= (r ^2) - (((((r * r) * 2) * (cos s)) * (sin s)) * (cos d)) by SQUARE_1:def 1
.= (r ^2) - (((((r ^2) * 2) * (cos s)) * (sin s)) * (cos d)) by SQUARE_1:def 1
.= (r ^2) - (((r ^2) * ((2 * (sin s)) * (cos s))) * (cos d))
.= (r ^2) - (((r ^2) * (sin (2 * s))) * (cos d)) by SIN_COS5:5
.= (r ^2) - ((r ^2) * (cos (2 * t))) by A1
.= (r ^2) - ((r ^2) * (((cos t) ^2) - ((sin t) ^2))) by SIN_COS5:7
.= (r ^2) * (1 - (((cos t) ^2) - ((sin t) ^2)))
.= (r ^2) * ((((cos t) ^2) + ((sin t) ^2)) - (((cos t) ^2) - ((sin t) ^2))) by SIN_COS:29
.= (2 * (r ^2)) * ((sin t) ^2) ;
hence (((r * (cos s)) ^2) + ((r * (sin s)) ^2)) - (((2 * (r * (cos s))) * (r * (sin s))) * (cos d)) = (2 * (r ^2)) * ((sin t) ^2) ; :: thesis: verum