let t be commutative monotonic with-1-identity BinOp of [.0,1.]; :: thesis: for a being Element of [.0,1.] holds t . (a,0) = 0
let a be Element of [.0,1.]; :: thesis: t . (a,0) = 0
T0: ( 0 in [.0,1.] & 1 in [.0,1.] ) by XXREAL_1:1;
then T3: t . (1,0) = t . (0,1) by BINOP_1:def 2
.= 0 by T0, IdDef ;
for a being Element of [.0,1.] holds t . (a,0) = 0

proof

let a be Element of [.0,1.]; :: thesis: t . (a,0) = 0
t . (a,0) in [.0,1.] by NormIn01;
then T4: 0 <= t . (a,0) by XXREAL_1:1;
a <= 1 by XXREAL_1:1;
hence t . (a,0) = 0 by T4, T0, MonDef, T3; :: thesis: verum

end;

hence t . (a,0) = 0 ; :: thesis: verum