let A be finite Approximation_Space; :: thesis: for x being Element of A
for X being disjoint_valued FinSequence of bool the carrier of A holds (MemberFunc (Union X),A) . x = Sum (FinSeqM x,X)
let x be Element of A; :: thesis: for X being disjoint_valued FinSequence of bool the carrier of A holds (MemberFunc (Union X),A) . x = Sum (FinSeqM x,X)
let X be disjoint_valued FinSequence of bool the carrier of A; :: thesis: (MemberFunc (Union X),A) . x = Sum (FinSeqM x,X)
defpred S₁[ FinSequence of bool the carrier of A] means ( $1 is disjoint_valued implies (MemberFunc (Union $1),A) . x = Sum (FinSeqM x,$1) );
A1: S₁[ <*> (bool the carrier of A)]

proof

assume <*> (bool the carrier of A) is disjoint_valued ; :: thesis: (MemberFunc (Union (<*> (bool the carrier of A))),A) . x = Sum (FinSeqM x,(<*> (bool the carrier of A)))
set F = FinSeqM x,(<*> (bool the carrier of A));
dom (FinSeqM x,(<*> (bool the carrier of A))) = dom (<*> (bool the carrier of A)) by Def10;
then A2: Sum (FinSeqM x,(<*> (bool the carrier of A))) = 0 by RELAT_1:64, RVSUM_1:102;
Union (<*> (bool the carrier of A)) = {} A by ZFMISC_1:2;
hence (MemberFunc (Union (<*> (bool the carrier of A))),A) . x = Sum (FinSeqM x,(<*> (bool the carrier of A))) by A2, Th54; :: thesis: verum

end;

A3: for p being FinSequence of bool the carrier of A
for y being Subset of A st S₁[p] holds
S₁[p ^ <*y*>]

proof

let p be FinSequence of bool the carrier of A; :: thesis: for y being Subset of A st S₁[p] holds
S₁[p ^ <*y*>]
let y be Subset of A; :: thesis: ( S₁[p] implies S₁[p ^ <*y*>] )
assume A4: S₁[p] ; :: thesis: S₁[p ^ <*y*>]
S₁[p ^ <*y*>]

proof

assume A5: p ^ <*y*> is disjoint_valued ; :: thesis: (MemberFunc (Union (p ^ <*y*>)),A) . x = Sum (FinSeqM x,(p ^ <*y*>))
A7: Union (p ^ <*y*>) = (Union p) \/ (Union <*y*>) by Th5
.= (Union p) \/ y by FUNCT_6:39 ;
Union p misses y

proof

assume Union p meets y ; :: thesis: contradiction
then consider x being set such that
A8: ( x in Union p & x in y ) by XBOOLE_0:3;
consider X being set such that
A9: ( x in X & X in rng p ) by A8, TARSKI:def 4;
consider m being set such that
A10: ( m in dom p & X = p . m ) by A9, FUNCT_1:def 5;
reconsider m = m as Element of NAT by A10;
A11: p . m meets y by A8, A9, A10, XBOOLE_0:3;
A12: (p ^ <*y*>) . m = p . m by A10, FINSEQ_1:def 7;
A13: (p ^ <*y*>) . ((len p) + 1) = y by FINSEQ_1:59;
A14: len p < (len p) + 1 by NAT_1:13;
m <= len p by A10, FINSEQ_3:27;
hence contradiction by A5, A11, A12, A13, A14, PROB_2:def 3; :: thesis: verum

end;

then (MemberFunc (Union (p ^ <*y*>)),A) . x = ((MemberFunc (Union p),A) . x) + ((MemberFunc y,A) . x) by A7, Th51
.= Sum ((FinSeqM x,p) ^ <*((MemberFunc y,A) . x)*>) by A4, A5, Th6, FINSEQ_6:12, RVSUM_1:104
.= Sum (FinSeqM x,(p ^ <*y*>)) by Th53 ;
hence (MemberFunc (Union (p ^ <*y*>)),A) . x = Sum (FinSeqM x,(p ^ <*y*>)) ; :: thesis: verum

end;

hence S₁[p ^ <*y*>] ; :: thesis: verum

end;

for p being FinSequence of bool the carrier of A holds S₁[p] from FINSEQ_2:sch 2(A1, A3);
hence (MemberFunc (Union X),A) . x = Sum (FinSeqM x,X) ; :: thesis: verum