let t be commutative monotonic with-1-identity BinOp of [.0,1.]; for a being Element of [.0,1.] holds t . (a,0) = 0
let a be Element of [.0,1.]; 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
hence
t . (a,0) = 0
; verum