let T1, T2 be _Theta; :: thesis: for epsilon1, epsilon2 being Real st 0 <= epsilon1 & 0 <= epsilon2 holds
ex T being _Theta st (T1 * epsilon1) + (T2 * epsilon2) = T * (epsilon1 + epsilon2)
let epsilon1, epsilon2 be Real; :: thesis: ( 0 <= epsilon1 & 0 <= epsilon2 implies ex T being _Theta st (T1 * epsilon1) + (T2 * epsilon2) = T * (epsilon1 + epsilon2) )
assume A1: ( 0 <= epsilon1 & 0 <= epsilon2 ) ; :: thesis: ex T being _Theta st (T1 * epsilon1) + (T2 * epsilon2) = T * (epsilon1 + epsilon2)
reconsider I = 1 as _Theta by Def1;
( - 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 ( ((- 1) * epsilon1) + ((- 1) * epsilon2) <= (T1 * epsilon1) + (T2 * epsilon2) & (T1 * epsilon1) + (T2 * epsilon2) <= (1 * epsilon1) + (1 * epsilon2) ) by XREAL_1:7;
then ( (- I) * (epsilon1 + epsilon2) <= (T1 * epsilon1) + (T2 * epsilon2) & (T1 * epsilon1) + (T2 * epsilon2) <= I * (epsilon1 + epsilon2) ) ;
hence ex T being _Theta st (T1 * epsilon1) + (T2 * epsilon2) = T * (epsilon1 + epsilon2) by Th4; :: thesis: verum