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

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

hence
t . (a,1) = 1
; :: thesis: verum
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;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