let x1, x2, x3 be Real; ( sin x1 <> 0 & sin x2 <> 0 & sin x3 <> 0 implies sin ((x1 + x2) + x3) = (((sin x1) * (sin x2)) * (sin x3)) * (((((cot x2) * (cot x3)) + ((cot x1) * (cot x3))) + ((cot x1) * (cot x2))) - 1) )
assume that
A1:
sin x1 <> 0
and
A2:
sin x2 <> 0
and
A3:
sin x3 <> 0
; sin ((x1 + x2) + x3) = (((sin x1) * (sin x2)) * (sin x3)) * (((((cot x2) * (cot x3)) + ((cot x1) * (cot x3))) + ((cot x1) * (cot x2))) - 1)
sin ((x1 + x2) + x3) =
sin (x1 + (x2 + x3))
.=
((sin x1) * (cos (x2 + x3))) + ((cos x1) * (sin (x2 + x3)))
by SIN_COS:75
.=
((sin x1) * (((cos x2) * (cos x3)) - ((sin x2) * (sin x3)))) + ((cos x1) * (sin (x2 + x3)))
by SIN_COS:75
.=
(((sin x1) * ((cos x2) * (cos x3))) - ((sin x1) * ((sin x2) * (sin x3)))) + ((cos x1) * (((sin x2) * (cos x3)) + ((cos x2) * (sin x3))))
by SIN_COS:75
.=
((((sin x1) * (cos x2)) * (cos x3)) - (((sin x1) * (sin x2)) * (sin x3))) + ((((cos x1) * (sin x2)) * (cos x3)) + (((cos x1) * (cos x2)) * (sin x3)))
.=
((((sin x1) * ((sin x2) * (cot x2))) * (cos x3)) - (((sin x1) * (sin x2)) * (sin x3))) + ((((cos x1) * (sin x2)) * (cos x3)) + (((cos x1) * (cos x2)) * (sin x3)))
by A2, Th2
.=
((((sin x1) * ((sin x2) * (cot x2))) * ((sin x3) * (cot x3))) - (((sin x1) * (sin x2)) * (sin x3))) + ((((cos x1) * (sin x2)) * (cos x3)) + (((cos x1) * (cos x2)) * (sin x3)))
by A3, Th2
.=
((((sin x1) * (sin x2)) * (sin x3)) * (((cot x2) * (cot x3)) - 1)) + (((((sin x1) * (cot x1)) * (sin x2)) * (cos x3)) + (((cos x1) * (cos x2)) * (sin x3)))
by A1, Th2
.=
((((sin x1) * (sin x2)) * (sin x3)) * (((cot x2) * (cot x3)) - 1)) + (((((sin x1) * (cot x1)) * (sin x2)) * ((sin x3) * (cot x3))) + (((cos x1) * (cos x2)) * (sin x3)))
by A3, Th2
.=
(((((sin x1) * (sin x2)) * (sin x3)) * (((cot x2) * (cot x3)) - 1)) + (((((sin x1) * (sin x2)) * (sin x3)) * (cot x1)) * (cot x3))) + (((cos x1) * (cos x2)) * (sin x3))
.=
((((sin x1) * (sin x2)) * (sin x3)) * ((((cot x2) * (cot x3)) - 1) + ((cot x1) * (cot x3)))) + ((((sin x1) * (cot x1)) * (cos x2)) * (sin x3))
by A1, Th2
.=
((((sin x1) * (sin x2)) * (sin x3)) * ((((cot x2) * (cot x3)) - 1) + ((cot x1) * (cot x3)))) + ((((sin x1) * (cot x1)) * ((sin x2) * (cot x2))) * (sin x3))
by A2, Th2
.=
(((sin x1) * (sin x2)) * (sin x3)) * (((((cot x2) * (cot x3)) + ((cot x1) * (cot x3))) + ((cot x1) * (cot x2))) - 1)
;
hence
sin ((x1 + x2) + x3) = (((sin x1) * (sin x2)) * (sin x3)) * (((((cot x2) * (cot x3)) + ((cot x1) * (cot x3))) + ((cot x1) * (cot x2))) - 1)
; verum