A: (3 -Root 2) |^ (1 + 1) =
((3 -Root 2) |^ 1) * (3 -Root 2)
by NEWTON:6
.=
((1_ F_Real) * 3-Root(2)) * 3-Root(2)
.=
(((power F_Real) . (3-Root(2),0)) * 3-Root(2)) * 3-Root(2)
by GROUP_1:def 7
.=
((power F_Real) . (3-Root(2),(0 + 1))) * 3-Root(2)
by GROUP_1:def 7
.=
(power F_Real) . (3-Root(2),(1 + 1))
by GROUP_1:def 7
;
(3 -Root 2) |^ (2 + 1) =
((power F_Real) . (3-Root(2),2)) * 3-Root(2)
by A, NEWTON:6
.=
(power F_Real) . (3-Root(2),(2 + 1))
by GROUP_1:def 7
.=
3-Root(2) |^ 3
by BINOM:def 2
;
hence
3-Root(2) |^ 3 = 2
by PREPOWER:def 2; verum