let X be non empty set ; :: thesis: for S being non empty Subset-Family of X
for f being Function of NAT,S
for F being Functional_Sequence of X,ExtREAL st f is disjoint_valued & ( for n being Nat holds F . n = chi ((f . n),X) ) holds
for x being object st x in X holds
(chi ((Union f),X)) . x = (lim (Partial_Sums F)) . x
let S be non empty Subset-Family of X; :: thesis: for f being Function of NAT,S
for F being Functional_Sequence of X,ExtREAL st f is disjoint_valued & ( for n being Nat holds F . n = chi ((f . n),X) ) holds
for x being object st x in X holds
(chi ((Union f),X)) . x = (lim (Partial_Sums F)) . x
let f be Function of NAT,S; :: thesis: for F being Functional_Sequence of X,ExtREAL st f is disjoint_valued & ( for n being Nat holds F . n = chi ((f . n),X) ) holds
for x being object st x in X holds
(chi ((Union f),X)) . x = (lim (Partial_Sums F)) . x
let F be Functional_Sequence of X,ExtREAL; :: thesis: ( f is disjoint_valued & ( for n being Nat holds F . n = chi ((f . n),X) ) implies for x being object st x in X holds
(chi ((Union f),X)) . x = (lim (Partial_Sums F)) . x )
assume A0: f is disjoint_valued ; :: thesis: ( ex n being Nat st not F . n = chi ((f . n),X) or for x being object st x in X holds
(chi ((Union f),X)) . x = (lim (Partial_Sums F)) . x )
assume A1: for n being Nat holds F . n = chi ((f . n),X) ; :: thesis: for x being object st x in X holds
(chi ((Union f),X)) . x = (lim (Partial_Sums F)) . x
let x be object ; :: thesis: ( x in X implies (chi ((Union f),X)) . x = (lim (Partial_Sums F)) . x )
assume A2: x in X ; :: thesis: (chi ((Union f),X)) . x = (lim (Partial_Sums F)) . x
then reconsider x1 = x as Element of X ;

A3: now :: thesis: for n, m being Nat st n <> m holds
for x being set holds
( not x in (dom (F . n)) /\ (dom (F . m)) or (F . n) . x <> +infty or (F . m) . x <> -infty )

let n, m be Nat; :: thesis: ( n <> m implies for x being set holds
( not x in (dom (F . n)) /\ (dom (F . m)) or (F . n) . x <> +infty or (F . m) . x <> -infty ) )
assume n <> m ; :: thesis: for x being set holds
( not x in (dom (F . n)) /\ (dom (F . m)) or (F . n) . x <> +infty or (F . m) . x <> -infty )

hereby :: thesis: verum

let x be set ; :: thesis: ( not x in (dom (F . n)) /\ (dom (F . m)) or (F . n) . x <> +infty or (F . m) . x <> -infty )
assume x in (dom (F . n)) /\ (dom (F . m)) ; :: thesis: ( (F . n) . x <> +infty or (F . m) . x <> -infty )
then A5: ( x in dom (F . n) & x in dom (F . m) ) by XBOOLE_0:def 4;
( F . n = chi ((f . n),X) & F . m = chi ((f . m),X) ) by A1;
then ( rng (F . n) c= {0,1} & rng (F . m) c= {0,1} ) by FUNCT_3:39;
then ( not +infty in rng (F . n) & not -infty in rng (F . m) ) ;
hence ( (F . n) . x <> +infty or (F . m) . x <> -infty ) by A5, FUNCT_1:3; :: thesis: verum

end;

end;

now :: thesis: for n, m being Nat holds dom (F . n) = dom (F . m)

let n, m be Nat; :: thesis: dom (F . n) = dom (F . m)
( F . n = chi ((f . n),X) & F . m = chi ((f . m),X) ) by A1;
then ( dom (F . n) = X & dom (F . m) = X ) by FUNCT_3:def 3;
hence dom (F . n) = dom (F . m) ; :: thesis: verum

end;

