Let $\sin$ be the D1931: Standard real sine function.
Let $\cos$ be the D1927: Standard real cosine function.
Let $x \in \mathbb{R}$ be a D993: Real number.
Let $\cos$ be the D1927: Standard real cosine function.
Let $x \in \mathbb{R}$ be a D993: Real number.
Then
\begin{equation}
\sin^2 x + \cos^2 x
= 1
\end{equation}