theorem Th02: :: BKMODEL3:2

for a being non zero Real
for b, r being Real st r = sqrt ((a ^2) + (b ^2)) holds
( r is positive & ((a / r) ^2) + ((b / r) ^2) = 1 )