let n be Element of NAT ; :: thesis: for A being closed-interval Subset of REAL
for f being PartFunc of REAL ,(REAL n)
for g being Function of A,(REAL n) 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 ,(REAL n)
for g being Function of A,(REAL n) st f | A = g holds
( f is_integrable_on A iff g is integrable )
let f be PartFunc of REAL ,(REAL n); :: thesis: for g being Function of A,(REAL n) st f | A = g holds
( f is_integrable_on A iff g is integrable )
let g be Function of A,(REAL n); :: 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 )
thus ( f is_integrable_on A implies g is integrable ) :: thesis: ( g is integrable implies f is_integrable_on A )

proof

assume A2: f is_integrable_on A ; :: thesis: g is integrable
for i being Element of NAT st i in Seg n holds
(proj i,n) * g is integrable

proof

let i be Element of NAT ; :: thesis: ( i in Seg n implies (proj i,n) * g is integrable )
dom (proj i,n) = REAL n by FUNCT_2:def 1;
then rng f c= dom (proj i,n) ;
then A3: dom ((proj i,n) * f) = dom f by RELAT_1:46;
A = dom g by FUNCT_2:def 1
.= (dom f) /\ A by A1, RELAT_1:90 ;
then ((proj i,n) * f) || A is total by A3, INTEGRA5:6, XBOOLE_1:17;
then reconsider F = ((proj i,n) * f) | A as Function of A,REAL ;
assume i in Seg n ; :: thesis: (proj i,n) * g is integrable
then (proj i,n) * f is_integrable_on A by A2, Def16;
then F is integrable by INTEGRA5:def 2;
hence (proj i,n) * g is integrable by A1, Lm6; :: thesis: verum

end;

hence g is integrable by Def13; :: thesis: verum

end;

assume A4: g is integrable ; :: thesis: f is_integrable_on A
for i being Element of NAT st i in Seg n holds
(proj i,n) * f is_integrable_on A

proof

let i be Element of NAT ; :: thesis: ( i in Seg n implies (proj i,n) * f is_integrable_on A )
assume A5: i in Seg n ; :: thesis: (proj i,n) * f is_integrable_on A
(proj i,n) * g = ((proj i,n) * f) | A by A1, Lm6;
then ((proj i,n) * f) || A is integrable by A4, A5, Def13;
hence (proj i,n) * f is_integrable_on A by INTEGRA5:def 2; :: thesis: verum

end;

hence f is_integrable_on A by Def16; :: thesis: verum