let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma 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 Sigma 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 Sigma; :: 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 object such that
A3: x in (Partial_Union ASeq) . n and
A4: x in ASeq . m by XBOOLE_0:3;
reconsider ASeq = ASeq as SetSequence of Omega ;
consider k being Nat such that
A5: k <= n and
A6: x in ASeq . k by A3, Th13;
ASeq . k misses ASeq . m by A1, A2, A5;
then (ASeq . k) /\ (ASeq . m) = {} ;
hence contradiction by A4, A6, XBOOLE_0:def 4; :: thesis: verum