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,a,x) ) & Intf is_left_convergent_in b ) by A1;

take lim_left (Intf,b) ; :: 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,a,x) ) & Intf is_left_convergent_in b & lim_left (Intf,b) = lim_left (Intf,b) )

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,a,x) ) & Intf is_left_convergent_in b & lim_left (Intf,b) = lim_left (Intf,b) ) by A2; :: thesis: verum

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

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

take lim_left (Intf,b) ; :: 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,a,x) ) & Intf is_left_convergent_in b & lim_left (Intf,b) = lim_left (Intf,b) )

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,a,x) ) & Intf is_left_convergent_in b & lim_left (Intf,b) = lim_left (Intf,b) ) by A2; :: thesis: verum