theorem :: FUZIMPL3:16

for I being Fuzzy_Implication
for f being bijective increasing UnOp of [.0,1.] holds ConjImpl (I,f) = ((f ") * I) * [:f,f:]