defpred S₁[ object ] means ( $1 = inf I & $1 in I );
defpred S₂[ object ] means ( $1 = sup I & $1 in I );
defpred S₃[ object ] means $1 in ].(inf I),(sup I).[;
deffunc H₁( object ) -> Element of REAL = In ((Rdiff (f,(In ($1,REAL)))),REAL);
deffunc H₂( object ) -> Element of REAL = In ((Ldiff (f,(In ($1,REAL)))),REAL);
deffunc H₃( object ) -> Element of REAL = In ((diff (f,(In ($1,REAL)))),REAL);
A2: for r being Element of REAL holds
( ( S₁[r] implies not S₂[r] ) & ( S₁[r] implies not S₃[r] ) & ( S₂[r] implies not S₃[r] ) ) by A1, XXREAL_1:4;
consider IT being PartFunc of REAL,REAL such that
A3: ( ( for r being Element of REAL holds
( r in dom IT iff ( S₁[r] or S₂[r] or S₃[r] ) ) ) & ( for r being Element of REAL st r in dom IT holds
( ( S₁[r] implies IT . r = H₁(r) ) & ( S₂[r] implies IT . r = H₂(r) ) & ( S₃[r] implies IT . r = H₃(r) ) ) ) ) from SCHEME1:sch 9(A2);
take IT ; :: thesis: ( dom IT = I & ( for x being Real st x in I holds
( ( x = inf I implies IT . x = Rdiff (f,x) ) & ( x = sup I implies IT . x = Ldiff (f,x) ) & ( x <> inf I & x <> sup I implies IT . x = diff (f,x) ) ) ) )

now :: thesis: for r being set st r in dom IT holds
r in I

let r be set ; :: thesis: ( r in dom IT implies b₁ in I )
assume r in dom IT ; :: thesis: b₁ in I

per cases then ( S₁[r] or S₂[r] or S₃[r] ) by A3;

suppose ( S₁[r] or S₂[r] ) ; :: thesis: b₁ in I

hence r in I ; :: thesis: verum

end;

suppose A5: S₃[r] ; :: thesis: b₁ in I

then reconsider r1 = r as Real ;
( inf I < r1 & r1 < sup I ) by A5, XXREAL_1:4;
hence r in I by XXREAL_2:83; :: thesis: verum

end;

end;

end;

then A6: dom IT c= I ;

now :: thesis: for r being set st r in I holds
r in dom IT

let r be set ; :: thesis: ( r in I implies b₁ in dom IT )
assume A7: r in I ; :: thesis: b₁ in dom IT
then reconsider r1 = r as Real ;

per cases ( I is closed_interval or I is right_open_interval or I is left_open_interval or I is open_interval ) by MEASURE5:1;

suppose I is closed_interval ; :: thesis: b₁ in dom IT

then ( S₁[r] or S₂[r] or S₃[r] ) by A7, Lm1;
hence r in dom IT by A3; :: thesis: verum

end;

suppose I is right_open_interval ; :: thesis: b₁ in dom IT

then ( S₁[r] or S₃[r] ) by A7, Lm2;
hence r in dom IT by A3; :: thesis: verum

end;

suppose I is left_open_interval ; :: thesis: b₁ in dom IT

then ( S₂[r] or S₃[r] ) by A7, Lm3;
hence r in dom IT by A3; :: thesis: verum

end;

suppose I is open_interval ; :: thesis: b₁ in dom IT

hence r in dom IT by A3, A7, Lm4; :: thesis: verum

end;

end;

end;

then A8: I c= dom IT ;
hence dom IT = I by A6, XBOOLE_0:def 10; :: thesis: for x being Real st x in I holds
( ( x = inf I implies IT . x = Rdiff (f,x) ) & ( x = sup I implies IT . x = Ldiff (f,x) ) & ( x <> inf I & x <> sup I implies IT . x = diff (f,x) ) )
thus for x being Real st x in I holds
( ( x = inf I implies IT . x = Rdiff (f,x) ) & ( x = sup I implies IT . x = Ldiff (f,x) ) & ( x <> inf I & x <> sup I implies IT . x = diff (f,x) ) ) :: thesis: verum

proof

let x be Real; :: thesis: ( x in I implies ( ( x = inf I implies IT . x = Rdiff (f,x) ) & ( x = sup I implies IT . x = Ldiff (f,x) ) & ( x <> inf I & x <> sup I implies IT . x = diff (f,x) ) ) )
assume A9: x in I ; :: thesis: ( ( x = inf I implies IT . x = Rdiff (f,x) ) & ( x = sup I implies IT . x = Ldiff (f,x) ) & ( x <> inf I & x <> sup I implies IT . x = diff (f,x) ) )

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

suppose A10: x = inf I ; :: thesis: ( ( x = inf I implies IT . x = Rdiff (f,x) ) & ( x = sup I implies IT . x = Ldiff (f,x) ) & ( x <> inf I & x <> sup I implies IT . x = diff (f,x) ) )

then IT . x = H₁(x) by A3, A8, A9;
hence ( ( x = inf I implies IT . x = Rdiff (f,x) ) & ( x = sup I implies IT . x = Ldiff (f,x) ) & ( x <> inf I & x <> sup I implies IT . x = diff (f,x) ) ) by A10, A1; :: thesis: verum

end;

suppose A11: x = sup I ; :: thesis: ( ( x = inf I implies IT . x = Rdiff (f,x) ) & ( x = sup I implies IT . x = Ldiff (f,x) ) & ( x <> inf I & x <> sup I implies IT . x = diff (f,x) ) )

then IT . x = H₂(x) by A3, A8, A9;
hence ( ( x = inf I implies IT . x = Rdiff (f,x) ) & ( x = sup I implies IT . x = Ldiff (f,x) ) & ( x <> inf I & x <> sup I implies IT . x = diff (f,x) ) ) by A11, A1; :: thesis: verum

end;

suppose A12: ( x <> inf I & x <> sup I ) ; :: thesis: ( ( x = inf I implies IT . x = Rdiff (f,x) ) & ( x = sup I implies IT . x = Ldiff (f,x) ) & ( x <> inf I & x <> sup I implies IT . x = diff (f,x) ) )

A13: x in ].(inf I),(sup I).[

proof

A14: ( I is closed_interval implies x in ].(inf I),(sup I).[ ) by A9, A12, Lm1;
A15: ( I is right_open_interval implies x in ].(inf I),(sup I).[ ) by A9, A12, Lm2;
( I is left_open_interval implies x in ].(inf I),(sup I).[ ) by A9, A12, Lm3;
hence x in ].(inf I),(sup I).[ by A14, A15, A9, Lm4, MEASURE5:1; :: thesis: verum

end;

then ( inf I < x & x < sup I ) by XXREAL_1:4;
then x in I by XXREAL_2:83;
then IT . x = H₃(x) by A3, A8, A13;
hence ( ( x = inf I implies IT . x = Rdiff (f,x) ) & ( x = sup I implies IT . x = Ldiff (f,x) ) & ( x <> inf I & x <> sup I implies IT . x = diff (f,x) ) ) by A12; :: thesis: verum

end;

end;

end;