let X be RealNormSpace; :: thesis: for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL, the carrier of X
for g being Function of A, the carrier of X st f | A = g holds
( f is_integrable_on A iff g is integrable )
let A be non empty closed_interval Subset of REAL; :: thesis: for f being PartFunc of REAL, the carrier of X
for g being Function of A, the carrier of X st f | A = g holds
( f is_integrable_on A iff g is integrable )
let f be PartFunc of REAL, the carrier of X; :: thesis: for g being Function of A, the carrier of X st f | A = g holds
( f is_integrable_on A iff g is integrable )
let g be Function of A, the carrier of X; :: thesis: ( f | A = g implies ( f is_integrable_on A iff g is integrable ) )
assume A1: f | A = g ; :: thesis: ( f is_integrable_on A iff g is integrable )

hereby :: thesis: ( g is integrable implies f is_integrable_on A )

assume f is_integrable_on A ; :: thesis: g is integrable
then ex g being Function of A, the carrier of X st
( g = f | A & g is integrable ) by Def7;
hence g is integrable by A1; :: thesis: verum

end;

assume g is integrable ; :: thesis: f is_integrable_on A
hence f is_integrable_on A by A1, Def7; :: thesis: verum