let X be RealNormSpace; :: thesis: for A being 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 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 AS: 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 Def16;
hence g is integrable by AS; :: thesis: verum

end;

assume g is integrable ; :: thesis: f is_integrable_on A
hence f is_integrable_on A by AS, Def16; :: thesis: verum