theorem :: BKMODEL1:16

for a, b, c being Real st (a ^2) + (b ^2) = 1 & - 1 < c & c < 1 holds
ex d, e, f being Real st
( e = ((d * c) * a) + ((1 - d) * (- b)) & f = ((d * c) * b) + ((1 - d) * a) & (e ^2) + (f ^2) = d ^2 )