let u, u9, v, v9 be Real; :: thesis: ( u <> u9 implies ex x being Real st (u * x) + v = (u9 * x) + v9 )
set x = (v9 - v) / (u - u9);
assume u <> u9 ; :: thesis: ex x being Real st (u * x) + v = (u9 * x) + v9
then u - u9 <> 0 ;
then A1: (u - u9) * ((v9 - v) / (u - u9)) = v9 - v by XCMPLX_1:87;
reconsider x = (v9 - v) / (u - u9) as Real ;
take x ; :: thesis: (u * x) + v = (u9 * x) + v9
thus (u * x) + v = (u9 * x) + v9 by A1; :: thesis: verum