2 |^ 3 = 2 |^ (2 + 1)
.= (2 |^ 2) * 2 by NEWTON:6
.= (2 ^2) * 2 by Lm1
.= 8 ;
hence 2 |^ 3 = 8 ; :: thesis: verum