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