let I be satisfying_(EP) satisfying_(OP) BinOp of [.0,1.]; :: thesis: ((FNegation I) * (FNegation I)) * (FNegation I) = FNegation I
set f = FNegation I;

now :: thesis: for x being Element of [.0,1.] holds (((FNegation I) * (FNegation I)) * (FNegation I)) . x = (FNegation I) . x

let x be Element of [.0,1.]; :: thesis: (((FNegation I) * (FNegation I)) * (FNegation I)) . x = (FNegation I) . x
FNegation I is non-increasing by N2Def;
then R2: (FNegation I) . ((FNegation I) . ((FNegation I) . x)) <= (FNegation I) . x by NonInc, Prop1417ii;
v1: (FNegation I) . x = I . (x,0) by FNeg;
v2: I . ((I . ((I . (x,0)),0)),0) = I . ((I . (((FNegation I) . x),0)),0) by FNeg
.= I . (((FNegation I) . ((FNegation I) . x)),0) by FNeg
.= (FNegation I) . ((FNegation I) . ((FNegation I) . x)) by FNeg ;
vz: (FNegation I) . ((FNegation I) . x) = I . ((I . (x,0)),0) by FNeg, v1;
r1: dom ((FNegation I) * (FNegation I)) = [.0,1.] by FUNCT_2:def 1;
0 in [.0,1.] by XXREAL_1:1;
then I . ((I . (x,0)),(I . ((I . ((I . (x,0)),0)),0))) = I . ((I . ((I . (x,0)),0)),(I . ((I . (x,0)),0))) by FUZIMPL2:def 2, vz, v1
.= 1 by vz, FUZIMPL2:def 3 ;
then (FNegation I) . x <= I . ((I . (((FNegation I) . x),0)),0) by v1, v2, FUZIMPL2:def 4;
then (FNegation I) . x <= I . (((FNegation I) . ((FNegation I) . x)),0) by FNeg;
then (FNegation I) . x <= (FNegation I) . ((FNegation I) . ((FNegation I) . x)) by FNeg;
then (FNegation I) . x = (FNegation I) . ((FNegation I) . ((FNegation I) . x)) by R2, XXREAL_0:1;
then (FNegation I) . x = (FNegation I) . (((FNegation I) * (FNegation I)) . x) by r1, FUNCT_1:12
.= ((FNegation I) * ((FNegation I) * (FNegation I))) . x by FUNCT_1:13, r1 ;
hence (((FNegation I) * (FNegation I)) * (FNegation I)) . x = (FNegation I) . x by RELAT_1:36; :: thesis: verum

end;

hence ((FNegation I) * (FNegation I)) * (FNegation I) = FNegation I by FUNCT_2:63; :: thesis: verum