let T1, T2 be _Theta; :: thesis: for lambda, epsilon1, epsilon2 being Real st lambda = (1 + (T1 * epsilon1)) * (1 + (T2 * epsilon2)) & 0 <= epsilon1 & epsilon1 <= 1 & 0 <= epsilon2 holds
ex T being _Theta st lambda = 1 + (T * (epsilon1 + (2 * epsilon2)))
let lambda, epsilon1, epsilon2 be Real; :: thesis: ( lambda = (1 + (T1 * epsilon1)) * (1 + (T2 * epsilon2)) & 0 <= epsilon1 & epsilon1 <= 1 & 0 <= epsilon2 implies ex T being _Theta st lambda = 1 + (T * (epsilon1 + (2 * epsilon2))) )
assume A1: ( lambda = (1 + (T1 * epsilon1)) * (1 + (T2 * epsilon2)) & 0 <= epsilon1 & epsilon1 <= 1 & 0 <= epsilon2 ) ; :: thesis: ex T being _Theta st lambda = 1 + (T * (epsilon1 + (2 * epsilon2)))
reconsider epsilon1 = epsilon1 as _Theta by A1, Def1;
set ep = epsilon1 + (2 * epsilon2);

per cases ( epsilon1 + (2 * epsilon2) = 0 or epsilon1 + (2 * epsilon2) <> 0 ) ;

suppose epsilon1 + (2 * epsilon2) = 0 ; :: thesis: ex T being _Theta st lambda = 1 + (T * (epsilon1 + (2 * epsilon2)))

then A2: ( epsilon1 = 0 & 2 * epsilon2 = 0 ) by A1;
take T = 0 ; :: thesis: lambda = 1 + (T * (epsilon1 + (2 * epsilon2)))
thus lambda = 1 + (T * (epsilon1 + (2 * epsilon2))) by A2, A1; :: thesis: verum

end;

suppose A3: epsilon1 + (2 * epsilon2) <> 0 ; :: thesis: ex T being _Theta st lambda = 1 + (T * (epsilon1 + (2 * epsilon2)))

( - 1 <= T1 & T1 <= 1 & - 1 <= T2 & T2 <= 1 ) by Def1;
then ( (- 1) * epsilon1 <= T1 * epsilon1 & T1 * epsilon1 <= 1 * epsilon1 & (- 1) * epsilon2 <= T2 * epsilon2 & T2 * epsilon2 <= 1 * epsilon2 ) by A1, XREAL_1:64;
then A4: ( ((- 1) * epsilon1) + ((- 1) * epsilon2) <= (T1 * epsilon1) + (T2 * epsilon2) & (T1 * epsilon1) + (T2 * epsilon2) <= epsilon1 + epsilon2 ) by XREAL_1:7;
( - 1 <= (T1 * T2) * epsilon1 & (T1 * T2) * epsilon1 <= 1 ) by Def1;
then ( (- 1) * epsilon2 <= ((T1 * T2) * epsilon1) * epsilon2 & ((T1 * T2) * epsilon1) * epsilon2 <= 1 * epsilon2 ) by A1, XREAL_1:64;
then ( (((- 1) * epsilon1) + ((- 1) * epsilon2)) + ((- 1) * epsilon2) <= ((T1 * epsilon1) + (T2 * epsilon2)) + (((T1 * T2) * epsilon1) * epsilon2) & ((T1 * epsilon1) + (T2 * epsilon2)) + (((T1 * T2) * epsilon1) * epsilon2) <= (epsilon1 + epsilon2) + epsilon2 ) by A4, XREAL_1:7;
then ( (- 1) * (epsilon1 + (2 * epsilon2)) <= ((T1 * epsilon1) + (T2 * epsilon2)) + (((T1 * T2) * epsilon1) * epsilon2) & ((T1 * epsilon1) + (T2 * epsilon2)) + (((T1 * T2) * epsilon1) * epsilon2) <= 1 * (epsilon1 + (2 * epsilon2)) ) ;
then ( - 1 <= (((T1 * epsilon1) + (T2 * epsilon2)) + (((T1 * T2) * epsilon1) * epsilon2)) / (epsilon1 + (2 * epsilon2)) & (((T1 * epsilon1) + (T2 * epsilon2)) + (((T1 * T2) * epsilon1) * epsilon2)) / (epsilon1 + (2 * epsilon2)) <= 1 ) by A3, A1, XREAL_1:77, XREAL_1:79;
then reconsider T = (((T1 * epsilon1) + (T2 * epsilon2)) + (((T1 * T2) * epsilon1) * epsilon2)) / (epsilon1 + (2 * epsilon2)) as _Theta by Def1;
take T ; :: thesis: lambda = 1 + (T * (epsilon1 + (2 * epsilon2)))
T * (epsilon1 + (2 * epsilon2)) = ((T1 * epsilon1) + (T2 * epsilon2)) + (((T1 * T2) * epsilon1) * epsilon2) by A3, XCMPLX_1:87;
hence lambda = 1 + (T * (epsilon1 + (2 * epsilon2))) by A1; :: thesis: verum

end;

end;