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 A0:
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 A10:
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 )
assume K0:
i in Seg n
;
:: thesis: (proj i,n) * g is integrable
then K1:
(proj i,n) * f is_integrable_on A
by A10, Defintable;
dom (proj i,n) = REAL n
by FUNCT_2:def 1;
then
rng f c= dom (proj i,n)
;
then K2:
dom ((proj i,n) * f) = dom f
by RELAT_1:46;
A =
dom g
by FUNCT_2:def 1
.=
(dom f) /\ A
by A0, RELAT_1:90
;
then
((proj i,n) * f) || A is
total
by K2, XBOOLE_1:17, INTEGRA5:6;
then reconsider F =
((proj i,n) * f) | A as
Function of
A,
REAL ;
F is
integrable
by K1, INTEGRA5:def 2;
hence
(proj i,n) * g is
integrable
by A0, K0, LMDEF;
:: thesis: verum
end;
hence
g is
integrable
by Intablen;
:: thesis: verum
end;
assume K0:
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
hence
f is_integrable_on A
by Defintable; :: thesis: verum