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

proof

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

end;

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