set t = H₂(3);
<*H₂(3),H₂(3),H₂(3),H₂(3),H₂(3),H₂(3)*> " = <*(H₂(3) "),(H₂(3) "),(H₂(3) "),(H₂(3) "),(H₂(3) "),(H₂(3) ")*> by Th17;
hence Sum (<*H₂(3),H₂(3),H₂(3),H₂(3),H₂(3),H₂(3)*> ") = (((((H₂(3) ") + (H₂(3) ")) + (H₂(3) ")) + (H₂(3) ")) + (H₂(3) ")) + (H₂(3) ") by Th22
.= 1 by NUMPOLY1:13 ;
:: according to NUMBER17:def 6 :: thesis: verum