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

proof

let a, b be Element of [.0,1.]; :: thesis: probsum_conorm . (a,b) = 1 - (prodnorm . ((1 - a),(1 - b)))
A3: ( 1 - a in [.0,1.] & 1 - b in [.0,1.] ) by OpIn01;
probsum_conorm . (a,b) = (a + b) - (a * b) by ProbSumDef
.= 1 - ((1 - a) * (1 - b))
.= 1 - (prodnorm . ((1 - a),(1 - b))) by ProdDef, A3 ;
hence probsum_conorm . (a,b) = 1 - (prodnorm . ((1 - a),(1 - b))) ; :: thesis: verum

end;

hence conorm prodnorm = probsum_conorm by CoDef; :: thesis: verum