let X be non empty set ; for S being SigmaField of X
for f being PartFunc of X,ExtREAL
for F being Finite_Sep_Sequence of S
for a being FinSequence of ExtREAL
for x being Element of X st F,a are_Re-presentation_of f & x in dom f holds
ex ax being FinSequence of ExtREAL st
( dom ax = dom a & ( for n being Nat st n in dom ax holds
ax . n = (a . n) * ((chi ((F . n),X)) . x) ) & f . x = Sum ax )
let S be SigmaField of X; for f being PartFunc of X,ExtREAL
for F being Finite_Sep_Sequence of S
for a being FinSequence of ExtREAL
for x being Element of X st F,a are_Re-presentation_of f & x in dom f holds
ex ax being FinSequence of ExtREAL st
( dom ax = dom a & ( for n being Nat st n in dom ax holds
ax . n = (a . n) * ((chi ((F . n),X)) . x) ) & f . x = Sum ax )
let f be PartFunc of X,ExtREAL; for F being Finite_Sep_Sequence of S
for a being FinSequence of ExtREAL
for x being Element of X st F,a are_Re-presentation_of f & x in dom f holds
ex ax being FinSequence of ExtREAL st
( dom ax = dom a & ( for n being Nat st n in dom ax holds
ax . n = (a . n) * ((chi ((F . n),X)) . x) ) & f . x = Sum ax )
let F be Finite_Sep_Sequence of S; for a being FinSequence of ExtREAL
for x being Element of X st F,a are_Re-presentation_of f & x in dom f holds
ex ax being FinSequence of ExtREAL st
( dom ax = dom a & ( for n being Nat st n in dom ax holds
ax . n = (a . n) * ((chi ((F . n),X)) . x) ) & f . x = Sum ax )
let a be FinSequence of ExtREAL ; for x being Element of X st F,a are_Re-presentation_of f & x in dom f holds
ex ax being FinSequence of ExtREAL st
( dom ax = dom a & ( for n being Nat st n in dom ax holds
ax . n = (a . n) * ((chi ((F . n),X)) . x) ) & f . x = Sum ax )
let x be Element of X; ( F,a are_Re-presentation_of f & x in dom f implies ex ax being FinSequence of ExtREAL st
( dom ax = dom a & ( for n being Nat st n in dom ax holds
ax . n = (a . n) * ((chi ((F . n),X)) . x) ) & f . x = Sum ax ) )
assume that
A1:
F,a are_Re-presentation_of f
and
A2:
x in dom f
; ex ax being FinSequence of ExtREAL st
( dom ax = dom a & ( for n being Nat st n in dom ax holds
ax . n = (a . n) * ((chi ((F . n),X)) . x) ) & f . x = Sum ax )
A3:
dom F = dom a
by A1;
deffunc H1( Nat) -> Element of ExtREAL = (a . $1) * ((chi ((F . $1),X)) . x);
consider ax being FinSequence of ExtREAL such that
A4:
( len ax = len a & ( for j being Nat st j in dom ax holds
ax . j = H1(j) ) )
from FINSEQ_2:sch 1();
A5:
dom ax = Seg (len a)
by A4, FINSEQ_1:def 3;
A6:
dom f = union (rng F)
by A1;
A7:
f . x = Sum ax
proof
consider Y being
set such that A8:
x in Y
and A9:
Y in rng F
by A2, A6, TARSKI:def 4;
consider k being
object such that A10:
k in dom F
and A11:
Y = F . k
by A9, FUNCT_1:def 3;
reconsider k =
k as
Element of
NAT by A10;
A12:
k in Seg (len a)
by A3, A10, FINSEQ_1:def 3;
then A13:
len ax >= k
by A4, FINSEQ_1:1;
A14:
for
i being
Nat st
i in Seg (len ax) &
i <> k holds
ax . i = 0.
consider SA being
sequence of
ExtREAL such that A18:
Sum ax = SA . (len ax)
and A19:
SA . 0 = 0.
and A20:
for
i being
Nat st
i < len ax holds
SA . (i + 1) = (SA . i) + (ax . (i + 1))
by EXTREAL1:def 2;
defpred S1[
Nat]
means ( $1
<= len ax implies ( ( $1
< k implies
SA . $1
= 0. ) & ( $1
>= k implies
SA . $1
= f . x ) ) );
A21:
for
i being
Nat st
i in Seg (len ax) &
i = k holds
ax . i = f . x
proof
let i be
Nat;
( i in Seg (len ax) & i = k implies ax . i = f . x )
assume that A22:
i in Seg (len ax)
and A23:
i = k
;
ax . i = f . x
(chi ((F . i),X)) . x = 1.
by A8, A11, A23, FUNCT_3:def 3;
then ax . i =
(a . i) * 1.
by A4, A5, A22
.=
a . i
by XXREAL_3:81
;
hence
ax . i = f . x
by A1, A8, A10, A11, A23;
verum
end;
A24:
for
i being
Nat st
S1[
i] holds
S1[
i + 1]
proof
let i be
Nat;
( S1[i] implies S1[i + 1] )
assume A25:
S1[
i]
;
S1[i + 1]
assume A26:
i + 1
<= len ax
;
( ( i + 1 < k implies SA . (i + 1) = 0. ) & ( i + 1 >= k implies SA . (i + 1) = f . x ) )
reconsider i =
i as
Element of
NAT by ORDINAL1:def 12;
now ( ( i + 1 < k & ( i + 1 < k implies SA . (i + 1) = 0. ) & ( i + 1 >= k implies SA . (i + 1) = f . x ) ) or ( i + 1 >= k & ( i + 1 < k implies SA . (i + 1) = 0. ) & ( i + 1 >= k implies SA . (i + 1) = f . x ) ) )per cases
( i + 1 < k or i + 1 >= k )
;
case A27:
i + 1
< k
;
( ( i + 1 < k implies SA . (i + 1) = 0. ) & ( i + 1 >= k implies SA . (i + 1) = f . x ) )A28:
k <= len a
by A12, FINSEQ_1:1;
A29:
i <= i + 1
by NAT_1:11;
then
i < k
by A27, XXREAL_0:2;
then A30:
i < len ax
by A4, A28, XXREAL_0:2;
then
( 1
<= i + 1 &
i + 1
<= len ax )
by NAT_1:11, NAT_1:13;
then A31:
i + 1
in Seg (len ax)
by FINSEQ_1:1;
SA . (i + 1) =
0. + (ax . (i + 1))
by A20, A25, A27, A29, A30, XXREAL_0:2
.=
ax . (i + 1)
by XXREAL_3:4
.=
0.
by A14, A27, A31
;
hence
( (
i + 1
< k implies
SA . (i + 1) = 0. ) & (
i + 1
>= k implies
SA . (i + 1) = f . x ) )
by A27;
verum end; case A32:
i + 1
>= k
;
( ( i + 1 < k implies SA . (i + 1) = 0. ) & ( i + 1 >= k implies SA . (i + 1) = f . x ) )now ( ( k = i + 1 & SA . (i + 1) = f . x ) or ( k <> i + 1 & SA . (i + 1) = f . x ) )per cases
( k = i + 1 or k <> i + 1 )
;
case A33:
k = i + 1
;
SA . (i + 1) = f . xA34:
k <= len a
by A12, FINSEQ_1:1;
then
i < len ax
by A4, A33, NAT_1:13;
hence SA . (i + 1) =
(SA . i) + (ax . (i + 1))
by A20
.=
ax . k
by A4, A25, A33, A34, NAT_1:13, XXREAL_3:4
.=
f . x
by A4, A12, A21
;
verum end; end; end; hence
( (
i + 1
< k implies
SA . (i + 1) = 0. ) & (
i + 1
>= k implies
SA . (i + 1) = f . x ) )
by A32;
verum end; end; end;
hence
( (
i + 1
< k implies
SA . (i + 1) = 0. ) & (
i + 1
>= k implies
SA . (i + 1) = f . x ) )
;
verum
end;
A37:
S1[
0 ]
by A12, A19, FINSEQ_1:1;
for
i being
Nat holds
S1[
i]
from NAT_1:sch 2(A37, A24);
hence
f . x = Sum ax
by A18, A13;
verum
end;
take
ax
; ( dom ax = dom a & ( for n being Nat st n in dom ax holds
ax . n = (a . n) * ((chi ((F . n),X)) . x) ) & f . x = Sum ax )
dom ax = Seg (len a)
by A4, FINSEQ_1:def 3;
hence
( dom ax = dom a & ( for n being Nat st n in dom ax holds
ax . n = (a . n) * ((chi ((F . n),X)) . x) ) & f . x = Sum ax )
by A4, A7, FINSEQ_1:def 3; verum