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

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