let n be Element of NAT ; for A being non empty closed_interval Subset of REAL
for f being Function of A,(REAL n)
for g being Function of A,(REAL-NS n)
for I being Element of REAL n
for J being Point of (REAL-NS n) st f = g & I = J holds
( ( for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) ) iff for T being DivSequence of A
for S being middle_volume_Sequence of g,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = J ) )
let A be non empty closed_interval Subset of REAL; for f being Function of A,(REAL n)
for g being Function of A,(REAL-NS n)
for I being Element of REAL n
for J being Point of (REAL-NS n) st f = g & I = J holds
( ( for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) ) iff for T being DivSequence of A
for S being middle_volume_Sequence of g,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = J ) )
let f be Function of A,(REAL n); for g being Function of A,(REAL-NS n)
for I being Element of REAL n
for J being Point of (REAL-NS n) st f = g & I = J holds
( ( for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) ) iff for T being DivSequence of A
for S being middle_volume_Sequence of g,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = J ) )
let g be Function of A,(REAL-NS n); for I being Element of REAL n
for J being Point of (REAL-NS n) st f = g & I = J holds
( ( for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) ) iff for T being DivSequence of A
for S being middle_volume_Sequence of g,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = J ) )
let I be Element of REAL n; for J being Point of (REAL-NS n) st f = g & I = J holds
( ( for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) ) iff for T being DivSequence of A
for S being middle_volume_Sequence of g,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = J ) )
let J be Point of (REAL-NS n); ( f = g & I = J implies ( ( for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) ) iff for T being DivSequence of A
for S being middle_volume_Sequence of g,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = J ) ) )
assume A1:
( f = g & I = J )
; ( ( for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) ) iff for T being DivSequence of A
for S being middle_volume_Sequence of g,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = J ) )
hereby ( ( for T being DivSequence of A
for S being middle_volume_Sequence of g,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = J ) ) implies for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) )
assume A2:
for
T being
DivSequence of
A for
S being
middle_volume_Sequence of
f,
T st
delta T is
convergent &
lim (delta T) = 0 holds
(
middle_sum (
f,
S) is
convergent &
lim (middle_sum (f,S)) = I )
;
for T being DivSequence of A
for S0 being middle_volume_Sequence of g,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (g,S0) is convergent & lim (middle_sum (g,S0)) = J )A3:
the
carrier of
(REAL-NS n) = REAL n
by REAL_NS1:def 4;
thus
for
T being
DivSequence of
A for
S0 being
middle_volume_Sequence of
g,
T st
delta T is
convergent &
lim (delta T) = 0 holds
(
middle_sum (
g,
S0) is
convergent &
lim (middle_sum (g,S0)) = J )
verumproof
let T be
DivSequence of
A;
for S0 being middle_volume_Sequence of g,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (g,S0) is convergent & lim (middle_sum (g,S0)) = J )let S0 be
middle_volume_Sequence of
g,
T;
( delta T is convergent & lim (delta T) = 0 implies ( middle_sum (g,S0) is convergent & lim (middle_sum (g,S0)) = J ) )
assume A4:
(
delta T is
convergent &
lim (delta T) = 0 )
;
( middle_sum (g,S0) is convergent & lim (middle_sum (g,S0)) = J )
reconsider S =
S0 as
middle_volume_Sequence of
f,
T by A3, A1, Th38;
(
middle_sum (
f,
S) is
convergent &
lim (middle_sum (f,S)) = I )
by A2, A4;
hence
(
middle_sum (
g,
S0) is
convergent &
lim (middle_sum (g,S0)) = J )
by A1, Th39;
verum
end;
end;
assume A5:
for T being DivSequence of A
for S being middle_volume_Sequence of g,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = J )
; for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I )
A6:
the carrier of (REAL-NS n) = REAL n
by REAL_NS1:def 4;
thus
for T being DivSequence of A
for S0 being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S0) is convergent & lim (middle_sum (f,S0)) = I )
verumproof
let T be
DivSequence of
A;
for S0 being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S0) is convergent & lim (middle_sum (f,S0)) = I )let S0 be
middle_volume_Sequence of
f,
T;
( delta T is convergent & lim (delta T) = 0 implies ( middle_sum (f,S0) is convergent & lim (middle_sum (f,S0)) = I ) )
assume A7:
(
delta T is
convergent &
lim (delta T) = 0 )
;
( middle_sum (f,S0) is convergent & lim (middle_sum (f,S0)) = I )
reconsider S =
S0 as
middle_volume_Sequence of
g,
T by A6, A1, Th38;
(
middle_sum (
g,
S) is
convergent &
lim (middle_sum (g,S)) = I )
by A1, A5, A7;
hence
(
middle_sum (
f,
S0) is
convergent &
lim (middle_sum (f,S0)) = I )
by A1, Th39;
verum
end;