set dn = conorm Hamacher_norm;
set dc = Hamacher_conorm ;
for a, b being Element of [.0,1.] holds Hamacher_conorm . (a,b) = 1 - (Hamacher_norm . ((1 - a),(1 - b)))

proof

let a, b be Element of [.0,1.]; :: thesis: Hamacher_conorm . (a,b) = 1 - (Hamacher_norm . ((1 - a),(1 - b)))
AB: 0 in [.0,1.] by XXREAL_1:1;
A3: ( 1 - a in [.0,1.] & 1 - b in [.0,1.] ) by OpIn01;
WE: ( 0 <= a & a <= 1 & 0 <= b & b <= 1 ) by XXREAL_1:1;

per cases ( a <> 1 or b <> 1 or ( a = b & b = 1 ) ) ;

suppose Aa: ( a <> 1 or b <> 1 ) ; :: thesis: Hamacher_conorm . (a,b) = 1 - (Hamacher_norm . ((1 - a),(1 - b)))

then AA: 1 - (a * b) <> 0 by WE, XREAL_1:150;
Hamacher_conorm . (a,b) = ((a + b) - ((2 * a) * b)) / (1 - (a * b)) by HamCoDef, Aa
.= ((1 * (((1 - a) + (1 - b)) - ((1 - a) * (1 - b)))) - ((1 - a) * (1 - b))) / (((1 - a) + (1 - b)) - ((1 - a) * (1 - b)))
.= 1 - (((1 - a) * (1 - b)) / (((1 - a) + (1 - b)) - ((1 - a) * (1 - b)))) by XCMPLX_1:127, AA
.= 1 - (Hamacher_norm . ((1 - a),(1 - b))) by HamDef, A3 ;
hence Hamacher_conorm . (a,b) = 1 - (Hamacher_norm . ((1 - a),(1 - b))) ; :: thesis: verum

end;

suppose T1: ( a = b & b = 1 ) ; :: thesis: Hamacher_conorm . (a,b) = 1 - (Hamacher_norm . ((1 - a),(1 - b)))

then Hamacher_norm . ((1 - a),(1 - b)) = (0 * 0) / ((0 + 0) - (0 * 0)) by HamDef, AB
.= 0 ;
hence Hamacher_conorm . (a,b) = 1 - (Hamacher_norm . ((1 - a),(1 - b))) by T1, HamCoDef; :: thesis: verum

end;

end;

end;

hence conorm Hamacher_norm = Hamacher_conorm by CoDef; :: thesis: verum