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