A1: (@ sin) |^ 2 =
(@ sin) |^ (1 + 1)
.=
((@ sin) |^ 1) * (@ sin)
by Th20
.=
(@ sin) * (@ sin)
by BINOM:8
;
A2: (@ sin) * (@ sin) =
(@ (@ sin)) (#) (@ (@ sin))
by Th13
.=
sin (#) sin
;
A4: (@ cos) * (@ cos) =
(@ (@ cos)) (#) (@ (@ cos))
by Th13
.=
cos (#) cos
;
A3: (@ cos) |^ 2 =
(@ cos) |^ (1 + 1)
.=
((@ cos) |^ 1) * (@ cos)
by Th20
.=
(@ cos) * (@ cos)
by BINOM:8
;
then ((@ sin) |^ 2) + ((@ cos) |^ 2) =
(@ ((@ sin) * (@ sin))) + (@ ((@ cos) * (@ cos)))
by Th18, A1
.=
((@ (@ sin)) (#) (@ (@ sin))) + (@ ((@ cos) * (@ cos)))
by Th13
.=
((@ (@ sin)) (#) (@ (@ sin))) + ((@ (@ cos)) (#) (@ (@ cos)))
by Th13
.=
(sin (#) sin) + (cos (#) cos)
;
hence
( ((@ sin) |^ 2) + ((@ cos) |^ 2) = 1. (RAlgebra REAL) & (@ sin) |^ 2 = sin (#) sin & (@ cos) |^ 2 = cos (#) cos & (@ sin) |^ 2 = (@ sin) * (@ sin) & (@ cos) |^ 2 = (@ cos) * (@ cos) )
by Th34, A1, A2, A3, A4; verum