thus 0 = [\0/] by INT_1:47
.= [\(log (2,1))/] by POWER:59 ; :: thesis: verum