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, PROB_2:def 3;
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 Def2;
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 by Def3; :: thesis: verum