let f be PartFunc of REAL,REAL; for a, b being Real st 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_divergent_to+infty_in a or Intf is_right_divergent_to-infty_in a ) ) holds
not f is_left_ext_Riemann_integrable_on a,b
let a, b be Real; ( 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_divergent_to+infty_in a or Intf is_right_divergent_to-infty_in a ) ) implies not f is_left_ext_Riemann_integrable_on a,b )
assume
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_divergent_to+infty_in a or Intf is_right_divergent_to-infty_in a ) )
; not f is_left_ext_Riemann_integrable_on a,b
then consider Intf being PartFunc of REAL,REAL such that
A1:
dom Intf = ].a,b.]
and
A2:
for x being Real st x in dom Intf holds
Intf . x = integral (f,x,b)
and
A3:
( Intf is_right_divergent_to+infty_in a or Intf is_right_divergent_to-infty_in a )
;
hereby verum
assume
f is_left_ext_Riemann_integrable_on a,
b
;
contradictionthen consider I being
PartFunc of
REAL,
REAL such that A4:
dom I = ].a,b.]
and A5:
for
x being
Real st
x in dom I holds
I . x = integral (
f,
x,
b)
and A6:
I is_right_convergent_in a
by INTEGR10:def 2;
then
I = Intf
by A1, A4, PARTFUN1:5;
hence
contradiction
by A3, A6, Th8, Th9;
verum
end;