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: 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 A2: S₁[p] ; :: thesis: S₁[p ^ <*y*>]
S₁[p ^ <*y*>]

proof

assume A3: p ^ <*y*> is disjoint_valued ; :: thesis: (MemberFunc (Union (p ^ <*y*>)),A) . x = Sum (FinSeqM x,(p ^ <*y*>))
A4: Union p misses y

proof

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

end;

Union (p ^ <*y*>) = (Union p) \/ (Union <*y*>) by Th5
.= (Union p) \/ y by FUNCT_6:39 ;
then (MemberFunc (Union (p ^ <*y*>)),A) . x = ((MemberFunc (Union p),A) . x) + ((MemberFunc y,A) . x) by A4, Th51
.= Sum ((FinSeqM x,p) ^ <*((MemberFunc y,A) . x)*>) by A2, A3, 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;

A13: S₁[ <*> (bool the carrier of A)]

proof

set F = FinSeqM x,(<*> (bool the carrier of A));
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)))
dom (FinSeqM x,(<*> (bool the carrier of A))) = dom (<*> (bool the carrier of A)) by Def10;
then A14: 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 A14, Th54; :: thesis: verum

end;

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