let Omega be non empty set ; :: thesis: for f being SetSequence of Omega st f is disjoint_valued holds
for X being Subset of Omega holds seqIntersection (X,f) is disjoint_valued
let f be SetSequence of Omega; :: thesis: ( f is disjoint_valued implies for X being Subset of Omega holds seqIntersection (X,f) is disjoint_valued )
assume A1: f is disjoint_valued ; :: thesis: for X being Subset of Omega holds seqIntersection (X,f) is disjoint_valued
let X be Subset of Omega; :: thesis: seqIntersection (X,f) is disjoint_valued
for n, m being Element of NAT st n < m holds
(seqIntersection (X,f)) . n misses (seqIntersection (X,f)) . m

proof

let n, m be Element of NAT ; :: thesis: ( n < m implies (seqIntersection (X,f)) . n misses (seqIntersection (X,f)) . m )
assume n < m ; :: thesis: (seqIntersection (X,f)) . n misses (seqIntersection (X,f)) . m
then f . n misses f . m by A1;
then A2: X /\ (f . n) misses f . m by XBOOLE_1:74;
( (seqIntersection (X,f)) . n = X /\ (f . n) & (seqIntersection (X,f)) . m = X /\ (f . m) ) by Def1;
hence (seqIntersection (X,f)) . n misses (seqIntersection (X,f)) . m by A2, XBOOLE_1:74; :: thesis: verum

end;

hence seqIntersection (X,f) is disjoint_valued ; :: thesis: verum