thus (2 |^ 65536) - 3 = (2 |^|^ (2 + 3)) - 3 by Lm1, Lm3, Lm4, Th5
.= H₁(4,2) by Th12 ; :: thesis: verum