let I be Fuzzy_Implication; :: thesis: for f being bijective increasing UnOp of [.0,1.] holds ConjImpl (I,f) = ((f ") * I) * [:f,f:]
let f be bijective increasing UnOp of [.0,1.]; :: thesis: ConjImpl (I,f) = ((f ") * I) * [:f,f:]
set g = ConjImpl (I,f);
dom (ConjImpl (I,f)) = [:[.0,1.],[.0,1.]:] by FUNCT_2:def 1;
then A1: dom (ConjImpl (I,f)) = dom (((f ") * I) * [:f,f:]) by FUNCT_2:def 1;
C2: dom f = [.0,1.] by FUNCT_2:def 1;
for x being object st x in dom (ConjImpl (I,f)) holds
(ConjImpl (I,f)) . x = (((f ") * I) * [:f,f:]) . x

proof

let x be object ; :: thesis: ( x in dom (ConjImpl (I,f)) implies (ConjImpl (I,f)) . x = (((f ") * I) * [:f,f:]) . x )
assume x in dom (ConjImpl (I,f)) ; :: thesis: (ConjImpl (I,f)) . x = (((f ") * I) * [:f,f:]) . x
then W1: x in [:[.0,1.],[.0,1.]:] by FUNCT_2:def 1;
then consider x1, x2 being object such that
C0: ( x1 in [.0,1.] & x2 in [.0,1.] & x = [x1,x2] ) by ZFMISC_1:def 2;
reconsider x1 = x1, x2 = x2 as Element of [.0,1.] by C0;
D1: x in dom [:f,f:] by W1, FUNCT_2:def 1;
X2: dom I = [:[.0,1.],[.0,1.]:] by FUNCT_2:def 1;
[(f . x1),(f . x2)] in [:[.0,1.],[.0,1.]:] by ZFMISC_1:87;
then [:f,f:] . (x1,x2) in dom I by X2;
then D2: [:f,f:] . x in dom I by C0, BINOP_1:def 1;
(ConjImpl (I,f)) . x = (ConjImpl (I,f)) . (x1,x2) by C0, BINOP_1:def 1
.= (f ") . (I . ((f . x1),(f . x2))) by BIDef
.= (f ") . (I . [(f . x1),(f . x2)]) by BINOP_1:def 1
.= (f ") . (I . ([:f,f:] . (x1,x2))) by C2, FUNCT_3:def 8
.= (f ") . (I . ([:f,f:] . x)) by C0, BINOP_1:def 1
.= ((f ") * I) . ([:f,f:] . x) by FUNCT_1:13, D2
.= (((f ") * I) * [:f,f:]) . x by FUNCT_1:13, D1 ;
hence (ConjImpl (I,f)) . x = (((f ") * I) * [:f,f:]) . x ; :: thesis: verum

end;

hence ConjImpl (I,f) = ((f ") * I) * [:f,f:] by A1, FUNCT_1:2; :: thesis: verum