then A9: F is with_the_same_dom by MESFUNC8:def 2;
F . 0 = chi ((f . 0),X) by A1;
then A20: dom (F . 0) = X by FUNCT_3:def 3;
then dom ((Partial_Sums F) . 0) = X by MESFUNC9:def 4;
then x in dom (lim (Partial_Sums F)) by A2, MESFUNC8:def 9;
then A14: (lim (Partial_Sums F)) . x = lim ((Partial_Sums F) # x1) by MESFUNC8:def 9;

per cases ( x in Union f or not x in Union f ) ;

suppose A10: x in Union f ; :: thesis: (chi ((Union f),X)) . x = (lim (Partial_Sums F)) . x

then x in union (rng f) by CARD_3:def 4;
then consider V being set such that
A11: ( x in V & V in rng f ) by TARSKI:def 4;
consider n being Element of NAT such that
A12: V = f . n by A11, FUNCT_2:113;
A15: for m being Nat st m <> n holds
(F . m) . x1 = 0

proof

let m be Nat; :: thesis: ( m <> n implies (F . m) . x1 = 0 )
assume m <> n ; :: thesis: (F . m) . x1 = 0
then not x in f . m by A0, PROB_2:def 2, A11, A12, XBOOLE_0:3;
then (chi ((f . m),X)) . x = 0 by A2, FUNCT_3:def 3;
hence (F . m) . x1 = 0 by A1; :: thesis: verum

end;

defpred S₁[ Nat] means ( $1 < n implies ((Partial_Sums F) # x1) . $1 = 0 );

now :: thesis: ( 0 < n implies ((Partial_Sums F) # x1) . 0 = 0 )

assume A16: 0 < n ; :: thesis: ((Partial_Sums F) # x1) . 0 = 0
((Partial_Sums F) # x1) . 0 = ((Partial_Sums F) . 0) . x1 by MESFUNC5:def 13
.= (F . 0) . x1 by MESFUNC9:def 4 ;
hence ((Partial_Sums F) # x1) . 0 = 0 by A15, A16; :: thesis: verum

end;

then A17: S₁[ 0 ] ;
A18: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A19: S₁[k] ; :: thesis: S₁[k + 1]
assume A21: k + 1 < n ; :: thesis: ((Partial_Sums F) # x1) . (k + 1) = 0
then A22: (Partial_Sums (F # x1)) . k = 0 by A9, A19, A20, A3, MESFUNC9:def 5, MESFUNC9:32, NAT_1:13;
((Partial_Sums F) # x1) . (k + 1) = (Partial_Sums (F # x1)) . (k + 1) by A3, A9, A20, MESFUNC9:def 5, MESFUNC9:32
.= ((Partial_Sums (F # x1)) . k) + ((F # x1) . (k + 1)) by MESFUNC9:def 1
.= (F # x1) . (k + 1) by A22, XXREAL_3:4
.= (F . (k + 1)) . x1 by MESFUNC5:def 13 ;
hence ((Partial_Sums F) # x1) . (k + 1) = 0 by A15, A21; :: thesis: verum

end;

A23: for k being Nat holds S₁[k] from NAT_1:sch 2(A17, A18);
defpred S₂[ Nat] means ( $1 >= n implies ((Partial_Sums F) # x1) . $1 = 1 );

now :: thesis: ( 0 >= n implies ((Partial_Sums F) # x1) . 0 = 1 )

assume 0 >= n ; :: thesis: ((Partial_Sums F) # x1) . 0 = 1
then A24: n = 0 ;
A25: ((Partial_Sums F) # x1) . 0 = ((Partial_Sums F) . 0) . x1 by MESFUNC5:def 13
.= (F . 0) . x1 by MESFUNC9:def 4 ;
F . 0 = chi ((f . n),X) by A24, A1;
hence ((Partial_Sums F) # x1) . 0 = 1 by A25, A11, A12, FUNCT_3:def 3; :: thesis: verum

end;

then A26: S₂[ 0 ] ;
A27: for k being Nat st S₂[k] holds
S₂[k + 1]

proof

let k be Nat; :: thesis: ( S₂[k] implies S₂[k + 1] )
assume A28: S₂[k] ; :: thesis: S₂[k + 1]
assume A29: k + 1 >= n ; :: thesis: ((Partial_Sums F) # x1) . (k + 1) = 1
A30: ((Partial_Sums F) # x1) . (k + 1) = (Partial_Sums (F # x1)) . (k + 1) by A3, A9, A20, MESFUNC9:def 5, MESFUNC9:32
.= ((Partial_Sums (F # x1)) . k) + ((F # x1) . (k + 1)) by MESFUNC9:def 1 ;

per cases ( k >= n or k < n ) ;

suppose A31: k >= n ; :: thesis: ((Partial_Sums F) # x1) . (k + 1) = 1

then k + 1 > n by NAT_1:13;
then (F . (k + 1)) . x1 = 0 by A15;
then (F # x1) . (k + 1) = 0 by MESFUNC5:def 13;
then ((Partial_Sums F) # x1) . (k + 1) = (Partial_Sums (F # x1)) . k by A30, XXREAL_3:4;
hence ((Partial_Sums F) # x1) . (k + 1) = 1 by A28, A31, A3, A9, A20, MESFUNC9:def 5, MESFUNC9:32; :: thesis: verum

end;

suppose A33: k < n ; :: thesis: ((Partial_Sums F) # x1) . (k + 1) = 1

then A34: k + 1 = n by A29, NAT_1:8;
((Partial_Sums F) # x1) . k = 0 by A23, A33;
then (Partial_Sums (F # x1)) . k = 0 by A3, A9, A20, MESFUNC9:def 5, MESFUNC9:32;
then ((Partial_Sums F) # x1) . (k + 1) = (F # x1) . (k + 1) by A30, XXREAL_3:4
.= (F . (k + 1)) . x1 by MESFUNC5:def 13
.= (chi ((f . (k + 1)),X)) . x by A1 ;
hence ((Partial_Sums F) # x1) . (k + 1) = 1 by A34, A11, A12, FUNCT_3:def 3; :: thesis: verum

end;

end;

end;

A35: for k being Nat holds S₂[k] from NAT_1:sch 2(A26, A27);
for k being Nat holds (((Partial_Sums F) # x1) ^\ n) . k = 1

proof

let k be Nat; :: thesis: (((Partial_Sums F) # x1) ^\ n) . k = 1
(((Partial_Sums F) # x1) ^\ n) . k = ((Partial_Sums F) # x1) . (n + k) by NAT_1:def 3;
hence (((Partial_Sums F) # x1) ^\ n) . k = 1 by A35, NAT_1:12; :: thesis: verum

end;

then ( ((Partial_Sums F) # x1) ^\ n is convergent_to_finite_number & lim (((Partial_Sums F) # x1) ^\ n) = 1 ) by MESFUNC5:52;
then (lim (Partial_Sums F)) . x = 1 by A14, RINFSUP2:16;
hence (chi ((Union f),X)) . x = (lim (Partial_Sums F)) . x by A10, A2, FUNCT_3:def 3; :: thesis: verum

end;

suppose A37: not x in Union f ; :: thesis: (chi ((Union f),X)) . x = (lim (Partial_Sums F)) . x

then not x in union (rng f) by CARD_3:def 4;
then A38: for V being set st V in rng f holds
not x in V by TARSKI:def 4;
defpred S₁[ Nat] means ((Partial_Sums F) # x1) . $1 = 0 ;
A39: ((Partial_Sums F) # x1) . 0 = ((Partial_Sums F) . 0) . x1 by MESFUNC5:def 13
.= (F . 0) . x1 by MESFUNC9:def 4
.= (chi ((f . 0),X)) . x1 by A1 ;
not x in f . 0 by A38, FUNCT_2:4;
then A40: S₁[ 0 ] by A39, FUNCT_3:def 3;
A41: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume S₁[k] ; :: thesis: S₁[k + 1]
then A42: (Partial_Sums (F # x1)) . k = 0 by A3, A9, A20, MESFUNC9:def 5, MESFUNC9:32;
A43: ((Partial_Sums F) # x1) . (k + 1) = (Partial_Sums (F # x1)) . (k + 1) by A3, A9, A20, MESFUNC9:def 5, MESFUNC9:32
.= ((Partial_Sums (F # x1)) . k) + ((F # x1) . (k + 1)) by MESFUNC9:def 1
.= (F # x1) . (k + 1) by A42, XXREAL_3:4
.= (F . (k + 1)) . x1 by MESFUNC5:def 13
.= (chi ((f . (k + 1)),X)) . x by A1 ;
not x in f . (k + 1) by A38, FUNCT_2:4;
hence S₁[k + 1] by A43, FUNCT_3:def 3; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A40, A41);
then ( (Partial_Sums F) # x1 is convergent_to_finite_number & lim ((Partial_Sums F) # x1) = 0 ) by MESFUNC5:52;
hence (chi ((Union f),X)) . x = (lim (Partial_Sums F)) . x by A37, A14, FUNCT_3:def 3; :: thesis: verum

end;

end;