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

proof

let a, b be Element of [.0,1.]; :: thesis: BoundedSum_conorm . (a,b) = 1 - (Lukasiewicz_norm . ((1 - a),(1 - b)))
A3: ( 1 - a in [.0,1.] & 1 - b in [.0,1.] ) by OpIn01;
BoundedSum_conorm . (a,b) = min ((a + b),1) by LukConorm
.= 1 - (max (0,(((1 - a) + (1 - b)) - 1))) by LukasiDual
.= 1 - (Lukasiewicz_norm . ((1 - a),(1 - b))) by LukNorm, A3 ;
hence BoundedSum_conorm . (a,b) = 1 - (Lukasiewicz_norm . ((1 - a),(1 - b))) ; :: thesis: verum

end;

hence conorm Lukasiewicz_norm = BoundedSum_conorm by CoDef; :: thesis: verum