let f be PartFunc of REAL,REAL; :: thesis: for a, b being Real st a < b & [.a,b.[ c= dom f & f is_right_improper_integrable_on a,b & abs f is_right_ext_Riemann_integrable_on a,b holds
max+ f is_right_ext_Riemann_integrable_on a,b
let a, b be Real; :: thesis: ( a < b & [.a,b.[ c= dom f & f is_right_improper_integrable_on a,b & abs f is_right_ext_Riemann_integrable_on a,b implies max+ f is_right_ext_Riemann_integrable_on a,b )
assume that
A1: a < b and
A2: [.a,b.[ c= dom f and
A3: f is_right_improper_integrable_on a,b and
A4: abs f is_right_ext_Riemann_integrable_on a,b ; :: thesis: max+ f is_right_ext_Riemann_integrable_on a,b
f is_right_ext_Riemann_integrable_on a,b by A1, A2, A3, A4, Th57;
hence max+ f is_right_ext_Riemann_integrable_on a,b by A1, A2, A4, Th64; :: thesis: verum