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

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

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