set f = conorm t;
A1: for a, b being Element of [.0,1.] holds (conorm t) . (a,b) = (conorm t) . (b,a)

proof

let a, b be Element of [.0,1.]; :: thesis: (conorm t) . (a,b) = (conorm t) . (b,a)
A2: ( 1 - a in [.0,1.] & 1 - b in [.0,1.] ) by OpIn01;
(conorm t) . (a,b) = 1 - (t . ((1 - a),(1 - b))) by CoDef
.= 1 - (t . ((1 - b),(1 - a))) by A2, BINOP_1:def 2
.= (conorm t) . (b,a) by CoDef ;
hence (conorm t) . (a,b) = (conorm t) . (b,a) ; :: thesis: verum

end;

C1: for a, b, c being Element of [.0,1.] holds (conorm t) . (((conorm t) . (a,b)),c) = (conorm t) . (a,((conorm t) . (b,c)))

proof

let a, b, c be Element of [.0,1.]; :: thesis: (conorm t) . (((conorm t) . (a,b)),c) = (conorm t) . (a,((conorm t) . (b,c)))
A2: ( 1 - a in [.0,1.] & 1 - b in [.0,1.] & 1 - c in [.0,1.] ) by OpIn01;
set A = 1 - (t . ((1 - a),(1 - b)));
H1: 1 - (t . ((1 - a),(1 - b))) in [.0,1.] by CoIn01;
set C = 1 - (t . ((1 - b),(1 - c)));
H2: 1 - (t . ((1 - b),(1 - c))) in [.0,1.] by CoIn01;
(conorm t) . (((conorm t) . (a,b)),c) = (conorm t) . ((1 - (t . ((1 - a),(1 - b)))),c) by CoDef
.= 1 - (t . ((1 - (1 - (t . ((1 - a),(1 - b))))),(1 - c))) by CoDef, H1
.= 1 - (t . ((1 - a),(1 - (1 - (t . ((1 - b),(1 - c))))))) by BINOP_1:def 3, A2
.= (conorm t) . (a,(1 - (t . ((1 - b),(1 - c))))) by CoDef, H2
.= (conorm t) . (a,((conorm t) . (b,c))) by CoDef ;
hence (conorm t) . (((conorm t) . (a,b)),c) = (conorm t) . (a,((conorm t) . (b,c))) ; :: thesis: verum

end;

D1: for a, b, c, d being Element of [.0,1.] st a <= c & b <= d holds
(conorm t) . (a,b) <= (conorm t) . (c,d)

proof

let a, b, c, d be Element of [.0,1.]; :: thesis: ( a <= c & b <= d implies (conorm t) . (a,b) <= (conorm t) . (c,d) )
A2: ( 1 - a in [.0,1.] & 1 - b in [.0,1.] & 1 - c in [.0,1.] & 1 - d in [.0,1.] ) by OpIn01;
assume ( a <= c & b <= d ) ; :: thesis: (conorm t) . (a,b) <= (conorm t) . (c,d)
then ( 1 - c <= 1 - a & 1 - d <= 1 - b ) by XREAL_1:10;
then t . ((1 - a),(1 - b)) >= t . ((1 - c),(1 - d)) by A2, MonDef;
then 1 - (t . ((1 - a),(1 - b))) <= 1 - (t . ((1 - c),(1 - d))) by XREAL_1:10;
then (conorm t) . (a,b) <= 1 - (t . ((1 - c),(1 - d))) by CoDef;
hence (conorm t) . (a,b) <= (conorm t) . (c,d) by CoDef; :: thesis: verum

end;

for a being Element of [.0,1.] holds (conorm t) . (a,0) = a

proof

let a be Element of [.0,1.]; :: thesis: (conorm t) . (a,0) = a
T1: 0 in [.0,1.] by XXREAL_1:1;
1 - a in [.0,1.] by OpIn01;
then t . ((1 - a),1) = 1 - a by IdDef;
then 1 - (t . ((1 - a),(1 - 0))) = a ;
hence (conorm t) . (a,0) = a by CoDef, T1; :: thesis: verum

end;

hence ( conorm t is monotonic & conorm t is commutative & conorm t is associative & conorm t is with-0-identity ) by A1, BINOP_1:def 2, BINOP_1:def 3, D1, C1; :: thesis: verum