let F1, F2 be PartFunc of REAL,REAL; :: thesis: ( dom F1 = I & ( for x being Real st x in I holds
( ( x = inf I implies F1 . x = Rdiff (f,x) ) & ( x = sup I implies F1 . x = Ldiff (f,x) ) & ( x <> inf I & x <> sup I implies F1 . x = diff (f,x) ) ) ) & dom F2 = I & ( for x being Real st x in I holds
( ( x = inf I implies F2 . x = Rdiff (f,x) ) & ( x = sup I implies F2 . x = Ldiff (f,x) ) & ( x <> inf I & x <> sup I implies F2 . x = diff (f,x) ) ) ) implies F1 = F2 )
assume that
A16: ( dom F1 = I & ( for x being Real st x in I holds
( ( x = inf I implies F1 . x = Rdiff (f,x) ) & ( x = sup I implies F1 . x = Ldiff (f,x) ) & ( x <> inf I & x <> sup I implies F1 . x = diff (f,x) ) ) ) ) and
A17: ( dom F2 = I & ( for x being Real st x in I holds
( ( x = inf I implies F2 . x = Rdiff (f,x) ) & ( x = sup I implies F2 . x = Ldiff (f,x) ) & ( x <> inf I & x <> sup I implies F2 . x = diff (f,x) ) ) ) ) ; :: thesis: F1 = F2
for x being Element of REAL st x in dom F1 holds
F1 . x = F2 . x

proof

let x be Element of REAL ; :: thesis: ( x in dom F1 implies F1 . x = F2 . x )
assume A18: x in dom F1 ; :: thesis: F1 . x = F2 . x

per cases ( x = inf I or x = sup I or ( x <> inf I & x <> sup I ) ) ;

suppose x = inf I ; :: thesis: F1 . x = F2 . x

then ( F1 . x = Rdiff (f,x) & F2 . x = Rdiff (f,x) ) by A16, A17, A18;
hence F1 . x = F2 . x ; :: thesis: verum

end;

suppose x = sup I ; :: thesis: F1 . x = F2 . x

then ( F1 . x = Ldiff (f,x) & F2 . x = Ldiff (f,x) ) by A16, A17, A18;
hence F1 . x = F2 . x ; :: thesis: verum

end;

suppose ( x <> inf I & x <> sup I ) ; :: thesis: F1 . x = F2 . x

then ( F1 . x = diff (f,x) & F2 . x = diff (f,x) ) by A16, A17, A18;
hence F1 . x = F2 . x ; :: thesis: verum

end;

end;

end;

hence F1 = F2 by A16, A17, PARTFUN1:5; :: thesis: verum