theorem :: BKMODEL1:11

for a, b being Real st a <> 0 & b ^2 = 1 + (a * a) holds
(((a * (1 / b)) * a) * ((- 1) / b)) + ((1 / b) * ((- 1) / b)) = - 1