let a, b, c be Real; ( (a ^2) + (b ^2) = 1 & - 1 < c & c < 1 implies 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 ) )
assume that
A1:
(a ^2) + (b ^2) = 1
and
A2:
( - 1 < c & c < 1 )
; 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 )
consider d being Real such that
A3:
(((((1 + (c * c)) * d) * d) - (2 * d)) + 1) - (d * d) = 0
by A2, Lem07;
reconsider e = ((d * c) * a) + ((1 - d) * (- b)), f = ((d * c) * b) + ((1 - d) * a) as Real ;
(e ^2) + (f ^2) =
(((d * c) ^2) * ((a ^2) + (b ^2))) + ((((1 - d) * b) ^2) + (((1 - d) * a) ^2))
.=
(((d * c) ^2) * 1) + (((1 - d) ^2) * 1)
by A1, Lem06
.=
d ^2
by A3
;
hence
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 )
; verum