let a, b, c be Real; :: thesis: ( (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 ) ; :: thesis: 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 ) ; :: thesis: verum