let t be BinOp of [.0,1.]; :: thesis: conorm (conorm t) = t
set tt = conorm (conorm t);
for a, b being Element of [.0,1.] holds t . (a,b) = (conorm (conorm t)) . (a,b)

proof

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

end;

hence conorm (conorm t) = t by BINOP_1:2; :: thesis: verum