let I be Fuzzy_Implication; :: thesis: for h being bijective increasing UnOp of [.0,1.] holds ConjNeg ((FNegation I),h) = FNegation (ConjImpl (I,h))
let h be bijective increasing UnOp of [.0,1.]; :: thesis: ConjNeg ((FNegation I),h) = FNegation (ConjImpl (I,h))
set f = ConjNeg ((FNegation I),h);
set g = FNegation (ConjImpl (I,h));
AA: 0 in [.0,1.] by XXREAL_1:1;
for x being Element of [.0,1.] holds (ConjNeg ((FNegation I),h)) . x = (FNegation (ConjImpl (I,h))) . x

proof

let x be Element of [.0,1.]; :: thesis: (ConjNeg ((FNegation I),h)) . x = (FNegation (ConjImpl (I,h))) . x
(ConjNeg ((FNegation I),h)) . x = (h ") . ((FNegation I) . (h . x)) by CNDef
.= (h ") . (I . ((h . x),0)) by FNeg
.= (h ") . (I . ((h . x),(h . 0))) by LemmaBound
.= (ConjImpl (I,h)) . (x,0) by AA, BIDef
.= (FNegation (ConjImpl (I,h))) . x by FNeg ;
hence (ConjNeg ((FNegation I),h)) . x = (FNegation (ConjImpl (I,h))) . x ; :: thesis: verum

end;

hence ConjNeg ((FNegation I),h) = FNegation (ConjImpl (I,h)) by FUNCT_2:63; :: thesis: verum