consider Intf being PartFunc of REAL,REAL such that

A2: ( dom Intf = ].a,b.] & ( for x being Real st x in dom Intf holds

Intf . x = integral (f,x,b) ) & Intf is_right_convergent_in a ) by A1;

take lim_right (Intf,a) ; :: thesis: ex Intf being PartFunc of REAL,REAL st

( dom Intf = ].a,b.] & ( for x being Real st x in dom Intf holds

Intf . x = integral (f,x,b) ) & Intf is_right_convergent_in a & lim_right (Intf,a) = lim_right (Intf,a) )

thus ex Intf being PartFunc of REAL,REAL st

( dom Intf = ].a,b.] & ( for x being Real st x in dom Intf holds

Intf . x = integral (f,x,b) ) & Intf is_right_convergent_in a & lim_right (Intf,a) = lim_right (Intf,a) ) by A2; :: thesis: verum

A2: ( dom Intf = ].a,b.] & ( for x being Real st x in dom Intf holds

Intf . x = integral (f,x,b) ) & Intf is_right_convergent_in a ) by A1;

take lim_right (Intf,a) ; :: thesis: ex Intf being PartFunc of REAL,REAL st

( dom Intf = ].a,b.] & ( for x being Real st x in dom Intf holds

Intf . x = integral (f,x,b) ) & Intf is_right_convergent_in a & lim_right (Intf,a) = lim_right (Intf,a) )

thus ex Intf being PartFunc of REAL,REAL st

( dom Intf = ].a,b.] & ( for x being Real st x in dom Intf holds

Intf . x = integral (f,x,b) ) & Intf is_right_convergent_in a & lim_right (Intf,a) = lim_right (Intf,a) ) by A2; :: thesis: verum