let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for ASeq being SetSequence of st ASeq is disjoint_valued holds
for n, m being Nat st n < m holds
(@Partial_Union ASeq) . n misses ASeq . m
let Sigma be SigmaField of Omega; :: thesis: for ASeq being SetSequence of st ASeq is disjoint_valued holds
for n, m being Nat st n < m holds
(@Partial_Union ASeq) . n misses ASeq . m
let ASeq be SetSequence of ; :: thesis: ( ASeq is disjoint_valued implies for n, m being Nat st n < m holds
(@Partial_Union ASeq) . n misses ASeq . m )
assume A1: ASeq is disjoint_valued ; :: thesis: for n, m being Nat st n < m holds
(@Partial_Union ASeq) . n misses ASeq . m
let n, m be Nat; :: thesis: ( n < m implies (@Partial_Union ASeq) . n misses ASeq . m )
assume A2: n < m ; :: thesis: (@Partial_Union ASeq) . n misses ASeq . m
assume (@Partial_Union ASeq) . n meets ASeq . m ; :: thesis: contradiction
then consider x being set such that
A3: ( x in (@Partial_Union ASeq) . n & x in ASeq . m ) by XBOOLE_0:3;
consider k being Nat such that
A4: ( k <= n & x in ASeq . k ) by A3, Th15;
( m in NAT & k in NAT ) by ORDINAL1:def 13;
then ASeq . k misses ASeq . m by A1, A2, A4, PROB_2:def 4;
then (ASeq . k) /\ (ASeq . m) = {} by XBOOLE_0:def 7;
hence contradiction by A3, A4, XBOOLE_0:def 4; :: thesis: verum