set f = conorm t;
A1: for a, b being Element of [.0,1.] holds () . (a,b) = () . (b,a)
proof
let a, b be Element of [.0,1.]; :: thesis: () . (a,b) = () . (b,a)
A2: ( 1 - a in [.0,1.] & 1 - b in [.0,1.] ) by OpIn01;
() . (a,b) = 1 - (t . ((1 - a),(1 - b))) by CoDef
.= 1 - (t . ((1 - b),(1 - a))) by
.= () . (b,a) by CoDef ;
hence (conorm t) . (a,b) = () . (b,a) ; :: thesis: verum
end;
C1: for a, b, c being Element of [.0,1.] holds () . ((() . (a,b)),c) = () . (a,(() . (b,c)))
proof
let a, b, c be Element of [.0,1.]; :: thesis: () . ((() . (a,b)),c) = () . (a,(() . (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;
() . ((() . (a,b)),c) = () . ((1 - (t . ((1 - a),(1 - b)))),c) by CoDef
.= 1 - (t . ((1 - (1 - (t . ((1 - a),(1 - b))))),(1 - c))) by
.= 1 - (t . ((1 - a),(1 - (1 - (t . ((1 - b),(1 - c))))))) by
.= () . (a,(1 - (t . ((1 - b),(1 - c))))) by
.= () . (a,(() . (b,c))) by CoDef ;
hence (conorm t) . ((() . (a,b)),c) = () . (a,(() . (b,c))) ; :: thesis: verum
end;
D1: for a, b, c, d being Element of [.0,1.] st a <= c & b <= d holds
() . (a,b) <= () . (c,d)
proof
let a, b, c, d be Element of [.0,1.]; :: thesis: ( a <= c & b <= d implies () . (a,b) <= () . (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: () . (a,b) <= () . (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 ;
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) <= () . (c,d) by CoDef; :: thesis: verum
end;
for a being Element of [.0,1.] holds () . (a,0) = a
proof
let a be Element of [.0,1.]; :: thesis: () . (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 ; :: thesis: verum
end;
hence ( conorm t is monotonic & conorm t is commutative & conorm t is associative & conorm t is with-0-identity ) by ; :: thesis: verum