let I be Fuzzy_Implication; 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.]; 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.];
(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
;
verum
end;
hence
ConjNeg ((FNegation I),h) = FNegation (ConjImpl (I,h))
by FUNCT_2:63; verum