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

proof

let x be Element of [.0,1.]; :: thesis: (FNegation I_RS) . x = NegationD1 . x

per cases ( x <= 0 or x > 0 ) ;

suppose B1: x <= 0 ; :: thesis: (FNegation I_RS) . x = NegationD1 . x

then B2: x = 0 by XXREAL_1:1;
(FNegation I_RS) . x = I_RS . (x,0) by FNeg
.= 1 by FUZIMPL1:def 20, B1, A1
.= NegationD1 . x by D1Def, B2 ;
hence (FNegation I_RS) . x = NegationD1 . x ; :: thesis: verum

end;

suppose B1: x > 0 ; :: thesis: (FNegation I_RS) . x = NegationD1 . x

(FNegation I_RS) . x = I_RS . (x,0) by FNeg
.= 0 by A1, B1, FUZIMPL1:def 20
.= NegationD1 . x by D1Def, B1 ;
hence (FNegation I_RS) . x = NegationD1 . x ; :: thesis: verum

end;

end;

end;

hence FNegation I_RS = NegationD1 by FUNCT_2:63; :: thesis: verum