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

proof

let x be Element of [.0,1.]; :: thesis: (FNegation I_I4) . 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_I4) . x = NegationD2 . x

(FNegation I_I4) . x = I_I4 . (x,0) by FUZIMPL3:def 16
.= 1 by II4Def, B1, A1
.= NegationD2 . x by FUZIMPL3:def 18, B1 ;
hence (FNegation I_I4) . x = NegationD2 . x ; :: thesis: verum

end;

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

(FNegation I_I4) . x = I_I4 . (x,0) by FUZIMPL3:def 16
.= 0 by A1, B1, II4Def
.= NegationD2 . x by FUZIMPL3:def 18, B1 ;
hence (FNegation I_I4) . x = NegationD2 . x ; :: thesis: verum

end;

end;

end;

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