let T be _Theta; :: thesis: for lambda, epsilon1, epsilon2 being Real st lambda = T * epsilon1 & |.epsilon1.| <= |.epsilon2.| holds
ex T1 being _Theta st lambda = T1 * epsilon2
let lambda, epsilon1, epsilon2 be Real; :: thesis: ( lambda = T * epsilon1 & |.epsilon1.| <= |.epsilon2.| implies ex T1 being _Theta st lambda = T1 * epsilon2 )
assume A1: ( lambda = T * epsilon1 & |.epsilon1.| <= |.epsilon2.| ) ; :: thesis: ex T1 being _Theta st lambda = T1 * epsilon2

per cases ( epsilon2 = 0 or epsilon2 > 0 or epsilon2 < 0 ) ;

suppose A2: epsilon2 = 0 ; :: thesis: ex T1 being _Theta st lambda = T1 * epsilon2

take T1 = 0 ; :: thesis: lambda = T1 * epsilon2
epsilon1 = 0 by A2, A1;
hence lambda = T1 * epsilon2 by A1; :: thesis: verum

end;

suppose A3: epsilon2 > 0 ; :: thesis: ex T1 being _Theta st lambda = T1 * epsilon2

then A4: |.epsilon2.| = epsilon2 by ABSVALUE:def 1;

per cases ( epsilon1 >= 0 or epsilon1 < 0 ) ;

suppose A5: epsilon1 >= 0 ; :: thesis: ex T1 being _Theta st lambda = T1 * epsilon2

then |.epsilon1.| = epsilon1 by ABSVALUE:def 1;
then reconsider T1 = epsilon1 / epsilon2 as _Theta by Def1, XREAL_1:183, A5, A1, A4;
take TT = T * T1; :: thesis: lambda = TT * epsilon2
thus TT * epsilon2 = T * ((epsilon1 / epsilon2) * epsilon2)
.= lambda by A1, XCMPLX_1:87, A3 ; :: thesis: verum

end;

suppose A6: epsilon1 < 0 ; :: thesis: ex T1 being _Theta st lambda = T1 * epsilon2

then A7: - epsilon1 > 0 ;
|.epsilon1.| = - epsilon1 by A6, ABSVALUE:def 1;
then A8: (- epsilon1) / epsilon2 is theta by XREAL_1:183, A7, A1, A4;
- ((- epsilon1) / epsilon2) = - (- (epsilon1 / epsilon2)) by XCMPLX_1:187;
then reconsider T1 = epsilon1 / epsilon2 as _Theta by A8;
take TT = T * T1; :: thesis: lambda = TT * epsilon2
thus TT * epsilon2 = T * ((epsilon1 / epsilon2) * epsilon2)
.= lambda by A1, XCMPLX_1:87, A3 ; :: thesis: verum

end;

end;

end;

suppose A9: epsilon2 < 0 ; :: thesis: ex T1 being _Theta st lambda = T1 * epsilon2

then A10: |.epsilon2.| = - epsilon2 by ABSVALUE:def 1;

per cases ( epsilon1 >= 0 or epsilon1 < 0 ) ;

suppose A11: epsilon1 >= 0 ; :: thesis: ex T1 being _Theta st lambda = T1 * epsilon2

then |.epsilon1.| = epsilon1 by ABSVALUE:def 1;
then A12: epsilon1 / (- epsilon2) is theta by XREAL_1:183, A11, A1, A10;
- (epsilon1 / (- epsilon2)) = - (- (epsilon1 / epsilon2)) by XCMPLX_1:188;
then reconsider T1 = epsilon1 / epsilon2 as _Theta by A12;
take TT = T * T1; :: thesis: lambda = TT * epsilon2
thus TT * epsilon2 = T * ((epsilon1 / epsilon2) * epsilon2)
.= lambda by A1, XCMPLX_1:87, A9 ; :: thesis: verum

end;

suppose A13: epsilon1 < 0 ; :: thesis: ex T1 being _Theta st lambda = T1 * epsilon2

then A14: - epsilon1 > 0 ;
|.epsilon1.| = - epsilon1 by A13, ABSVALUE:def 1;
then (- epsilon1) / (- epsilon2) is theta by XREAL_1:183, A14, A1, A10;
then reconsider T1 = epsilon1 / epsilon2 as _Theta by XCMPLX_1:191;
take TT = T * T1; :: thesis: lambda = TT * epsilon2
thus TT * epsilon2 = T * ((epsilon1 / epsilon2) * epsilon2)
.= lambda by XCMPLX_1:87, A9, A1 ; :: thesis: verum

end;

end;

end;

end;