set I = I_WB ;
set f = FNegation I_WB;
set g = NegationD2 ;
A1: 0 in [.0,1.] by XXREAL_1:1;
for x being Element of [.0,1.] holds (FNegation I_WB) . x = NegationD2 . x

proof

let x be Element of [.0,1.]; :: thesis: (FNegation I_WB) . x = NegationD2 . x
x <= 1 by XXREAL_1:1;

per cases then ( x < 1 or x = 1 ) by XXREAL_0:1;

suppose B1: x < 1 ; :: thesis: (FNegation I_WB) . x = NegationD2 . x

(FNegation I_WB) . x = I_WB . (x,0) by FNeg
.= 1 by FUZIMPL1:def 22, B1, A1
.= NegationD2 . x by D2Def, B1 ;
hence (FNegation I_WB) . x = NegationD2 . x ; :: thesis: verum

end;

suppose B1: x = 1 ; :: thesis: (FNegation I_WB) . x = NegationD2 . x

(FNegation I_WB) . x = I_WB . (x,0) by FNeg
.= 0 by A1, B1, FUZIMPL1:def 22
.= NegationD2 . x by D2Def, B1 ;
hence (FNegation I_WB) . x = NegationD2 . x ; :: thesis: verum

end;

end;

end;

hence FNegation I_WB = NegationD2 by FUNCT_2:63; :: thesis: verum