let u, u', v, v' be Real; :: thesis: ( u <> u' implies ex x being Real st (u * x) + v = (u' * x) + v' )
set x = (v' - v) / (u - u');
assume u <> u' ; :: thesis: ex x being Real st (u * x) + v = (u' * x) + v'
then u - u' <> 0 ;
then A1: (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 A1; :: thesis: verum