let a, b be Element of [.0,1.]; :: thesis: (1 - a) + (a * b) in [.0,1.]
1 - a in [.0,1.] by FUZNORM1:7;
then A0: 1 - a >= 0 by XXREAL_1:1;
a * b in [.0,1.] by FUZNORM1:3;
then a1: a * b >= 0 by XXREAL_1:1;
b <= 1 by XXREAL_1:1;
then a2: b - 1 <= 1 - 1 by XREAL_1:9;
a >= 0 by XXREAL_1:1;
then a * (b - 1) <= 0 by a2;
then 1 + ((a * b) - a) <= 1 + 0 by XREAL_1:7;
hence (1 - a) + (a * b) in [.0,1.] by a1, A0, XXREAL_1:1; :: thesis: verum